Why not login to Qiita and try out its useful features?

We'll deliver articles that match you.

You can read useful information later.

2
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

Coqメモ

Last updated at Posted at 2019-08-05

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

2
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up

Qiita Conference 2025 will be held!: 4/23(wed) - 4/25(Fri)

Qiita Conference is the largest tech conference in Qiita!

Keynote Speaker

ymrl、Masanobu Naruse, Takeshi Kano, Junichi Ito, uhyo, Hiroshi Tokumaru, MinoDriven, Minorun, Hiroyuki Sakuraba, tenntenn, drken, konifar

View event details
2
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?