前回までの記事で、MyIntが半順序集合(≈ partial order)であることを示しました。今回はその続きとして、MyIntが全順序であること、さらに順序環であることを証明していきます。この2つの性質が揃うと、Mathlibのlinarithやnlinarithといった強力な自動証明タクティクが使えるようになり、不等式を含む証明が一気に書きやすくなります。今回の内容はゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発の該当章に沿っています。
全順序とは
集合Xにおける二項関係が全順序であるとは、次の2つを満たすことをいいます。
- Xがその二項関係について半順序集合である
- \( \forall x, y \in X,\ x \le y \lor y \le x \)
半順序は「比較できない要素があってもよい」順序でしたが、全順序ではどの2つの要素をとっても必ずどちらかがどちらか以下になります。MyIntはすでに半順序であることがわかっているので、あとは任意の2元が比較可能であることさえ示せば全順序であることが言えます。
0 ≤ a ∨ 0 ≤ -a の証明
いきなり\( a \le b \lor b \le a \)を狙うのではなく、まずは\( 0 \le a \lor 0 \le -a \)という補題を用意します。MyIntは\( m - n \)の形の商型として定義されているので、Quotient.inductionOnで代表元のペア(m, n)を取り出せば、話はMyNatの世界の大小比較に帰着します。MyNatはすでに全順序(MyNat.le_total)であることを証明済みなので、そこからn ≤ mかm ≤ nのどちらかが言え、あとはsimp [mk_def]とnorm_castでMyIntの言葉に翻訳するだけです。
theorem MyInt.nonneg_or_nonneg_neg {a : MyInt} : 0 ≤ a ∨ 0 ≤ -a := by
induction a using Quotient.inductionOn with
| h a =>
obtain ⟨m, n⟩ := a
have : n ≤ m ∨ m ≤ n := by
exact MyNat.le_total n m
cases this with
| inl h =>
left
simp [mk_def]
norm_cast
| inr h =>
right
simp [mk_def]
norm_castMyInt.le_total の証明
本題の\( a \le b \lor b \le a \)は、\( 0 \le b - a \lor 0 \le -(b - a) \)という形に置き換えると、先ほどの補題がそのまま使えます。ここでsufficesタクティクを使い、「この形が示せればゴールも示せる」ことを先に片付けてから、実際にその形を証明する流れです。\( 0 \le b - a \)から\( a \le b \)への変換には前回定義したMyInt.sub_nonnegを使い、もう片方はabelタクティクで\( -(b-a) = a - b \)という可換群の計算を自動で処理させています。
theorem MyInt.le_total (a b : MyInt) : a ≤ b ∨ b ≤ a := by
suffices goal : 0 ≤ b - a ∨ 0 ≤ -(b -a) from by
cases goal with
| inl h =>
left
rw [← MyInt.sub_nonneg]
assumption
| inr h =>
right
rw [← MyInt.sub_nonneg]
rw [show -(b -a) = a - b from by abel] at h
assumption
exact MyInt.nonneg_or_nonneg_negLinearOrderへの登録
全順序であることが証明できたので、MathlibのLinearOrder型クラスにMyIntを登録します。le_totalフィールドに先ほどの定理を渡すだけで済み、決定可能性(toDecidableLE)はすでにあるDecidableLEインスタンスからinfer_instanceで自動導出できます。
instance : LinearOrder MyInt where
le_total := MyInt.le_total
toDecidableLE := by infer_instanceこの登録によって、orderタクティクが使えるようになります。orderタクティクは、≤・<・=に関する既知の事実から、全順序の公理だけを使って導ける結論を自動で探してくれるタクティクです。例えば次のように、場合分けの一部をorderに任せることができます。
theorem MyInt.eq_or_lt_of_le {a b : MyInt} (h : a ≤ b) : a = b ∨ a < b := by
by_cases hor : a = b
case pos =>
left
assumption
case neg =>
right
order
theorem MyInt.le_of_eq_or_lt {a b : MyInt} (h : a = b ∨ a < b) : a ≤ b := by
cases h with
| inl h => rw [h]
| inr h => order
theorem MyInt.le_iff_eq_or_lt (m n : MyInt) : n ≤ m ↔ n = m ∨ n < m := by
constructor
case mp => apply MyInt.eq_or_lt_of_le
case mpr => apply MyInt.le_of_eq_or_lt順序環とは
次はMyIntが順序環であることを示します。順序環とは、集合Xとその上の2つの二項演算が環をなし、さらに次の2条件を満たすもののことです。
- \( \forall x, y, z \in X,\ x \le y \to x + z \le y + z \)
- \( \forall x, y \in X,\ 0 \le x \land 0 \le y \to 0 \le x \cdot y \)
つまり、順序が加法とは常に整合し、乗法とは非負の範囲で整合する、という性質です。これをMathlibの型クラスとして登録することが目標です。
狭義順序を加法の式へ変換する
MyIntの狭義順序\( a < b \)は\( a \le b \land \lnot (b \le a) \)として定義されています。これから先の証明では、この論理式のままだと扱いにくい場面が多いため、\( a < b \)を「\( b \)は\( a \)にMyNatの正の値を足したものである」という形、つまり\( \exists k : \text{MyNat},\ a + (k + 1) = b \)に書き換えられることを証明しておきます。こうしておくと、後の証明でMyNat側の帰納法や具体的な値の計算がそのまま使えるようになります。
lt.destでは、まずnotation_simpで\( a < b \)の定義を展開し、\( a \le b \)の中身である\( \exists k, a + k = b \)からkを取り出します。もしk=0なら\( a = b \)となってしまい、これは\( \lnot (b \le a) \)という仮定と矛盾するので、kは0ではなく、必ず何かの後者\( k+1 \)の形になっている、という筋道です。逆向きのlt.introでは、証拠となる\( a + (k+1) = b \)から\( a \le b \)を作るのは簡単ですが、\( \lnot (b \le a) \)の証明がやや技巧的で、もし\( b \le a \)だったとすると\( 1 \le 0 \)という矛盾が\( \text{calc} \)ブロックの計算で導かれ、最後はorderタクティクで締めています。
variable {a b c : MyInt}
theorem MyInt.lt.dest (h : a < b) : ∃ k : MyNat, a + (↑k + 1) = b := by
notation_simp at h
-- a b : MyInt
-- h : (∃ k, a + ↑k = b) ∧ ¬∃ k, b + ↑k = a
-- ⊢ ∃ k, a + (↑k + 1) = b
obtain ⟨⟨k, hk⟩, h⟩ := h
-- h : ¬∃ k, b + ↑k = a
-- k : MyNat
-- hk : a + ↑k = b
-- ⊢ ∃ k, a + (↑k + 1) = b
induction k with
| zero =>
exfalso
replace hk : a = b := by simp_all
have : ∃ k : MyNat, b + ↑k = a := by
rw [hk]
exists 0
simp
contradiction
| succ k _ =>
push_cast at hk
use k
assumption
theorem MyInt.le.intro (a : MyInt) (b : MyNat) : a ≤ a + ↑b := by
exact ⟨b, rfl⟩
theorem MyInt.lt.intro (h : ∃ k : MyNat, a + (k + 1) = b) : a < b := by
obtain ⟨k, hk⟩ := h
simp only [lt_def] -- ⊢ a ≤ b ∧ ¬b ≤ a
constructor
case left => -- ⊢ a ≤ b
notation_simp
use k + 1
assumption
case right => -- ⊢ ¬b ≤ a
notation_simp
intro ⟨s, hs⟩
rw [← hs] at hk
-- hk : a + (↑k + 1) = b
-- hs : b + ↑s = a
-- ⊢ a + (↑k + 1) = b
have : ↑(s + k) + (1 : MyInt) = 0 := calc
_ = (↑s + ↑k) + (1 : MyInt) := by push_cast; ac_rfl
_ = (b + ↑s + (↑k + 1)) - b := by abel
_ = b - b := by rw [hk]
_ = 0 := by abel
replace : (0 : MyInt) > 0 := calc
_ = ↑(s + k) + (1 : MyInt) := by rw [this]
_ = (1 : MyInt) + ↑(s + k):= by ac_rfl
_ ≥ (1 : MyInt) := by apply MyInt.le.intro
_ > (0 : MyInt) := by decide
order
theorem MyInt.lt_iff_add : a < b ↔ ∃ k : MyNat, a + (k + 1) = b := by
constructor
case mp => exact MyInt.lt.dest
case mpr => exact MyInt.lt.intro掛け算が狭義順序を保つことの証明
次に\( a < b \land 0 < c \to c \cdot a < c \cdot b \)を示します。まず準備として、MyNatの掛け算がMyIntへのキャストと可換であることを示すofMyNat_mulを@[push_cast]属性付きで登録しておきます。これにより以降の証明でpush_castタクティクがこの等式を自動的に使ってくれるようになります。
mul_posでは、\( 0 < a \)と\( 0 < b \)をそれぞれ先ほどの\( \exists k, \dots \)の形に展開し、\( a = 0 + (c+1) \)、\( b = 0 + (d+1) \)と書き換えたうえで、積の証拠として\( c \cdot d + c + d \)を提示します。あとはpush_castとringで両辺が等しいことを機械的に確認するだけです。sub_posは\( 0 < a - b \leftrightarrow b < a \)という、引き算と大小関係を結びつける補題で、これを使うと\( c \cdot a < c \cdot b \)の証明を「\( 0 < c \cdot (b-a) \)を示せばよい」というmul_posが使える形に帰着できます。
@[push_cast]
theorem MyInt.ofMyNat_mul (m n : MyNat) : ↑(m * n) = (m : MyInt) * (n : MyInt) := by
dsimp [MyInt.ofMyNat]
apply Quotient.sound
notation_simp
ring
theorem MyInt.mul_pos (ha : 0 < a) (hb : 0 < b) : 0 < a * b := by
rw [MyInt.lt_iff_add] at *
obtain ⟨c, hc⟩ := ha
obtain ⟨d, hd⟩ := hb
-- hc : 0 + (↑c + 1) = a
-- hd : 0 + (↑d + 1) = b
-- ⊢ ∃ k, 0 + (↑k + 1) = a * b
rw [← hc, ← hd] -- ⊢ ∃ k, 0 + (↑k + 1) = (0 + (↑c + 1)) * (0 + (↑d + 1))
use c * d + c + d
push_cast
ring
theorem MyInt.sub_pos : 0 < a - b ↔ b < a := by
constructor <;> intro h
· rw [MyInt.lt_iff_add] at *
obtain ⟨k, hk⟩ := h
simp at hk
use k
rw [hk]
abel
· rw [MyInt.lt_iff_add] at *
obtain ⟨k, hk⟩ := h
use k
rw [← hk]
abel
theorem MyInt.mul_lt_mul_of_pos_left (h : a < b) (pos : 0 < c)
: c * a < c * b := by
suffices 0 < c * (b - a) from by
-- h : a < b
-- pos : 0 < c
-- this : 0 < c * (b - a)
-- ⊢ c * a < c * b
rw [MyInt.lt_iff_add] at this ⊢
-- this : ∃ k, 0 + (↑k + 1) = c * (b - a) ⊢ ∃ k, c * a + (↑k + 1) = c * b
obtain ⟨k, hk⟩ := this
simp at hk
use k
rw [hk]
simp [MyInt.left_distrib]
replace h : 0 < b - a := by
rw [MyInt.sub_pos]
assumption
apply MyInt.mul_pos (ha := pos) (hb := h)
theorem MyInt.mul_lt_mul_of_pos_right (h : a < b) (pos : 0 < c)
: a * c < b * c := by
rw [MyInt.mul_comm a c, MyInt.mul_comm b c]
apply MyInt.mul_lt_mul_of_pos_left (h := h) (pos := pos)
instance : IsStrictOrderedRing MyInt where
zero_le_one := by decide
exists_pair_ne := by exists 0, 1
mul_lt_mul_of_pos_left := by
intro a ha b c hbc
exact MyInt.mul_lt_mul_of_pos_left hbc ha
mul_lt_mul_of_pos_right := by
intro c hc a b hab
exact MyInt.mul_lt_mul_of_pos_right hab hc最後にこれらをまとめてIsStrictOrderedRing型クラスに登録します。このクラスは環の演算と狭義順序が整合していることを表すもので、zero_le_one(0と1の大小)やexists_pair_ne(異なる2元が存在すること、つまり自明でない環であること)なども要求されます。
linarithタクティクの利用
順序環として登録できたことで、linarithタクティクが使えるようになります。linarithは、仮定と結論がすべて線形な等式・不等式で表せるとき、それらを組み合わせて矛盾や結論を自動で導いてくれるタクティクです。手で式変形をする必要がなくなるため、非常に強力です。
example (h : a < b) : a + c < b + c := by
linarith
example (h1 : 2 * a - b = 1) (h2 : a + b = 5) : a = 2 := by
linarithただし実際に使ってみると、数値リテラル(2や5など)の扱いでうまくいかないケースがありました。原因は、MyIntのCommRingインスタンスにおいて自然数キャストの後者に関する規則(natCast_succ)が正しく設定されていなかったことにあります。そこでMyInt.ofNatが後者演算と整合することを示すofNat_succを用意し、CommRingインスタンスに明示的に組み込みました。
theorem MyInt.ofNat_succ (n : Nat) : MyInt.ofNat (n + 1) = MyInt.ofNat n + 1 := by
apply Quotient.sound
notation_simp
simp [MyInt.ofNat, MyNat.ofNat]
change (MyNat.ofNat n).succ = MyNat.ofNat n + MyNat.succ 0
exact (MyNat.add_succ (MyNat.ofNat n) 0).symm
instance : CommRing MyInt where
natCast := MyInt.ofNat
natCast_zero := rfl
natCast_succ := MyInt.ofNat_succ掛け算の広義順序とnlinarith
最後に広義順序\( 0 \le c \land a \le b \to c \cdot a \le c \cdot b \)を示します。これはこれまでに証明した狭義順序の性質やその他の環・順序の公理から論理的に導けるのですが、ここでは手で証明を組み立てる代わりにnlinarithタクティクに任せています。nlinarithはlinarithを拡張し、仮定同士の積など簡単な非線形の組み合わせも試したうえで線形な矛盾を探してくれるタクティクで、掛け算が絡む今回のような主張にも直接使えます。
theorem MyInt.mul_le_mul_of_nonneg_left (h : a ≤ b) (nneg: 0 ≤ c)
: c * a ≤ c * b := by
nlinarith
theorem MyInt.mul_le_mul_of_nonneg_right (h : a ≤ b) (nneg: 0 ≤ c)
: a * c ≤ b * c := by
nlinarith
instance : IsOrderedRing MyInt where
zero_le_one := by decide
mul_le_mul_of_nonneg_left := by
intro a ha b c hbc
exact MyInt.mul_le_mul_of_nonneg_left hbc ha
mul_le_mul_of_nonneg_right := by
intro c hc a b hab
exact MyInt.mul_le_mul_of_nonneg_right hab hc
example (h1 : 3 * a - 2 * b = 5) (h2: 6 * a - 5 * b = 11)
: b = -1 := by nlinarithこれでIsOrderedRing型クラスへの登録も完了し、nlinarithだけで非線形な等式・不等式の証明が書けるようになりました。
まとめ
今回はMyIntが全順序であることと、順序環であることを証明し、LinearOrder・IsStrictOrderedRing・IsOrderedRingの3つの型クラスに登録しました。これにより、order・linarith・nlinarithという強力な自動証明タクティクがMyIntに対しても使えるようになっています。教科書にあるgrindタクティクについては本シリーズでは扱いませんが、これで教科書の内容はすべて終了となります。
コードの全体はhttps://github.com/ringring-creator/LearnLeanで公開しています。
0 件のコメント:
コメントを投稿