代码之家 › 专栏 › 技术社区 › Etherian

IDRIS中决策函数的构造证明

theorem-proving idris proof

Etherian · 技术社区 · 6 年前

data PreceedsN : Nat -> Nat -> Nat -> Type where
    PreceedsS : {auto prf : S a `LT` m} -> PreceedsN m a (S a)
    PreceedsZ : {auto prf : S a = m} -> PreceedsN m a Z

doesPreceedN : (m : Nat) -> (a : Nat) -> (b : Nat) -> Dec (PreceedsN m a b)
doesPreceedN m a b with (S a `cmp` m)
    doesPreceedN (S a + S d) a b     | CmpLT d with (S a `decEq` b)
        doesPreceedN (S a + S d) a b | CmpLT d | Yes prf = Yes ?bIsSa
        doesPreceedN (S a + S d) a b | CmpLT d | No contra = No ?bNotSa
    doesPreceedN (S m) m b     | CmpEQ   with (b `decEq` 0)
        doesPreceedN (S m) m Z | CmpEQ | Yes prf = Yes PreceedsZ
        doesPreceedN (S m) m b | CmpEQ | No contra = No ?saIsmAndbIsNotZ
    doesPreceedN (S m) (m + (S d)) b | CmpGT d = No ?saCannotBeGTm

我已经尽了最大的努力,但我还不太清楚自己是否能独立构建必要的证明,尤其是矛盾的证明。你能告诉我怎么填一个或多个 holes

另外,如果你使用任何方便的工具,比如 absurd ,请 impossible tactics ,你能解释一下它们是如何工作的,它们在证据中扮演的角色吗?

1 回复 | 直到 6 年前

xash 6 年前

而 prf PreceedsN -构造函数需要 LTE LT a b LTE (S a) b )你的第一个 cmp S a 证明:

doesPreceedN m a b with (S (S a) `isLTE` m)

with ,我们有:

  | (Yes lte) = case (decEq b (S a)) of
      Yes Refl => PreceedsS
      No notlte => No ?contra_notlte
  | (No notlte) with (decEq (S a) m)
    | Yes eq = case b of
      Z => Yes PreceedsZ
      (S b) => No ?contra_notZ
    | No noteq = No ?contra_noteq

a -> Void ,所以你可以假设,你有 a ?contra_notZ

No (\contra => case contra of prec => ?contra_notZ)

如果你分开 prec

No (\contra => case contra of PreceedsS => ?contra_notZ)

notlte : LTE (S (S b)) m -> Void
prf : LTE (S (S b)) m

PreceedsS

No (\contra => case contra of (PreceedsS {prf}) => notlte prf)

?contra_noteq 可以类似地解决。

?contra_notlte

No notlte => No (\contra => case contra of
  PreceedsS => ?contra_notlte_1
  PreceedsZ => ?contra_notlte_2)

检查类型给出:

:t ?contra_notlte_1
notlte : (S a = S a) -> Void
:t ?contra_notlte_2
lte : LTE (S (S a)) m
prf : S a = m

?contra_notlte_2 notlte .但你可以在那之后看到 lte : LTE (S m) m

notLTE : Not (LTE (S n) n)
notLTE LTEZero impossible
notLTE (LTESucc lte) = notLTE lte

现在我们有:

PreceedsZ {prf} => notLTE ?contra_notlte_2
?contra_notlte_2 : LTE (S n) n

(rewrite prf in lte) 但那不起作用,因为策略找不到合适的属性来重写。但我们可以明确指出:

PreceedsZ {prf} => notLTE (replace prf lte)

> Type mismatch between
        LTE (S (S a)) m
and
        P (S a)

P 通过设置显式 {P=(\x => LTE (S x) m)}

结果是:

doesPreceedN : (m : Nat) -> (a : Nat) -> (b : Nat) -> Dec (PreceedsN m a b)
doesPreceedN m a b with (S (S a) `isLTE` m)
  | (Yes lte) = case (decEq b (S a)) of
    Yes Refl => Yes PreceedsS
    No notlte => No (\contra => case contra of
      PreceedsS => notlte Refl
      PreceedsZ {prf} => notLTE  (replace prf {P=(\x => LTE (S x) m)} lte))
  | (No notlte) with (decEq (S a) m)
    | Yes eq = case b of
      Z => Yes PreceedsZ
      (S b) => No (\contra => case contra of (PreceedsS {prf}) => notlte prf)
    | No noteq = No (\contra => case contra of 
        PreceedsS {prf} => notlte prf
        PreceedsZ {prf} => noteq prf)

replace : (x = y) -> P x -> P y 例如,使用 (n + m = m + n) n + m 的一部分 Vect (n + m) a Vect (m + n) a P=\to_replace => Vect to_replace a 只是一个函数 Type -> Type

doesPreceedN .大多数时候, rewrite â¦ in â¦ replace 代替 :printdef replace 以下内容:

replace : (x = y) -> P x -> P y
replace Refl prf = prf