Coqメモ

14303 ワード
Coq Coq テキストリンク

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を分解し、証明以外のものにできてしまったら大変である。