Lean 1

Lean による定理証明に関する素振り．
vscode上でLeanをインストールすれば，下記のように拡張子が .lean のファイルを開くとvscodeがLeanモードになる．

Leanモードでは，サイドビューに定理証明の状況が表示される．
以下のように証明したい命題を example として定義し，by 以降に証明を書く．このモードを tactic mode という．

この状態で exampleの次の行へカーソルを移動させると，サイドビューに証明の状況が表示され，現在証明すべき命題が ⊢ の右側に表示される．P である．

命題 P の証明 hP があるので，apply hP とすれば証明完了．
サイドビューの Tactic state が変化し，No goals となる．これで証明完了（らしい）．