Agda の不等号の推論

最近いじってた Data.Fin とか < とか ≤ とか良くでてきてて、substとか<-transで適当に片付けていたんですが、

某所から降ってきたのが、結構、使いまくり。

　Agdaの特徴である推論使えないの?

だよなあ。で、

lemma1 : suc (suc m + n * suc m) ≤ suc (k * suc m) → suc (suc m + suc n * suc m ) ≤ suc (suc k * suc m)
lemma1 (s≤s lt) = s≤s ( s≤s (subst (λ x → x ) (
　 begin
　　 suc m + n * suc m ≤ k * suc m
　 ≡⟨⟩
　　 suc n * suc m　　 ≤ k * suc m
　 ≡⟨ ? ⟩
　　 m + suc n * suc m ≤ m + k * suc m
　 ∎ ) lt ))　where open ≡-Reasoning

とかやってみる。でも、これはだめ。suc n < suc m と n < m は等しくないから。

Bool で Setoid すればできるんじゃないかと思って agda-stdlib 見てたら、

　　agda-stdlib/src/Data/Nat/Properties.agda
　　-- A module for reasoning about the _≤_ and _<_ relations
　　module ≤-Reasoning where
　　　open import Relation.Binary.Reasoning.Base.Triple

なんだ、そこかぁ。

　　 lemma : {n k m : ℕ } → n < k　→ suc (k * suc m) > suc m + n * suc m
　　 lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y ))
　　 lemma {suc n} {suc k} {m} lt = begin
　　　　　　　　 suc (suc m + suc n * suc m)
　　　　　　　≡⟨⟩
　　　　　　　　 suc ( suc (suc n) * suc m)
　　　　　　　≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩
　　　　　　　　 suc (suc k * suc m)
　　　　　　　∎　 where open ≤-Reasoning

みたいに使うらしい。使い方は stdlib を grep して見つけました。