CoqのPropについて、メモします。
簡単なSet
Coq.Init.Datatypesに定義されている。
Inductive Empty_set : Set :=.
Inductive unit : Set :=
tt : unit.
Inductive bool : Set :=
| true : bool
| false : bool.
簡単なProp
Coq.Init.Logicで定義されている
Inductive True : Prop :=
I : True.
Inductive False : Prop :=.
簡単なSetと簡単なPropの間の対応
boolに対応するものは、Propには用意されていない？
boolに対応するSetを無理やり作る。
Inductive X:Prop := A|B.
対応を表にすると以下のようになる。
| Set | Prop |
|---|---|
Empty_set : Set |
False : Prop |
unit : Set |
True : Prop |
tt : unit |
I : True |
bool : Set |
X : Prop |
true : bool |
A : X |
false : bool |
B : X |
unitのmatchによる分解
以下はエラーにならない。
Check ( fun x :bool => match x with
| true => Set
| false => Prop
end).
Check ( fun x :bool => match x with
| true => True
| false => False
end
).
Check ( fun x :bool => match x with
| true => A
| false => B
end
).
Xのmatchによる分解
以下はエラーになる。
(* X -> Typeを作ろうとした *)
Check ( fun x :X => match x with
| A => Set
| B => Prop
end).
(* X -> Propを作ろうとした*)
Check ( fun x :X => match x with
| A => True
| B => False
end).
(* X -> Setを作ろうとした*)
Check ( fun x :X => match x with
| A => unit
| B => Empty_set
end
).
(* X -> boolを作ろうとした*)
Check ( fun x :X => match x with
| A => true
| B => false
end
).
以下はエラーにならない。
Check ( fun x :X => match x with
| A => A
| B => B
end
).
Check ( fun x :X => match x with
| A => I
| B => I
end
).
Check ( fun x :X => match x with
| _ => true
end
).
排中律（forall P:Prop, P \/ ~ P）があるとproof irrelevance（forall (P:Prop) (p1 p2:P), p1 = p2）が証明できるらしく、matchでXを分解し、証明以外のものにできてしまったら大変である。