在 Idris 中为决策函数构建证明

Question

我正在尝试为表示模块化空间中两个连续元素的类型创建决策函数。

（此代码源自from this excellent answer 到我的上一个问题。）

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，您能否解释一下它们的工作原理以及它们在证明中的作用？

Answer 1

虽然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 来证明一些 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 的 lambda：

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之后应该是false，所以我们为它创建了一个函数：

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