by と tactic モードの基本¶
by 以降に tactic を並べる書き方を tactic モードと呼びます．
Lean は現在のゴールを持っていて，各 tactic はそのゴールを変形したり閉じたりします．
VS Code の Infoview では，上側にローカルコンテキスト，下側に現在のゴールが表示されます．
tactic を 1 行実行するたびに，Lean は未解決のゴールを更新します．
すべてのゴールが閉じると，by ... 全体が証明項になります．
ここでいう tactic は，Lean のカーネルが直接持っている推論規則そのものではありません． tactic は，elaboration の途中で実行され，ゴールを操作しながら証明項を構成するためのプログラムです． 完成した証明項は，最後に Lean のカーネルによって型検査されます． この章では tactic の使い方に集中し，elaboration やカーネルの詳しい仕組みは Chapter 06 で扱います．
by は，example ... := by や theorem ... := by の直後だけに現れる特別な記号ではありません．
Lean がある場所で型 T の項を期待しているとき，そこに
と書くと，Lean は「型 T の項を tactic で作る」モードに入ります．
特に T : Prop のとき，これは「その場所で必要な証明を tactic で作る」という意味です．
一番直接的な tactic は exact です．
ゴールと同じ型をもつ項や証明をすでに持っているとき，それを exact に渡します．
厳密には，ゴールの型と exact に渡す項の型が定義的に等しいときに使えます．
assumption は，ローカルコンテキストの中からゴールと一致する仮定を探して使います．
rfl は，両辺が定義を展開すれば同じになる等式を閉じます．
「計算すれば同じ」という等式によく使います．
Lean の等式 a = b は Eq a b という型です．
rfl は Eq.refl，つまり反射律を使う tactic です．
反射律は本来 a = a を証明するものですが，Lean は両辺を計算・定義展開して同じ式になる場合にも rfl を受け入れます．
このように，計算や定義展開だけで同じと判定されることを「定義的に等しい（definitionally equal）」と言います．
#check Eq
#check Eq.refl
example : Eq 3 3 := by
rfl
example : (fun n : Nat => n + 1) 2 = 3 := by
exact Eq.refl 3
一方，数学的には正しい等式でも，定義的に等しくない場合は rfl では閉じません．
たとえば a + b = b + a は可換性の定理 Nat.add_comm を使って証明します．
このような「命題として証明された等式」は，rw などで書き換えに使います．
example (a b : Nat) : a + b = b + a := by
exact Nat.add_comm a b
def Positive (n : Nat) : Prop :=
0 < n
show は，現在のゴールを明示的に書く tactic です．
証明を読む人に「いま何を示しているか」を示すのに使えます．
show で書いた命題は，現在のゴールと定義的に同じでなければなりません．
change は，現在のゴールを定義的に等しい別の表示へ置き換える tactic です．
次の例では，Positive 3 を定義通り 0 < 3 に変えています．
論理的に同値な任意の命題へ変えられるわけではありません．
unfold も定義を展開します．
特定の名前を明示的に展開したいときに使います．
dsimp は definitional simplification の略で，定義を展開して計算で簡約できる部分を整理します．
MiL では，関数を値に適用した式や，定義の中に隠れている全称量化を見やすくする場面で使われます．
simp と違って，一般の補題による書き換えではなく，主に定義展開と計算による簡約を行います．