根据（进一步）证明证明类型相等答案

【问题标题】：Proving equality of types depending on (further) proofs根据（进一步）证明证明类型相等
【发布时间】：2019-02-27 19:51:37
【问题描述】：

假设我们想在Nats 上有一个“正确的”minus，需要m <= n 才能使n `minus` m 有意义：

%hide minus

minus : (n, m : Nat) -> { auto prf : m `LTE` n } -> Nat
minus { prf = LTEZero } n Z = n
minus { prf = LTESucc prevPrf } (S n) (S m) = minus n m

现在让我们尝试证明以下引理，声明(n + (1 + m)) - k = ((1 + n) + m) - k，假设双方都有效：

minusPlusTossS : (n, m, k : Nat) ->
                 { auto prf1 : k `LTE` n + S m } ->
                 { auto prf2 : k `LTE` S n + m } ->
                 minus (n + S m) k = minus (S n + m) k

目标表明以下问题可能会有所帮助：

plusTossS : (n, m : Nat) -> n + S m = S n + m
plusTossS Z m = Refl
plusTossS (S n) m = cong $ plusTossS n m

所以我们尝试使用它：

minusPlusTossS n m k =
  let tossPrf = plusTossS n m
  in rewrite tossPrf in ?rhs

我们失败了：

When checking right hand side of minusPlusTossS with expected type
        minus (n + S m) k = minus (S n + m) k

When checking argument prf to function Main.minus:
        Type mismatch between
                LTE k (S n + m) (Type of prf2)
        and
                LTE k replaced (Expected type)

        Specifically:
                Type mismatch between
                        S (plus n m)
                and
                        replaced

如果我正确理解了这个错误，它只是意味着它试图将目标相等（即minus { prf = prf2 } (S n + m) k）的 RHS 重写为minus { prf = prf2 } (n + S m) k 并且失败。当然，这是正确的，因为prf 是不同不等式的证明！虽然replace 可用于生成(S n + m) k 的证明（或prf1 也可以），但看起来不可能同时重写和更改证明对象以使其与重写匹配。

我该如何解决这个问题？或者，更一般地说，我如何证明这个引理？

【问题讨论】：

也许您可以将您的证明包含在plusTossS 中，以便人们可以更好地重现您的代码。
你可能需要对证明做一些智能的事情：``` minusPlusTossS n m Z {prf1 = LTEZero} {prf2 = LTEZero} = let tossPrf = plusTossS n m in rewrite tossPrf in Refl ``` typechecks ，但不是全部。
@Markus 我猜这是因为类型检查器无法将k `LTE` n + S m 与LTESucc 的可用表单相匹配。当然，我们可以将该证明重写为 k `LTE` S (n + m)，但这对我来说并不是特别有成果。

标签： idris dependent-type

【解决方案1】：

好的，我想我解决了。底线：如果您不知道该怎么做，请做一个引理！

所以我们有两个被减数n1, n2 相等的证明，我们需要产生n1 `minus` m = n2 `minus` m 的证明。让我们写下来！

minusReflLeft : { n1, n2, m : Nat } -> (prf : n1 = n2) -> (prf_n1 : m `LTE` n1) -> (prf_n2 : m `LTE` n2) -> n1 `minus` m = n2 `minus` m
minusReflLeft Refl LTEZero LTEZero = Refl
minusReflLeft Refl (LTESucc prev1) (LTESucc prev2) = minusReflLeft Refl prev1 prev2

我什至不再需要plusTossS，可以用更直接适用的引理代替：

plusRightS : (n, m : Nat) -> n + S m = S (n + m)
plusRightS Z m = Refl
plusRightS (S n) m = cong $ plusRightS n m

之后，原来的就变得微不足道了：

minusPlusTossS : (n, m, k : Nat) ->
                 { auto prf1 : k `LTE` n + S m } ->
                 { auto prf2 : k `LTE` S n + m } ->
                 minus (n + S m) k = minus (S n + m) k
minusPlusTossS {prf1} {prf2} n m k = minusReflLeft (plusRightS n m) prf1 prf2

【讨论】：