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.Diaconescu</title>
8
<h1>Library Coq.Logic.Diaconescu</h1>
11
<code class="keyword">Section</code> PredExt_GuardRelChoice_imp_EM.<br/>
14
<code class="keyword">Definition</code> <a name="PredicateExtensionality"></a>PredicateExtensionality :=<br/>
15
forall P Q:<a href="Coq.Init.Datatypes.html#bool">bool</a> -> Prop, (forall b:<a href="Coq.Init.Datatypes.html#bool">bool</a>, P b <-> Q b) -> P = Q.<br/>
18
<code class="keyword">Require</code> <code class="keyword">Import</code> ClassicalFacts.<br/>
21
<code class="keyword">Variable</code> pred_extensionality : <a href="Coq.Logic.Diaconescu.html#PredicateExtensionality">PredicateExtensionality</a>.<br/>
23
<code class="keyword">Lemma</code> <a name="prop_ext"></a>prop_ext : forall A B:Prop, (A <-> B) -> A = B.<br/>
24
<code class="keyword">Proof</code>.<br/>
25
intros A B H.<br/>
26
change ((fun _ => A) <a href="Coq.Init.Datatypes.html#true">true</a> = (fun _ => B) <a href="Coq.Init.Datatypes.html#true">true</a>) in |- *.<br/>
27
rewrite<br/>
28
pred_extensionality with (P:= fun _:<a href="Coq.Init.Datatypes.html#bool">bool</a> => A) (Q:= fun _:<a href="Coq.Init.Datatypes.html#bool">bool</a> => B).<br/>
29
reflexivity.<br/>
30
intros _; exact H.<br/>
31
<code class="keyword">Qed</code>.<br/>
34
<code class="keyword">Lemma</code> <a name="proof_irrel"></a>proof_irrel : forall (A:Prop) (a1 a2:A), a1 = a2.<br/>
35
<code class="keyword">Proof</code>.<br/>
36
apply (<a href="Coq.Logic.ClassicalFacts.html#ext_prop_dep_proof_irrel_cic">ext_prop_dep_proof_irrel_cic</a> <a href="Coq.Logic.Diaconescu.html#prop_ext">prop_ext</a>).<br/>
37
<code class="keyword">Qed</code>.<br/>
40
<code class="keyword">Require</code> <code class="keyword">Import</code> ChoiceFacts.<br/>
43
<code class="keyword">Variable</code> rel_choice : <a href="Coq.Logic.ChoiceFacts.html#RelationalChoice">RelationalChoice</a>.<br/>
46
<code class="keyword">Lemma</code> <a name="guarded_rel_choice"></a>guarded_rel_choice :<br/>
47
forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop),<br/>
48
(forall x:A, P x -> exists y : B, R x y) -><br/>
49
exists R' : A -> B -> Prop,<br/>
50
(forall x:A,<br/>
51
P x -><br/>
52
exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).<br/>
53
<code class="keyword">Proof</code>.<br/>
54
exact<br/>
55
(<a href="Coq.Logic.ChoiceFacts.html#rel_choice_and_proof_irrel_imp_guarded_rel_choice">rel_choice_and_proof_irrel_imp_guarded_rel_choice</a> rel_choice <a href="Coq.Logic.Diaconescu.html#proof_irrel">proof_irrel</a>).<br/>
56
<code class="keyword">Qed</code>.<br/>
59
<code class="keyword">Require</code> <code class="keyword">Import</code> Bool.<br/>
62
<code class="keyword">Lemma</code> <a name="AC"></a>AC :<br/>
63
exists R : (<a href="Coq.Init.Datatypes.html#bool">bool</a> -> Prop) -> <a href="Coq.Init.Datatypes.html#bool">bool</a> -> Prop,<br/>
64
(forall P:<a href="Coq.Init.Datatypes.html#bool">bool</a> -> Prop,<br/>
65
(exists b : <a href="Coq.Init.Datatypes.html#bool">bool</a>, P b) -><br/>
66
exists b : <a href="Coq.Init.Datatypes.html#bool">bool</a>, P b /\ R P b /\ (forall b':<a href="Coq.Init.Datatypes.html#bool">bool</a>, R P b' -> b = b')).<br/>
67
<code class="keyword">Proof</code>.<br/>
68
apply <a href="Coq.Logic.Diaconescu.html#guarded_rel_choice">guarded_rel_choice</a> with<br/>
69
(P:= fun Q:<a href="Coq.Init.Datatypes.html#bool">bool</a> -> Prop => exists y : _, Q y)<br/>
70
(R:= fun (Q:<a href="Coq.Init.Datatypes.html#bool">bool</a> -> Prop) (y:<a href="Coq.Init.Datatypes.html#bool">bool</a>) => Q y).<br/>
71
exact (fun _ H => H).<br/>
72
<code class="keyword">Qed</code>.<br/>
75
<code class="keyword">Theorem</code> <a name="pred_ext_and_rel_choice_imp_EM"></a>pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P.<br/>
76
<code class="keyword">Proof</code>.<br/>
80
destruct <a href="Coq.Logic.Diaconescu.html#AC">AC</a> as [R H].<br/>
83
set (class_of_true:= fun b => b = <a href="Coq.Init.Datatypes.html#true">true</a> \/ P).<br/>
84
set (class_of_false:= fun b => b = <a href="Coq.Init.Datatypes.html#false">false</a> \/ P).<br/>
87
destruct (H class_of_true) as [b0 [H0 [H0' H0'']]].<br/>
88
exists <a href="Coq.Init.Datatypes.html#true">true</a>; left; reflexivity.<br/>
92
destruct (H class_of_false) as [b1 [H1 [H1' H1'']]].<br/>
93
exists <a href="Coq.Init.Datatypes.html#false">false</a>; left; reflexivity.<br/>
99
assert (Hequiv : forall b:<a href="Coq.Init.Datatypes.html#bool">bool</a>, class_of_true b <-> class_of_false b).<br/>
101
unfold class_of_false in |- *; right; assumption.<br/>
102
unfold class_of_true in |- *; right; assumption.<br/>
103
assert (Heq : class_of_true = class_of_false).<br/>
104
apply pred_extensionality with (1 := Hequiv).<br/>
105
apply <a href="Coq.Bool.Bool.html#diff_true_false">diff_true_false</a>.<br/>
106
rewrite <- H0.<br/>
107
rewrite <- H1.<br/>
108
rewrite <- H0''. reflexivity.<br/>
113
left; assumption.<br/>
114
left; assumption.<br/>
117
<code class="keyword">Qed</code>.<br/>
120
<code class="keyword">End</code> PredExt_GuardRelChoice_imp_EM.<br/>
122
<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.Diaconescu.html
