證明（先前N）<= M選自正開始<=米

Question

我有下定義：

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。

有沒有辦法來證明<=和/或<='的引文？ 如果不是，那麼我應該如何更改定義才能使它成爲可能？

地址：使用哈馬爾的助手引理解決辦法：

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) 

Answer 1

試試這個引理：

weaken : {x y : Nat} -> x <= y -> x <= succ y 
weaken z<=n = z<=n 
weaken (s<=s n<=m) = s<=s (weaken n<=m) 

Answer 2

你可以找到引理的證明標準庫 http://www.cse.chalmers.se/~nad/listings/lib/Data.Nat.Properties.html#10457