1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: Diaconescu.v 6401 2004-12-05 16:44:57Z herbelin $ i*)
(** R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory
entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner]
adapted the proof to show that the axiom of choice in equivalence
classes entails Excluded-Middle in Type Theory.
This is an adaptatation of the proof by Hugo Herbelin to show that
the relational form of the Axiom of Choice + Extensionality for
predicates entails Excluded-Middle
[Diaconescu] R. Diaconescu, Axiom of Choice and Complementation, in
Proceedings of AMS, vol 51, pp 176-178, 1975.
[LacasWerner] S. Lacas, B Werner, Which Choices imply the excluded middle?,
preprint, 1999.
*)
Section PredExt_GuardRelChoice_imp_EM.
(** The axiom of extensionality for predicates *)
Definition PredicateExtensionality :=
forall P Q:bool -> Prop, (forall b:bool, P b <-> Q b) -> P = Q.
(** From predicate extensionality we get propositional extensionality
hence proof-irrelevance *)
Require Import ClassicalFacts.
Variable pred_extensionality : PredicateExtensionality.
Lemma prop_ext : forall A B:Prop, (A <-> B) -> A = B.
Proof.
intros A B H.
change ((fun _ => A) true = (fun _ => B) true) in |- *.
rewrite
pred_extensionality with (P := fun _:bool => A) (Q := fun _:bool => B).
reflexivity.
intros _; exact H.
Qed.
Lemma proof_irrel : forall (A:Prop) (a1 a2:A), a1 = a2.
Proof.
apply (ext_prop_dep_proof_irrel_cic prop_ext).
Qed.
(** From proof-irrelevance and relational choice, we get guarded
relational choice *)
Require Import ChoiceFacts.
Variable rel_choice : forall A B:Type, RelationalChoice A B.
Lemma guarded_rel_choice :
forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop),
(forall x:A, P x -> exists y : B, R x y) ->
exists R' : A -> B -> Prop,
(forall x:A,
P x ->
exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
Proof.
apply
(rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
Qed.
(** The form of choice we need: there is a functional relation which chooses
an element in any non empty subset of bool *)
Require Import Bool.
Lemma AC :
exists R : (bool -> Prop) -> bool -> Prop,
(forall P:bool -> Prop,
(exists b : bool, P b) ->
exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')).
Proof.
apply guarded_rel_choice with
(P := fun Q:bool -> Prop => exists y : _, Q y)
(R := fun (Q:bool -> Prop) (y:bool) => Q y).
exact (fun _ H => H).
Qed.
(** The proof of the excluded middle *)
(** Remark: P could have been in Set or Type *)
Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P.
Proof.
intro P.
(** first we exhibit the choice functional relation R *)
destruct AC as [R H].
set (class_of_true := fun b => b = true \/ P).
set (class_of_false := fun b => b = false \/ P).
(** the actual "decision": is (R class_of_true) = true or false? *)
destruct (H class_of_true) as [b0 [H0 [H0' H0'']]].
exists true; left; reflexivity.
destruct H0.
(** the actual "decision": is (R class_of_false) = true or false? *)
destruct (H class_of_false) as [b1 [H1 [H1' H1'']]].
exists false; left; reflexivity.
destruct H1.
(** case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *)
right.
intro HP.
assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b).
intro b; split.
unfold class_of_false in |- *; right; assumption.
unfold class_of_true in |- *; right; assumption.
assert (Heq : class_of_true = class_of_false).
apply pred_extensionality with (1 := Hequiv).
apply diff_true_false.
rewrite <- H0.
rewrite <- H1.
rewrite <- H0''. reflexivity.
rewrite Heq.
assumption.
(** cases where P is true *)
left; assumption.
left; assumption.
Qed.
End PredExt_GuardRelChoice_imp_EM.
|
