1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: ChoiceFacts.v 10756 2008-04-04 17:10:45Z herbelin $ i*)
11
(** Some facts and definitions concerning choice and description in
14
We investigate the relations between the following choice and
15
description principles
17
- AC_rel = relational form of the (non extensional) axiom of choice
18
(a "set-theoretic" axiom of choice)
19
- AC_fun = functional form of the (non extensional) axiom of choice
20
(a "type-theoretic" axiom of choice)
21
- AC! = functional relation reification
22
(known as axiom of unique choice in topos theory,
23
sometimes called principle of definite description in
24
the context of constructive type theory)
26
- GAC_rel = guarded relational form of the (non extensional) axiom of choice
27
- GAC_fun = guarded functional form of the (non extensional) axiom of choice
28
- GAC! = guarded functional relation reification
30
- OAC_rel = "omniscient" relational form of the (non extensional) axiom of choice
31
- OAC_fun = "omniscient" functional form of the (non extensional) axiom of choice
32
(called AC* in Bell [[Bell]])
35
- ID_iota = intuitionistic definite description
36
- ID_epsilon = intuitionistic indefinite description
38
- D_iota = (weakly classical) definite description principle
39
- D_epsilon = (weakly classical) indefinite description principle
41
- PI = proof irrelevance
42
- IGP = independence of general premises
43
(an unconstrained generalisation of the constructive principle of
44
independence of premises)
45
- Drinker = drinker's paradox (small form)
46
(called Ex in Bell [[Bell]])
50
IPL_2 = 2nd-order impredicative minimal predicate logic (with ex. quant.)
51
IPL^2 = 2nd-order functional minimal predicate logic (with ex. quant.)
52
IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal pred. logic (with ex. quant.)
54
with no prerequisite on the non-emptyness of domains
60
2. IPL_2^2 |- AC_rel + AC! = AC_fun
62
3.1. typed IPL_2 + Sigma-types + PI |- AC_rel = GAC_rel and IPL_2 |- AC_rel + IGP -> GAC_rel and IPL_2 |- GAC_rel = OAC_rel
64
3.2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker
66
3.3. D_iota -> ID_iota and D_epsilon <-> ID_epsilon + Drinker
68
4. Derivability of choice for decidable relations with well-ordered codomain
70
5. Equivalence of choices on dependent or non dependent functional types
72
6. Non contradiction of constructive descriptions wrt functional choices
74
7. Definite description transports classical logic to the computational world
78
[[Bell]] John L. Bell, Choice principles in intuitionistic set theory,
81
[[Bell93]] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic
82
Type Theories, Mathematical Logic Quarterly, volume 39, 1993.
84
[Carlstr�m05] Jesper Carlstr�m, Interpreting descriptions in
85
intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
88
Set Implicit Arguments.
90
(**********************************************************************)
93
(** Choice, reification and description schemes *)
95
Section ChoiceSchemes.
101
Variable R:A->B->Prop.
103
(** ** Constructive choice and description *)
107
Definition RelationalChoice_on :=
109
(forall x : A, exists y : B, R x y) ->
110
(exists R' : A->B->Prop, subrelation R' R /\ forall x, exists! y, R' x y).
114
Definition FunctionalChoice_on :=
116
(forall x : A, exists y : B, R x y) ->
117
(exists f : A->B, forall x : A, R x (f x)).
119
(** AC! or Functional Relation Reification (known as Axiom of Unique Choice
120
in topos theory; also called principle of definite description *)
122
Definition FunctionalRelReification_on :=
124
(forall x : A, exists! y : B, R x y) ->
125
(exists f : A->B, forall x : A, R x (f x)).
127
(** ID_epsilon (constructive version of indefinite description;
128
combined with proof-irrelevance, it may be connected to
129
Carlstr�m's type theory with a constructive indefinite description
132
Definition ConstructiveIndefiniteDescription_on :=
134
(exists x, P x) -> { x:A | P x }.
136
(** ID_iota (constructive version of definite description; combined
137
with proof-irrelevance, it may be connected to Carlstr�m's and
138
Stenlund's type theory with a constructive definite description
141
Definition ConstructiveDefiniteDescription_on :=
143
(exists! x, P x) -> { x:A | P x }.
145
(** ** Weakly classical choice and description *)
149
Definition GuardedRelationalChoice_on :=
150
forall P : A->Prop, forall R : A->B->Prop,
151
(forall x : A, P x -> exists y : B, R x y) ->
152
(exists R' : A->B->Prop,
153
subrelation R' R /\ forall x, P x -> exists! y, R' x y).
157
Definition GuardedFunctionalChoice_on :=
158
forall P : A->Prop, forall R : A->B->Prop,
160
(forall x : A, P x -> exists y : B, R x y) ->
161
(exists f : A->B, forall x, P x -> R x (f x)).
165
Definition GuardedFunctionalRelReification_on :=
166
forall P : A->Prop, forall R : A->B->Prop,
168
(forall x : A, P x -> exists! y : B, R x y) ->
169
(exists f : A->B, forall x : A, P x -> R x (f x)).
173
Definition OmniscientRelationalChoice_on :=
174
forall R : A->B->Prop,
175
exists R' : A->B->Prop,
176
subrelation R' R /\ forall x : A, (exists y : B, R x y) -> exists! y, R' x y.
180
Definition OmniscientFunctionalChoice_on :=
181
forall R : A->B->Prop,
183
exists f : A->B, forall x : A, (exists y : B, R x y) -> R x (f x).
187
Definition EpsilonStatement_on :=
189
inhabited A -> { x:A | (exists x, P x) -> P x }.
193
Definition IotaStatement_on :=
195
inhabited A -> { x:A | (exists! x, P x) -> P x }.
199
(** Generalized schemes *)
201
Notation RelationalChoice :=
202
(forall A B, RelationalChoice_on A B).
203
Notation FunctionalChoice :=
204
(forall A B, FunctionalChoice_on A B).
205
Notation FunctionalChoiceOnInhabitedSet :=
206
(forall A B, inhabited B -> FunctionalChoice_on A B).
207
Notation FunctionalRelReification :=
208
(forall A B, FunctionalRelReification_on A B).
210
Notation GuardedRelationalChoice :=
211
(forall A B, GuardedRelationalChoice_on A B).
212
Notation GuardedFunctionalChoice :=
213
(forall A B, GuardedFunctionalChoice_on A B).
214
Notation GuardedFunctionalRelReification :=
215
(forall A B, GuardedFunctionalRelReification_on A B).
217
Notation OmniscientRelationalChoice :=
218
(forall A B, OmniscientRelationalChoice_on A B).
219
Notation OmniscientFunctionalChoice :=
220
(forall A B, OmniscientFunctionalChoice_on A B).
222
Notation ConstructiveDefiniteDescription :=
223
(forall A, ConstructiveDefiniteDescription_on A).
224
Notation ConstructiveIndefiniteDescription :=
225
(forall A, ConstructiveIndefiniteDescription_on A).
227
Notation IotaStatement :=
228
(forall A, IotaStatement_on A).
229
Notation EpsilonStatement :=
230
(forall A, EpsilonStatement_on A).
232
(** Subclassical schemes *)
234
Definition ProofIrrelevance :=
235
forall (A:Prop) (a1 a2:A), a1 = a2.
237
Definition IndependenceOfGeneralPremises :=
238
forall (A:Type) (P:A -> Prop) (Q:Prop),
240
(Q -> exists x, P x) -> exists x, Q -> P x.
242
Definition SmallDrinker'sParadox :=
243
forall (A:Type) (P:A -> Prop), inhabited A ->
244
exists x, (exists x, P x) -> P x.
246
(**********************************************************************)
247
(** * AC_rel + AC! = AC_fun
249
We show that the functional formulation of the axiom of Choice
250
(usual formulation in type theory) is equivalent to its relational
251
formulation (only formulation of set theory) + functional relation
252
reification (aka axiom of unique choice, or, principle of (parametric)
253
definite descriptions) *)
255
(** This shows that the axiom of choice can be assumed (under its
256
relational formulation) without known inconsistency with classical logic,
257
though functional relation reification conflicts with classical logic *)
259
Lemma description_rel_choice_imp_funct_choice :
261
FunctionalRelReification_on A B -> RelationalChoice_on A B -> FunctionalChoice_on A B.
263
intros A B Descr RelCh R H.
264
destruct (RelCh R H) as (R',(HR'R,H0)).
265
destruct (Descr R') as (f,Hf).
268
destruct (H0 x) as (y,(HR'xy,Huniq)).
269
rewrite <- (Huniq (f x) (Hf x)).
270
apply HR'R; assumption.
273
Lemma funct_choice_imp_rel_choice :
274
forall A B, FunctionalChoice_on A B -> RelationalChoice_on A B.
276
intros A B FunCh R H.
277
destruct (FunCh R H) as (f,H0).
278
exists (fun x y => f x = y).
280
intros x y Heq; rewrite <- Heq; trivial.
281
intro x; exists (f x); split.
286
Lemma funct_choice_imp_description :
287
forall A B, FunctionalChoice_on A B -> FunctionalRelReification_on A B.
289
intros A B FunCh R H.
290
destruct (FunCh R) as [f H0].
293
destruct (H x) as (y,(HRxy,_)).
294
exists y; exact HRxy.
299
Corollary FunChoice_Equiv_RelChoice_and_ParamDefinDescr :
300
forall A B, FunctionalChoice_on A B <->
301
RelationalChoice_on A B /\ FunctionalRelReification_on A B.
305
[ exact (funct_choice_imp_rel_choice H)
306
| exact (funct_choice_imp_description H) ].
307
intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H).
310
(**********************************************************************)
311
(** * Connection between the guarded, non guarded and omniscient choices *)
313
(** We show that the guarded formulations of the axiom of choice
314
are equivalent to their "omniscient" variant and comes from the non guarded
315
formulation in presence either of the independance of general premises
316
or subset types (themselves derivable from subtypes thanks to proof-
319
(**********************************************************************)
320
(** ** AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel *)
322
Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice :
323
RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice.
325
intros rel_choice proof_irrel.
326
red in |- *; intros A B P R H.
327
destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as (R',(HR'R,H0)).
329
destruct (H x HPx) as (y,HRxy).
330
exists y; exact HRxy.
331
set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y).
333
intros x y (HPx,HR'xy).
334
change x with (projT1 (existT P x HPx)); apply HR'R; exact HR'xy.
336
destruct (H0 (existT P x HPx)) as (y,(HR'xy,Huniq)).
337
exists y; split. exists HPx; exact HR'xy.
338
intros y' (H'Px,HR'xy').
340
rewrite proof_irrel with (a1 := HPx) (a2 := H'Px); exact HR'xy'.
343
Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice :
344
forall A B, inhabited B -> RelationalChoice_on A B ->
345
IndependenceOfGeneralPremises -> GuardedRelationalChoice_on A B.
347
intros A B Inh AC_rel IndPrem P R H.
348
destruct (AC_rel (fun x y => P x -> R x y)) as (R',(HR'R,H0)).
349
intro x. apply IndPrem. exact Inh. intro Hx.
351
exists (fun x y => P x /\ R' x y).
355
Lemma guarded_rel_choice_imp_rel_choice :
356
forall A B, GuardedRelationalChoice_on A B -> RelationalChoice_on A B.
358
intros A B GAC_rel R H.
359
destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)).
361
exists R'; firstorder.
364
Lemma subset_types_imp_guarded_rel_choice_iff_rel_choice :
365
ProofIrrelevance -> (GuardedRelationalChoice <-> RelationalChoice).
368
guarded_rel_choice_imp_rel_choice,
369
rel_choice_and_proof_irrel_imp_guarded_rel_choice.
372
(** OAC_rel = GAC_rel *)
374
Corollary guarded_iff_omniscient_rel_choice :
375
GuardedRelationalChoice <-> OmniscientRelationalChoice.
378
intros GAC_rel A B R.
379
apply (GAC_rel A B (fun x => exists y, R x y) R); auto.
380
intros OAC_rel A B P R H.
381
destruct (OAC_rel A B R) as (f,Hf); exists f; firstorder.
384
(**********************************************************************)
385
(** ** AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker *)
387
(** AC_fun + IGP = GAC_fun *)
389
Lemma guarded_fun_choice_imp_indep_of_general_premises :
390
GuardedFunctionalChoice -> IndependenceOfGeneralPremises.
392
intros GAC_fun A P Q Inh H.
393
destruct (GAC_fun unit A (fun _ => Q) (fun _ => P) Inh) as (f,Hf).
399
Lemma guarded_fun_choice_imp_fun_choice :
400
GuardedFunctionalChoice -> FunctionalChoiceOnInhabitedSet.
402
intros GAC_fun A B Inh R H.
403
destruct (GAC_fun A B (fun _ => True) R Inh) as (f,Hf).
408
Lemma fun_choice_and_indep_general_prem_imp_guarded_fun_choice :
409
FunctionalChoiceOnInhabitedSet -> IndependenceOfGeneralPremises
410
-> GuardedFunctionalChoice.
412
intros AC_fun IndPrem A B P R Inh H.
413
apply (AC_fun A B Inh (fun x y => P x -> R x y)).
414
intro x; apply IndPrem; eauto.
417
Corollary fun_choice_and_indep_general_prem_iff_guarded_fun_choice :
418
FunctionalChoiceOnInhabitedSet /\ IndependenceOfGeneralPremises
419
<-> GuardedFunctionalChoice.
422
guarded_fun_choice_imp_indep_of_general_premises,
423
guarded_fun_choice_imp_fun_choice,
424
fun_choice_and_indep_general_prem_imp_guarded_fun_choice.
427
(** AC_fun + Drinker = OAC_fun *)
429
(** This was already observed by Bell [[Bell]] *)
431
Lemma omniscient_fun_choice_imp_small_drinker :
432
OmniscientFunctionalChoice -> SmallDrinker'sParadox.
434
intros OAC_fun A P Inh.
435
destruct (OAC_fun unit A (fun _ => P)) as (f,Hf).
437
exists (f tt); firstorder.
440
Lemma omniscient_fun_choice_imp_fun_choice :
441
OmniscientFunctionalChoice -> FunctionalChoiceOnInhabitedSet.
443
intros OAC_fun A B Inh R H.
444
destruct (OAC_fun A B R Inh) as (f,Hf).
445
exists f; firstorder.
448
Lemma fun_choice_and_small_drinker_imp_omniscient_fun_choice :
449
FunctionalChoiceOnInhabitedSet -> SmallDrinker'sParadox
450
-> OmniscientFunctionalChoice.
452
intros AC_fun Drinker A B R Inh.
453
destruct (AC_fun A B Inh (fun x y => (exists y, R x y) -> R x y)) as (f,Hf).
454
intro x; apply (Drinker B (R x) Inh).
455
exists f; assumption.
458
Corollary fun_choice_and_small_drinker_iff_omniscient_fun_choice :
459
FunctionalChoiceOnInhabitedSet /\ SmallDrinker'sParadox
460
<-> OmniscientFunctionalChoice.
463
omniscient_fun_choice_imp_small_drinker,
464
omniscient_fun_choice_imp_fun_choice,
465
fun_choice_and_small_drinker_imp_omniscient_fun_choice.
468
(** OAC_fun = GAC_fun *)
470
(** This is derivable from the intuitionistic equivalence between IGP and Drinker
471
but we give a direct proof *)
473
Theorem guarded_iff_omniscient_fun_choice :
474
GuardedFunctionalChoice <-> OmniscientFunctionalChoice.
477
intros GAC_fun A B R Inh.
478
apply (GAC_fun A B (fun x => exists y, R x y) R); auto.
479
intros OAC_fun A B P R Inh H.
480
destruct (OAC_fun A B R Inh) as (f,Hf).
481
exists f; firstorder.
484
(**********************************************************************)
485
(** ** D_iota -> ID_iota and D_epsilon <-> ID_epsilon + Drinker *)
487
(** D_iota -> ID_iota *)
489
Lemma iota_imp_constructive_definite_description :
490
IotaStatement -> ConstructiveDefiniteDescription.
493
destruct D_iota with (P:=P) as (x,H1).
494
destruct H; red in H; auto.
495
exists x; apply H1; assumption.
498
(** ID_epsilon + Drinker <-> D_epsilon *)
500
Lemma epsilon_imp_constructive_indefinite_description:
501
EpsilonStatement -> ConstructiveIndefiniteDescription.
503
intros D_epsilon A P H.
504
destruct D_epsilon with (P:=P) as (x,H1).
506
exists x; apply H1; assumption.
509
Lemma constructive_indefinite_description_and_small_drinker_imp_epsilon :
510
SmallDrinker'sParadox -> ConstructiveIndefiniteDescription ->
513
intros Drinkers D_epsilon A P Inh;
514
apply D_epsilon; apply Drinkers; assumption.
517
Lemma epsilon_imp_small_drinker :
518
EpsilonStatement -> SmallDrinker'sParadox.
520
intros D_epsilon A P Inh; edestruct D_epsilon; eauto.
523
Theorem constructive_indefinite_description_and_small_drinker_iff_epsilon :
524
(SmallDrinker'sParadox * ConstructiveIndefiniteDescription ->
527
SmallDrinker'sParadox * ConstructiveIndefiniteDescription).
530
epsilon_imp_constructive_indefinite_description,
531
constructive_indefinite_description_and_small_drinker_imp_epsilon,
532
epsilon_imp_small_drinker.
535
(**********************************************************************)
536
(** * Derivability of choice for decidable relations with well-ordered codomain *)
538
(** Countable codomains, such as [nat], can be equipped with a
539
well-order, which implies the existence of a least element on
540
inhabited decidable subsets. As a consequence, the relational form of
541
the axiom of choice is derivable on [nat] for decidable relations.
543
We show instead that functional relation reification and the
544
functional form of the axiom of choice are equivalent on decidable
545
relation with [nat] as codomain
548
Require Import Wf_nat.
549
Require Import Decidable.
551
Definition FunctionalChoice_on_rel (A B:Type) (R:A->B->Prop) :=
552
(forall x:A, exists y : B, R x y) ->
553
exists f : A -> B, (forall x:A, R x (f x)).
555
Lemma classical_denumerable_description_imp_fun_choice :
557
FunctionalRelReification_on A nat ->
558
forall R:A->nat->Prop,
559
(forall x y, decidable (R x y)) -> FunctionalChoice_on_rel R.
562
red in |- *; intros R Rdec H.
563
set (R':= fun x y => R x y /\ forall y', R x y' -> y <= y').
564
destruct (Descr R') as (f,Hf).
566
apply (dec_inh_nat_subset_has_unique_least_element (R x)).
571
destruct (Hf x) as (Hfx,_).
575
(**********************************************************************)
576
(** * Choice on dependent and non dependent function types are equivalent *)
578
(** ** Choice on dependent and non dependent function types are equivalent *)
580
Definition DependentFunctionalChoice_on (A:Type) (B:A -> Type) :=
581
forall R:forall x:A, B x -> Prop,
582
(forall x:A, exists y : B x, R x y) ->
583
(exists f : (forall x:A, B x), forall x:A, R x (f x)).
585
Notation DependentFunctionalChoice :=
586
(forall A (B:A->Type), DependentFunctionalChoice_on B).
590
Theorem dep_non_dep_functional_choice :
591
DependentFunctionalChoice -> FunctionalChoice.
593
intros AC_depfun A B R H.
594
destruct (AC_depfun A (fun _ => B) R H) as (f,Hf).
598
(** Deriving choice on product types requires some computation on
599
singleton propositional types, so we need computational
600
conjunction projections and dependent elimination of conjunction
603
Scheme and_indd := Induction for and Sort Prop.
604
Scheme eq_indd := Induction for eq Sort Prop.
606
Definition proj1_inf (A B:Prop) (p : A/\B) :=
609
Theorem non_dep_dep_functional_choice :
610
FunctionalChoice -> DependentFunctionalChoice.
612
intros AC_fun A B R H.
613
pose (B' := { x:A & B x }).
614
pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)).
615
destruct (AC_fun A B' R') as (f,Hf).
616
intros x. destruct (H x) as (y,Hy).
617
exists (existT (fun x => B x) x y). split; trivial.
618
exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))).
619
intro x; destruct (Hf x) as (Heq,HR) using and_indd.
620
destruct (f x); simpl in *.
621
destruct Heq using eq_indd; trivial.
624
(** ** Reification of dependent and non dependent functional relation are equivalent *)
626
Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) :=
627
forall (R:forall x:A, B x -> Prop),
628
(forall x:A, exists! y : B x, R x y) ->
629
(exists f : (forall x:A, B x), forall x:A, R x (f x)).
631
Notation DependentFunctionalRelReification :=
632
(forall A (B:A->Type), DependentFunctionalRelReification_on B).
636
Theorem dep_non_dep_functional_rel_reification :
637
DependentFunctionalRelReification -> FunctionalRelReification.
639
intros DepFunReify A B R H.
640
destruct (DepFunReify A (fun _ => B) R H) as (f,Hf).
644
(** Deriving choice on product types requires some computation on
645
singleton propositional types, so we need computational
646
conjunction projections and dependent elimination of conjunction
649
Theorem non_dep_dep_functional_rel_reification :
650
FunctionalRelReification -> DependentFunctionalRelReification.
652
intros AC_fun A B R H.
653
pose (B' := { x:A & B x }).
654
pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)).
655
destruct (AC_fun A B' R') as (f,Hf).
656
intros x. destruct (H x) as (y,(Hy,Huni)).
657
exists (existT (fun x => B x) x y). repeat split; trivial.
658
intros (x',y') (Heqx',Hy').
661
rewrite (Huni y'); trivial.
662
exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))).
663
intro x; destruct (Hf x) as (Heq,HR) using and_indd.
664
destruct (f x); simpl in *.
665
destruct Heq using eq_indd; trivial.
668
Corollary dep_iff_non_dep_functional_rel_reification :
669
FunctionalRelReification <-> DependentFunctionalRelReification.
672
non_dep_dep_functional_rel_reification,
673
dep_non_dep_functional_rel_reification.
676
(**********************************************************************)
677
(** * Non contradiction of constructive descriptions wrt functional axioms of choice *)
679
(** ** Non contradiction of indefinite description *)
681
Lemma relative_non_contradiction_of_indefinite_descr :
682
forall C:Prop, (ConstructiveIndefiniteDescription -> C)
683
-> (FunctionalChoice -> C).
686
assert (AC_depfun := non_dep_dep_functional_choice AC_fun).
687
pose (A0 := { A:Type & { P:A->Prop & exists x, P x }}).
688
pose (B0 := fun x:A0 => projT1 x).
689
pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 x) y).
690
pose (H0 := fun x:A0 => projT2 (projT2 x)).
691
destruct (AC_depfun A0 B0 R0 H0) as (f, Hf).
694
exists (f (existT _ A (existT _ P H'))).
695
pose (Hf' := Hf (existT _ A (existT _ P H'))).
699
Lemma constructive_indefinite_descr_fun_choice :
700
ConstructiveIndefiniteDescription -> FunctionalChoice.
702
intros IndefDescr A B R H.
703
exists (fun x => proj1_sig (IndefDescr B (R x) (H x))).
705
apply (proj2_sig (IndefDescr B (R x) (H x))).
708
(** ** Non contradiction of definite description *)
710
Lemma relative_non_contradiction_of_definite_descr :
711
forall C:Prop, (ConstructiveDefiniteDescription -> C)
712
-> (FunctionalRelReification -> C).
715
assert (DepFunReify := non_dep_dep_functional_rel_reification FunReify).
716
pose (A0 := { A:Type & { P:A->Prop & exists! x, P x }}).
717
pose (B0 := fun x:A0 => projT1 x).
718
pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 x) y).
719
pose (H0 := fun x:A0 => projT2 (projT2 x)).
720
destruct (DepFunReify A0 B0 R0 H0) as (f, Hf).
723
exists (f (existT _ A (existT _ P H'))).
724
pose (Hf' := Hf (existT _ A (existT _ P H'))).
728
Lemma constructive_definite_descr_fun_reification :
729
ConstructiveDefiniteDescription -> FunctionalRelReification.
731
intros DefDescr A B R H.
732
exists (fun x => proj1_sig (DefDescr B (R x) (H x))).
734
apply (proj2_sig (DefDescr B (R x) (H x))).
737
(** Remark, the following corollaries morally hold:
739
Definition In_propositional_context (A:Type) := forall C:Prop, (A -> C) -> C.
741
Corollary constructive_definite_descr_in_prop_context_iff_fun_reification :
742
In_propositional_context ConstructiveIndefiniteDescription
743
<-> FunctionalChoice.
745
Corollary constructive_definite_descr_in_prop_context_iff_fun_reification :
746
In_propositional_context ConstructiveDefiniteDescription
747
<-> FunctionalRelReification.
749
but expecting [FunctionalChoice] (resp. [FunctionalRelReification]) to
750
be applied on the same Type universes on both sides of the first
751
(resp. second) equivalence breaks the stratification of universes.
754
(**********************************************************************)
755
(** * Excluded-middle + definite description => computational excluded-middle *)
757
(** The idea for the following proof comes from [[ChicliPottierSimpson02]] *)
759
(** Classical logic and axiom of unique choice (i.e. functional
760
relation reification), as shown in [[ChicliPottierSimpson02]],
761
implies the double-negation of excluded-middle in [Set] (which is
762
incompatible with the impredicativity of [Set]).
764
We adapt the proof to show that constructive definite description
765
transports excluded-middle from [Prop] to [Set].
767
[[ChicliPottierSimpson02]] Laurent Chicli, Lo�c Pottier, Carlos
768
Simpson, Mathematical Quotients and Quotient Types in Coq,
769
Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
772
Require Import Setoid.
774
Theorem constructive_definite_descr_excluded_middle :
775
ConstructiveDefiniteDescription ->
776
(forall P:Prop, P \/ ~ P) -> (forall P:Prop, {P} + {~ P}).
779
pose (select := fun b:bool => if b then P else ~P).
780
assert { b:bool | select b } as ([|],HP).
782
rewrite <- unique_existence; split.
784
exists true; trivial.
785
exists false; trivial.
786
intros [|] [|] H1 H2; simpl in *; reflexivity || contradiction.
791
Corollary fun_reification_descr_computational_excluded_middle_in_prop_context :
792
FunctionalRelReification ->
793
(forall P:Prop, P \/ ~ P) ->
794
forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C.
796
intros FunReify EM C; auto decomp using
797
constructive_definite_descr_excluded_middle,
798
(relative_non_contradiction_of_definite_descr (C:=C)).
added
removed
theories/Logic/ChoiceFacts.v
