Lean

• 注: natural-number-nameで学んだ内容を元に書いてます

Tactics §

rfl §

• $A=A$を証明する
• reflexivity (反射律) の略

rw §

• rw [h]は与式に仮定$h$を代入する (substitute in)
• hは仮定を意味するhypothesisの頭文字から
• rewrite (書き換え) の略
• e.g. 与式$2y=2(x+1)$, 仮定$h:y=x+1$のとき, rw [h]を実行すると与式は$2(x+1)=2(x)$になる

Theorems (仮定) §

one_eq_succ_zero §

• 1 = succ 0を表す
• succ 0とは0の次の自然数, つまり1のことである
• oneとzeroは任意の自然数に書き換え可能

add_zero x §

• x + 0 = x
• 引数を省略した場合は? + 0 = ?
• repeat