我有下一个定义:
data Nat : Set where
zero : Nat
succ : Nat -> Nat
prev : Nat -> Nat
prev zero = zero
prev (succ n) = n
data _<=_ : Nat -> Nat -> Set where
z<=n : forall {n} -> zero <= n
s<=s : forall {n m} -> (n<=m : n <= m) -> (succ n) <= (succ m)
很容易证明下一个引理:
lem-prev : {x y : Nat} -> x <= y -> (prev x) <= (prev y)
lem-prev z<=n = z<=n
lem-prev (s<=s t) = t
但我找不到证明下一个引理的方法:
lem-prev' : {x y : Nat} -> x <= y -> (prev x) <= y
我可以将定义更改<=
为下一个:
data _<='_ : Nat -> Nat -> Set where
z<=n' : forall {n} -> zero <=' n
s<=s' : forall {n m} -> (n<=m : n <=' m) -> (succ n) <=' m
在那种情况下,我可以证明lem-prev'
:
lem-prev' : {x y : Nat} -> x <=' y -> (prev x) <=' y
lem-prev' z<=n' = z<=n'
lem-prev' (s<=s' t) = t
但现在我无法证明lem-prev
。
有没有办法证明<=
和/或的引理<='
?如果不是,那么我应该如何更改定义以使其成为可能?
添加:使用 hammar 的辅助引理的解决方案:
lem-prev : {x y : Nat} -> x <= y -> (prev x) <= y
lem-prev z<=n = z<=n
lem-prev (s<=s prev-n<=prev-m) = weaken (prev-n<=prev-m)