Mathlib でよく使う証明パターン¶
Mathlib を使う証明では，まず既存の補題を探し，rw，simp，exact，apply，ext などで組み合わせます．
型クラスによって定理が一般化されているため，具体的な型ではなく一般的な構造に対する定理を使うことが多くあります．
ここでは，Core Lean だけで進めた前章から一歩進んで，Mathlib を import した環境でよく使う補助 tactic も扱います．
by_contra，push Not，nth_rw，conv_lhs，aesop，norm_num，linarith，nlinarith，positivity，gcongr，#loogle などは，実用上よく使われますが，Core Lean だけの最小環境では使えないものがあります．
ただし，基本的な見方は前章と同じです．
rw は Eq や Iff の証明項を使った書き換え，ext は外延性補題の適用，norm_num や linarith は数値・不等式の証明項を自動生成する tactic として読むと，Mathlib の証明も追いやすくなります．
example (A B : Set Nat) (x : Nat) : x ∈ A ∩ B ↔ x ∈ A ∧ x ∈ B := by
exact Set.mem_inter_iff x A B
example (A B : Set Nat) (x : Nat) : x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B := by
exact Set.mem_union x A B
example (a b c : Nat) : a + b + c = a + (b + c) := by
rw [Nat.add_assoc]
example (a b : Nat) : a + b = b + a := by
simpa using Nat.add_comm a b
simpa using ... は，既存の補題の形とゴールが少し違うときに便利です．
補題とゴールの両方を simp で正規化して一致させます．
Mathlib の証明では，既存補題を exact でそのまま使うより，simpa using で少し形を整えて使う場面がよくあります．
norm_num: 数値計算¶
norm_num は，具体的な数値等式・不等式を証明する tactic です．
自然数だけでなく，整数，有理数，実数の数値計算にも使えます．
example : (3 : ℤ) + 4 = 7 := by
norm_num
example : (3 : ℚ) / 2 + 1 / 2 = 2 := by
norm_num
example : (3 : ℝ) ^ 2 + 4 ^ 2 = 25 := by
norm_num
by_contra と push Not¶
by_contra h は背理法の tactic です．
ゴール P を証明するかわりに h : ¬ P を仮定し，ゴールを False に変えます．
Core Lean では Classical.byContradiction を直接使えますが，Mathlib を使う実際の証明では by_contra がよく使われます．
push Not は，否定を量化子や論理結合子の内側へ押し込む tactic です．
たとえば古典論理のもとで，¬ ∀ x, P x は ∃ x, ¬ P x に変形されます．
演習¶
by_contra と push Not を使って，古典論理の証明を書いてください．
example (P : Prop) (h : ¬¬ P) : P := by
-- 解答例:
-- by_contra hP
-- exact h hP
sorry
example (P : Nat → Prop) (h : ¬ ∀ n, P n) : ∃ n, ¬ P n := by
-- 解答例:
-- push Not at h
-- exact h
sorry
nth_rw と conv_lhs¶
rw は通常，該当する箇所をまとめて書き換えます．
一部だけを書き換えたいときには，nth_rw や conv モードを使います．
nth_rw 1 [h] は，1 番目に現れる該当箇所だけを書き換えます．
conv_lhs は，等式の左辺に入って書き換えるための短い notation です．
Core Lean の conv => lhs と同じ発想ですが，短く書けるため実用上よく使われます．
演習¶
nth_rw または conv_lhs を使って，ゴールの一部だけを書き換えてください．
example (a b c : Nat) (h : a + b = c) :
(a + b) + (a + b) = c + (a + b) := by
-- 解答例:
-- nth_rw 1 [h]
sorry
example (a b c : Nat) : (a + b) + c = (b + a) + c := by
-- 解答例:
-- conv_lhs =>
-- rw [Nat.add_comm a b]
sorry
aesop¶
aesop は，論理規則や登録された補題を使って探索する自動証明 tactic です．
命題論理，単純な述語論理，コンストラクタによる証明に強く，短い補助目標を閉じるときに便利です．
example (P Q R : Prop) (hPQ : P → Q) (hQR : Q → R) (hP : P) : R := by
aesop
example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
aesop
演習¶
aesop で閉じる論理問題を作り，手動証明と比較してください．
検索支援: exact?，rw?，#loogle¶
exact?，rw?，try? は，現在のゴールを閉じる候補や書き換え候補を提案します．
出力は Lean や Mathlib のバージョンによって変わることがあるため，ここでは実行例として示します．
example (n : Nat) : n + 0 = n := by
exact?
example (a b : Nat) : a + b = b + a := by
rw?
example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
try?
#loogle は，式の形やキーワードから Mathlib の定理を探すためのコマンドです．
環境によっては Loogle サーバへの接続が必要です．