1
<html xmlns="http://www.w3.org/1999/xhtml">
3
<meta http-equiv="Content-Type" content="text/html; charset="><link rel="stylesheet" href="style.css" type="text/css"><title>Coq.Logic.ClassicalDescription</title>
8
<h1>Library Coq.Logic.ClassicalDescription</h1>
13
<table width="100%"><tr class="doc"><td>
14
This file provides classical logic and definite description
21
<table width="100%"><tr class="doc"><td>
22
Classical logic and definite description, as shown in <code>1</code>,
23
implies the double-negation of excluded-middle in Set, hence it
24
implies a strongly classical world. Especially it conflicts with
25
impredicativity of Set, knowing that true<>false in Set.
28
<code>1</code> Laurent Chicli, Lo�c Pottier, Carlos Simpson, Mathematical
29
Quotients and Quotient Types in Coq, Proceedings of TYPES 2002,
30
Lecture Notes in Computer Science 2646, Springer Verlag.
36
<code class="keyword">Require</code> <code class="keyword">Export</code> <a href="Coq.Logic.Classical.html">Classical</a>.<br/>
39
<code class="keyword">Axiom</code><br/>
40
<a name="dependent_description"></a>dependent_description :<br/>
41
forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),<br/>
42
(forall x:A,<br/>
43
exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) -><br/>
44
exists f : forall x:A, B x, (forall x:A, R x (f x)).<br/>
49
<table width="100%"><tr class="doc"><td>
50
Principle of definite descriptions (aka axiom of unique choice)
55
<code class="keyword">Theorem</code> <a name="description"></a>description :<br/>
56
forall (A B:Type) (R:A -> B -> Prop),<br/>
57
(forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) -><br/>
58
exists f : A -> B, (forall x:A, R x (f x)).<br/>
59
<code class="keyword">Proof</code>.<br/>
61
apply (<a href="Coq.Logic.ClassicalDescription.html#dependent_description">dependent_description</a> A (fun _ => B)).<br/>
62
<code class="keyword">Qed</code>.<br/>
67
<table width="100%"><tr class="doc"><td>
68
The followig proof comes from <code>1</code>
73
<code class="keyword">Theorem</code> <a name="classic_set"></a>classic_set : ((forall P:Prop, {P} + {~ P}) -> <a href="Coq.Init.Logic.html#False">False</a>) -> <a href="Coq.Init.Logic.html#False">False</a>.<br/>
74
<code class="keyword">Proof</code>.<br/>
76
set (R:= fun A b => A /\ <a href="Coq.Init.Datatypes.html#true">true</a> = b \/ ~ A /\ <a href="Coq.Init.Datatypes.html#false">false</a> = b).<br/>
77
assert (H : exists f : Prop -> <a href="Coq.Init.Datatypes.html#bool">bool</a>, (forall A:Prop, R A (f A))).<br/>
78
apply <a href="Coq.Logic.ClassicalDescription.html#description">description</a>.<br/>
80
destruct (<a href="Coq.Logic.Classical_Prop.html#classic">classic</a> A) as [Ha| Hnota].<br/>
81
exists <a href="Coq.Init.Datatypes.html#true">true</a>; split.<br/>
82
left; split; [ assumption | reflexivity ].<br/>
83
intros y [[_ Hy]| [Hna _]].<br/>
84
assumption.<br/>
85
contradiction.<br/>
86
exists <a href="Coq.Init.Datatypes.html#false">false</a>; split.<br/>
87
right; split; [ assumption | reflexivity ].<br/>
88
intros y [[Ha _]| [_ Hy]].<br/>
89
contradiction.<br/>
90
assumption.<br/>
91
destruct H as [f Hf].<br/>
94
assert (HfP:= Hf P).<br/>
96
left.<br/>
97
destruct HfP as [[Ha _]| [_ Hfalse]].<br/>
98
assumption.<br/>
99
discriminate.<br/>
100
right.<br/>
101
destruct HfP as [[_ Hfalse]| [Hna _]].<br/>
102
discriminate.<br/>
103
assumption.<br/>
104
<code class="keyword">Qed</code>.<br/>
107
<hr/><a href="index.html">Index</a><hr/><font size="-1">This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a></font>
b'\\ No newline at end of file'
added
removed
library/Coq.Logic.ClassicalDescription.html
