"Mathematics In Lean"に沿ってLean4の証明支援系の勉強を進めています。まだ基本編で、今やっているのはmin, maxの性質の証明です。具体的には全順序集合上の関数min a b （a, bの小さい方を返す）について次の性質の証明です。
min a (min b c) = min (min a b) c
直感的には結局両辺ともa,b,cのうち最小の値を返しますから等しくなるのは納得です。一方この学習では以下の４つの性質だけから上記の性質を示すことが課題です。
le_antisymm : a $\le$ b $\land$ b $\le$ a $\iff$ a=b
min_le_left a b : min a b $\le$ a
min_le_right a b : min a b $\le$ b
le_min : c $\le$ a $\implies$ c $\le$ b $\implies$ c $\le$ min a b
「適当に」やってみるとうまくいきません。なぜかといえば、、、答えのファイルをチラ見してみると20行くらいありました。適当に組み合わせてみても正しい20行を作り出すのは無理ですね。
というかまず正しい証明を自分で作ってからそれを形式証明に落とすようにするのが正しい手順です。Natural Number Gameでは数行のタクティクの組み合わせでしたので、ゲーム感覚でウェポンを繰り出していたのですが、ここではもう少しちゃんとやってみる必要があります。
以下はまず自分で考えた証明です。
証明したい事柄：min a (min b c)=min (min a b) c
補題１：min a (min b c)$\le$a,b,c (不等号はa,b,cいずれについても成り立つ)
証明：min a (min b c)$\le$aはmin_le_leftから自明。
またmin a (min b c)$\le$min b c $\le$b,c◼️
補題２：min (min a b) c$\le$a,b,c
証明：min (min a b) c$\le$cはmin_le_rightから自明。
またmin (min a b) c$\le$min a b$\le$a,b◼️
補題３：min (min a b) c$\le$min b cおよびmin a (min b c)$\le$min a b
証明：前半はmin (min a b) c $\le$ bとmin (min a b) c$\le$ cが補題２から証明済みなので、le_minから従う。後半はmin a (min b c)$\le$ aとmin a (min b c)$\le$ bが補題１で証明済みなのでle_minから従う。
補題４：min(min(a,b),c)$\le$min(a,min(b,c))
証明：min(min(a,b),c)$\le$a, min(b,c)が言えれば良いが最初の不等式は補題２で証明済み。２つ目の不等式は補題３で証明済み。
補題５：min(a,min(b,c))<=min(min(a,b),c)
証明：min(a,min(b,c))$\le$min(a,b), cが言えれば良いが、最初の不等式は補題３で証明済み。２つ目の不等式は補題１で証明済み。
補題４、５とle_antisymmより
min(a,min(b,c))=min(min(a,b),c)
QED.
このように証明できることが分かれば形式的な証明を書き下すことができます。上記の日本語の証明と下のLean4による形式証明はきちんと対応しています。haveはその環境で成立する補題を導入するものです。ただしsorryと書いてあるところはさらに証明を埋めなければなりません。
example : min (min a b) c = min a (min b c) := by
have lemma1a : min a (min b c) ≤ a := by apply min_le_left
have lemma1b : min a (min b c) ≤ b := by sorry
have lemma1c : min a (min b c) ≤ c := by sorry
have lemma2a : min (min a b) c ≤ a := by sorry
have lemma2b : min (min a b) c ≤ b := by sorry
have lemma2c : min (min a b) c ≤ c := by apply min_le_right
have lemma3bc : min (min a b) c ≤ min b c := by
apply le_min lemma2b lemma2c
have lemma3ab : min a (min b c) ≤ min a b := by
apply le_min lemma1a lemma1b
have lemma4 : min (min a b) c ≤ min a (min b c) := by
apply le_min
apply lemma2a
apply lemma3bchave lemma5 : min a (min b c) ≤ min (min a b) c := by
apply le_min
apply lemma3ab
apply lemma1c
apply le_antisymm
apply lemma4
apply lemma5
未証明の補題lemma1b,1c,2b,2cはapplyやrwタクティクではうまくいきませんでした。apply?というコマンドを使って候補となるタクティクとその結果を検索してみると、1b, 1cでは
refine min_le_of_right_le ?_
というタクティクがお勧めであることがわかります。2b, 2cも同じようなタクティクがお勧めされます。あとはゲーム感覚で進めば証明を完了することができました！
