4

私は次の定義を持っています：

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)
4

2 に答える 2

6

標準ライブラリhttp://www.cse.chalmers.se/~nad/listings/lib/Data.Nat.Properties.html#10457でその補題の証明を見つけることができ ます

于 2012-10-21T01:10:12.440 に答える
4

この補題を試してください:

weaken : {x y : Nat} -> x <= y -> x <= succ y
weaken z<=n = z<=n
weaken (s<=s n<=m) = s<=s (weaken n<=m)
于 2012-10-21T01:20:20.537 に答える