Chapter 03: tactic を用いた証明¶
この章では，Lean で証明を書くための基本的な道具を整理します．
前章までに，命題，型，定義，関数型・依存関数型，structure，inductive 型，class などを見ました．
ここでは，それらの型の項として証明を構成する方法に焦点を当てます．
Lean では命題は型であり，証明はその型の項です．
したがって，「証明する」とは，まずは fun，constructor，関数適用，Eq.refl などを使って証明項を構成することです．
by ... による tactic モードは，その証明項をゴールの変化を見ながら組み立てるための書き方です．
特に次の内容を扱います．
- 証明項としての証明
fun，constructor，関数適用，Eq.reflsorryと未完成の証明項byと tactic モードの読み方- tactic と証明項の対応
exact，assumption，rfl，show，change，dsimpapply，intro，specializehave，sufficesrw，simp，simpacalcモードconstructor，obtain，rintro，left，right，match，cases，rcasesinductioncongr，ext，funextby_cases，Classical.byContradiction，exfalso，contradictiondecide，grind#check，exact?，rw?などの検索支援convモード- Lean における等号の証明パターン
- 命題外延性，選択，商，Lean の追加原理
ring，nlinarith，linarith などの代数・不等式向け tactic は，次章の Mathlib を使う証明で扱います．