假设我们想在minus
s上有一个“适当的”Nat
,需要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
如果我正确理解了这个错误,那只是意味着它试图将目标相等的RHS(即minus { prf = prf2 } (S n + m) k
)重写为minus { prf = prf2 } (n + S m) k
并失败。当然,正确地说,因为prf
证明了不同的不平等!虽然replace
可以用来生成(S n + m) k
的证明(或prf1
也可以),但看起来不可能同时重写和更改证明对象以使其与重写相匹配。
我该如何解决这个问题?或者,更一般地说,我如何证明这个引理?
好的,我想我解决了。一句话:如果你不知道该怎么做,那就做一个引理吧!
因此,我们有两个muexswpoi相等的证明,我们需要生成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