ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発 › Leanにおける論理

TL;DR

• 命題論理の基本（命題、仮定、含意、否定、同値性、論理積と論理和）を Lean でどう表すかを学ぶ章である。
• それぞれを証明するためのタクティクを一通り紹介している。

内容

節ごとのメモ

この章のまとめは、節ごとに別のページに分けている。

• Lean における命題
• Lean における仮定
• Lean における含意
• Lean における否定
• Lean における同値性
• Lean における論理積 / 論理和

登場したタクティク

この章では次のタクティクが出てくる。

• trivial
• exact
• assumption
• rfl
• apply
• intro
• contradiction
• exfalso
• constructor
• rw
• left
• right
• cases
• case

キーワード

• Lean
• タクティク