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

Question

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

（此代码源自我之前的一个问题。）

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-构造函数中的 prf 需要 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 的 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。但是可以看到afterlte : 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

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

Constructing proofs for a decision function in Idris

proof

idris

theorem-proving