Lean 3

Lean による定理証明に関する素振り．
今回は次の命題を証明する．

命題 P → R を証明するための仮定として h : P → Q と，h' : Q → R が与えられているが，命題 P の証明は仮定として与えられていない．
この状態で h' : Q → R を適用すると，

このようなエラー表示が出てしまい，証明が進まない．

命題 P の証明が足りていないので，intro を使って apply h' より前に仮定を追加する．

intro (hP : P) は intro hP だけでもよい（Leanが忖度してくれる）．

続けて順に仮定を適用することで

No goals となる．これで証明完了．

なお，短く書くと次のようにも書ける．

example (h : P → Q) (h' : Q → R) : P → R := by
  intro hP
  apply h' (h hP)