LeanのProp

Propは非可述的(impredicative)

Propは命題宇宙

LeanのPropはproof-irrelevance(証明無関係)というものになる

code:lean

#check And -- Prop → Prop → Prop

#check Or -- Prop → Prop → Prop

#check Not -- Prop → Prop

#check Implies -- Prop → Prop → Prop

variable (p q r : Prop)

#check And p q -- Prop

#check Or (And p q) r -- Prop

#check Implies (And p q) (And q p) -- Prop

Bool, Propの違い

Bool と Prop の違い

どちらも言明に対応するため、Bool と似ているようですが以下のような目立つ相違点があります：

1. Prop の項はそれ自身が型であるため、Prop は型宇宙であると言われます。Bool の項は型ではありません。

2. Prop の項は True か False のどちらであるかを判定するアルゴリズムがあるとは限りません。Bool の項は簡約すれば必ず true か false になります。

確認用

Q. LeanのProp

参考