我正在尝试为表示模块化空间中两个连续元素的类型创建一个决策函数。
(这段代码是从我之前的一个问题中得出的这个出色的答案。
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
我已经尽力了，但我的知识还不够，无法自己构建必要的证明，尤其是矛盾的证明。你能告诉我如何填补上面代码中的一个或多个漏洞吗？
另外，如果你使用任何方便的工具，如absurd、impossible或策略，你能解释一下它们是如何工作的以及它们在证明中所扮演的角色吗？
虽然PreceedsN构造函数中的prfs需要一个LTE证明(LT a b只是LTE (S a) b的同义词(，但你的第一个cmp只是拆分S a。相反，您应该直接获得LTE证明：
doesPreceedN m a b with (S (S a) `isLTE` m)
如果您不需要重用所有变量，则在with情况下省略重复会使事情变得更漂亮。因此，要重复您的版本LTE，我们有：
| (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。您可以创建一个引理(您的编辑器可能有该引理的绑定(，也可以使用具有大小写拆分的 lambda。对于像这样的短函数，我更喜欢后者。对于?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
prf是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=(x => LTE (S x) m)}来显式设置P。
结果：
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)我们可以替换Vect (n + m) a的n + m部分Vect (m + n) a.这里P=to_replace => Vect to_replace a，所以P只是一个函数Type -> Type。
在doesPreceedN我们需要明确P。大多数时候，rewrite … in …(一种策略(可以自动找到此P并应用replace。 另一方面，replace只是一个简单的函数:printdef replace：
replace : (x = y) -> P x -> P y
replace Refl prf = prf