More than 5 years have passed since last update.
CoqのPropについて、メモします。
簡単なSet
Coq.Init.Datatypesに定義されている。
InductiveEmpty_set:Set:=.Inductiveunit:Set:=tt:unit.Inductivebool:Set:=|true:bool|false:bool.簡単なProp
Coq.Init.Logicで定義されている
InductiveTrue:Prop:=I:True.InductiveFalse:Prop:=.簡単なSetと簡単なPropの間の対応
boolに対応するものは、Propには用意されていない？
boolに対応するSetを無理やり作る。
InductiveX: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(funx:bool=>matchxwith|true=>Set|false=>Propend).Check(funx:bool=>matchxwith|true=>True|false=>Falseend).Check(funx:bool=>matchxwith|true=>A|false=>Bend).Xのmatchによる分解
以下はエラーになる。
(* X -> Typeを作ろうとした *)Check(funx:X=>matchxwith|A=>Set|B=>Propend).(* X -> Propを作ろうとした*)Check(funx:X=>matchxwith|A=>True|B=>Falseend).(* X -> Setを作ろうとした*)Check(funx:X=>matchxwith|A=>unit|B=>Empty_setend).(* X -> boolを作ろうとした*)Check(funx:X=>matchxwith|A=>true|B=>falseend).以下はエラーにならない。
Check(funx:X=>matchxwith|A=>A|B=>Bend).Check(funx:X=>matchxwith|A=>I|B=>Iend).Check(funx:X=>matchxwith|_=>trueend).排中律（forall P:Prop, P \/ ~ P）があるとproof irrelevance（forall (P:Prop) (p1 p2:P), p1 = p2）が証明できるらしく、matchでXを分解し、証明以外のものにできてしまったら大変である。
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme