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

TL;DR

• Lean では命題を Prop 型で表す。真である命題 True と偽である命題 False は、どちらも Prop の項である。
• True は trivial タクティクで無条件に証明できる。

内容

命題とは、真偽が定まる主張である。たとえば「すべての自然数 $n$ について $n\ge 0$ が成り立つ」は命題である。一方、自由変数を含むものは述語になる。たとえば「自然数 $n$ について $n+3=39$ が成り立つ」は、$n$ が決まるまで真偽が定まらない。

Lean では命題を Prop 型で表す。真である命題は True、偽である命題は False で、どちらも Prop の項である。True は無条件に証明できる。

example : True := by trivial

trivial タクティクは、ゴールが自明であることを示す。事前に登録された複数のタクティクを順に試してくれる。

キーワード

• Lean
• タクティク