summaryrefslogtreecommitdiff
path: root/theories/Logic
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /theories/Logic
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'theories/Logic')
-rw-r--r--theories/Logic/ChoiceFacts.v712
-rw-r--r--theories/Logic/ClassicalChoice.v38
-rw-r--r--theories/Logic/ClassicalDescription.v124
-rw-r--r--theories/Logic/ClassicalEpsilon.v90
-rw-r--r--theories/Logic/ClassicalFacts.v3
-rw-r--r--theories/Logic/ClassicalUniqueChoice.v79
-rw-r--r--theories/Logic/Classical_Prop.v11
-rw-r--r--theories/Logic/DecidableType.v156
-rw-r--r--theories/Logic/DecidableTypeEx.v50
-rw-r--r--theories/Logic/Diaconescu.v222
-rw-r--r--theories/Logic/RelationalChoice.v15
11 files changed, 1289 insertions, 211 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index bc892ca9..e0be9ed3 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,155 +7,453 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ChoiceFacts.v 8132 2006-03-05 10:59:47Z herbelin $ i*)
+(*i $Id: ChoiceFacts.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
-(** We show that the functional formulation of the axiom of Choice
- (usual formulation in type theory) is equivalent to its relational
- formulation (only formulation of set theory) + the axiom of
- (parametric) definite description (aka axiom of unique choice) *)
+(** ** Some facts and definitions concerning choice and description in
+ intuitionistic logic.
-(** This shows that the axiom of choice can be assumed (under its
- relational formulation) without known inconsistency with classical logic,
- though definite description conflicts with classical logic *)
+We investigate the relations between the following choice and
+description principles
+
+- AC_rel = relational form of the (non extensional) axiom of choice
+ (a "set-theoretic" axiom of choice)
+- AC_fun = functional form of the (non extensional) axiom of choice
+ (a "type-theoretic" axiom of choice)
+- AC! = functional relation reification
+ (known as axiom of unique choice in topos theory,
+ sometimes called principle of definite description in
+ the context of constructive type theory)
+
+- GAC_rel = guarded relational form of the (non extensional) axiom of choice
+- GAC_fun = guarded functional form of the (non extensional) axiom of choice
+- GAC! = guarded functional relation reification
+
+- OAC_rel = "omniscient" relational form of the (non extensional) axiom of choice
+- OAC_fun = "omniscient" functional form of the (non extensional) axiom of choice
+ (called AC* in Bell [Bell])
+- OAC!
+
+- ID_iota = intuitionistic definite description
+- ID_epsilon = intuitionistic indefinite description
+
+- D_iota = (weakly classical) definite description principle
+- D_epsilon = (weakly classical) indefinite description principle
+
+- PI = proof irrelevance
+- IGP = independence of general premises
+ (an unconstrained generalisation of the constructive principle of
+ independence of premises)
+- Drinker = drinker's paradox (small form)
+ (called Ex in Bell [Bell])
+
+We let also
+
+IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal predicate logic
+IPL_2 = 2nd-order impredicative minimal predicate logic
+IPL^2 = 2nd-order functional minimal predicate logic (with ex. quant.)
+
+Table of contents
+
+A. Definitions
+
+B. IPL_2^2 |- AC_rel + AC! = AC_fun
+
+C. 1. AC_rel + PI -> GAC_rel and PL_2 |- AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel
+
+C. 2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker
+
+D. Derivability of choice for decidable relations with well-ordered codomain
+
+E. Equivalence of choices on dependent or non dependent functional types
+
+F. Non contradiction of constructive descriptions wrt functional choices
+
+G. Definite description transports classical logic to the computational world
-Section ChoiceEquivalences.
+References:
+
+[Bell] John L. Bell, Choice principles in intuitionistic set theory,
+unpublished.
+
+[Bell93] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic
+Type Theories, Mathematical Logic Quarterly, volume 39, 1993.
+
+[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in
+intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
+*)
+
+Set Implicit Arguments.
+
+Notation Local "'inhabited' A" := A (at level 10, only parsing).
+
+(**********************************************************************)
+(** *** A. Definitions *)
+
+(** Choice, reification and description schemes *)
+
+Section ChoiceSchemes.
Variables A B :Type.
-Definition RelationalChoice :=
- forall (R:A -> B -> Prop),
- (forall x:A, exists y : B, R x y) ->
- exists R' : A -> B -> Prop,
- (forall x:A,
- exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+Variables P:A->Prop.
+
+Variables R:A->B->Prop.
+
+(** **** Constructive choice and description *)
+
+(** AC_rel *)
+
+Definition RelationalChoice_on :=
+ forall R:A->B->Prop,
+ (forall x : A, exists y : B, R x y) ->
+ (exists R' : A->B->Prop, subrelation R' R /\ forall x, exists! y, R' x y).
+
+(** AC_fun *)
+
+Definition FunctionalChoice_on :=
+ forall R:A->B->Prop,
+ (forall x : A, exists y : B, R x y) ->
+ (exists f : A->B, forall x : A, R x (f x)).
+
+(** AC! or Functional Relation Reification (known as Axiom of Unique Choice
+ in topos theory; also called principle of definite description *)
+
+Definition FunctionalRelReification_on :=
+ forall R:A->B->Prop,
+ (forall x : A, exists! y : B, R x y) ->
+ (exists f : A->B, forall x : A, R x (f x)).
+
+(** ID_epsilon (constructive version of indefinite description;
+ combined with proof-irrelevance, it may be connected to
+ Carlstrøm's type theory with a constructive indefinite description
+ operator) *)
+
+Definition ConstructiveIndefiniteDescription_on :=
+ forall P:A->Prop,
+ (exists x, P x) -> { x:A | P x }.
+
+(** ID_iota (constructive version of definite description; combined
+ with proof-irrelevance, it may be connected to Carlstrøm's and
+ Stenlund's type theory with a constructive definite description
+ operator) *)
+
+Definition ConstructiveDefiniteDescription_on :=
+ forall P:A->Prop,
+ (exists! x, P x) -> { x:A | P x }.
+
+(** **** Weakly classical choice and description *)
-Definition FunctionalChoice :=
- forall (R:A -> B -> Prop),
- (forall x:A, exists y : B, R x y) ->
- exists f : A -> B, (forall x:A, R x (f x)).
+(** GAC_rel *)
-Definition ParamDefiniteDescription :=
- forall (R:A -> B -> Prop),
- (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) ->
- exists f : A -> B, (forall x:A, R x (f x)).
+Definition GuardedRelationalChoice_on :=
+ forall P : A->Prop, forall R : A->B->Prop,
+ (forall x : A, P x -> exists y : B, R x y) ->
+ (exists R' : A->B->Prop,
+ subrelation R' R /\ forall x, P x -> exists! y, R' x y).
+
+(** GAC_fun *)
+
+Definition GuardedFunctionalChoice_on :=
+ forall P : A->Prop, forall R : A->B->Prop,
+ inhabited B ->
+ (forall x : A, P x -> exists y : B, R x y) ->
+ (exists f : A->B, forall x, P x -> R x (f x)).
+
+(** GFR_fun *)
+
+Definition GuardedFunctionalRelReification_on :=
+ forall P : A->Prop, forall R : A->B->Prop,
+ inhabited B ->
+ (forall x : A, P x -> exists! y : B, R x y) ->
+ (exists f : A->B, forall x : A, P x -> R x (f x)).
+
+(** OAC_rel *)
+
+Definition OmniscientRelationalChoice_on :=
+ forall R : A->B->Prop,
+ exists R' : A->B->Prop,
+ subrelation R' R /\ forall x : A, (exists y : B, R x y) -> exists! y, R' x y.
+
+(** OAC_fun *)
+
+Definition OmniscientFunctionalChoice_on :=
+ forall R : A->B->Prop,
+ inhabited B ->
+ exists f : A->B, forall x : A, (exists y : B, R x y) -> R x (f x).
+
+(** D_epsilon *)
+
+Definition ClassicalIndefiniteDescription :=
+ forall P:A->Prop,
+ A -> { x:A | (exists x, P x) -> P x }.
+
+(** D_iota *)
+
+Definition ClassicalDefiniteDescription :=
+ forall P:A->Prop,
+ A -> { x:A | (exists! x, P x) -> P x }.
+
+End ChoiceSchemes.
+
+(** Generalized schemes *)
+
+Notation RelationalChoice :=
+ (forall A B, RelationalChoice_on A B).
+Notation FunctionalChoice :=
+ (forall A B, FunctionalChoice_on A B).
+Notation FunctionalChoiceOnInhabitedSet :=
+ (forall A B, inhabited B -> FunctionalChoice_on A B).
+Notation FunctionalRelReification :=
+ (forall A B, FunctionalRelReification_on A B).
+
+Notation GuardedRelationalChoice :=
+ (forall A B, GuardedRelationalChoice_on A B).
+Notation GuardedFunctionalChoice :=
+ (forall A B, GuardedFunctionalChoice_on A B).
+Notation GuardedFunctionalRelReification :=
+ (forall A B, GuardedFunctionalRelReification_on A B).
+
+Notation OmniscientRelationalChoice :=
+ (forall A B, OmniscientRelationalChoice_on A B).
+Notation OmniscientFunctionalChoice :=
+ (forall A B, OmniscientFunctionalChoice_on A B).
+
+Notation ConstructiveDefiniteDescription :=
+ (forall A, ConstructiveDefiniteDescription_on A).
+Notation ConstructiveIndefiniteDescription :=
+ (forall A, ConstructiveIndefiniteDescription_on A).
+
+(** Subclassical schemes *)
+
+Definition ProofIrrelevance :=
+ forall (A:Prop) (a1 a2:A), a1 = a2.
+
+Definition IndependenceOfGeneralPremises :=
+ forall (A:Type) (P:A -> Prop) (Q:Prop),
+ inhabited A ->
+ (Q -> exists x, P x) -> exists x, Q -> P x.
+
+Definition SmallDrinker'sParadox :=
+ forall (A:Type) (P:A -> Prop), inhabited A ->
+ exists x, (exists x, P x) -> P x.
+
+(**********************************************************************)
+(** *** B. AC_rel + PDP = AC_fun
+
+ We show that the functional formulation of the axiom of Choice
+ (usual formulation in type theory) is equivalent to its relational
+ formulation (only formulation of set theory) + the axiom of
+ (parametric) definite description (aka axiom of unique choice) *)
+
+(** This shows that the axiom of choice can be assumed (under its
+ relational formulation) without known inconsistency with classical logic,
+ though definite description conflicts with classical logic *)
Lemma description_rel_choice_imp_funct_choice :
- ParamDefiniteDescription -> RelationalChoice -> FunctionalChoice.
-intros Descr RelCh.
-red in |- *; intros R H.
-destruct (RelCh R H) as [R' H0].
-destruct (Descr R') as [f H1].
-intro x.
-elim (H0 x); intros y [H2 [H3 H4]]; exists y; split; [ exact H3 | exact H4 ].
+ forall A B : Type,
+ FunctionalRelReification_on A B -> RelationalChoice_on A B -> FunctionalChoice_on A B.
+Proof.
+intros A B Descr RelCh R H.
+destruct (RelCh R H) as (R',(HR'R,H0)).
+destruct (Descr R') as (f,Hf).
+firstorder.
exists f; intro x.
-elim (H0 x); intros y [H2 [H3 H4]].
-rewrite <- (H4 (f x) (H1 x)).
-exact H2.
+destruct (H0 x) as (y,(HR'xy,Huniq)).
+rewrite <- (Huniq (f x) (Hf x)).
+apply HR'R; assumption.
Qed.
-Lemma funct_choice_imp_rel_choice : FunctionalChoice -> RelationalChoice.
-intros FunCh.
-red in |- *; intros R H.
-destruct (FunCh R H) as [f H0].
-exists (fun x y => y = f x).
-intro x; exists (f x); split;
- [ apply H0
- | split; [ reflexivity | intros y H1; symmetry in |- *; exact H1 ] ].
+Lemma funct_choice_imp_rel_choice :
+ forall A B, FunctionalChoice_on A B -> RelationalChoice_on A B.
+Proof.
+intros A B FunCh R H.
+destruct (FunCh R H) as (f,H0).
+exists (fun x y => f x = y).
+split.
+ intros x y Heq; rewrite <- Heq; trivial.
+ intro x; exists (f x); split.
+ reflexivity.
+ trivial.
Qed.
-Lemma funct_choice_imp_description :
- FunctionalChoice -> ParamDefiniteDescription.
-intros FunCh.
-red in |- *; intros R H.
+Lemma funct_choice_imp_description :
+ forall A B, FunctionalChoice_on A B -> FunctionalRelReification_on A B.
+Proof.
+intros A B FunCh R H.
destruct (FunCh R) as [f H0].
(* 1 *)
intro x.
-elim (H x); intros y [H0 H1].
-exists y; exact H0.
+destruct (H x) as (y,(HRxy,_)).
+exists y; exact HRxy.
(* 2 *)
exists f; exact H0.
Qed.
Theorem FunChoice_Equiv_RelChoice_and_ParamDefinDescr :
- FunctionalChoice <-> RelationalChoice /\ ParamDefiniteDescription.
-split.
+ forall A B, FunctionalChoice_on A B <->
+ RelationalChoice_on A B /\ FunctionalRelReification_on A B.
+Proof.
+intros A B; split.
intro H; split;
[ exact (funct_choice_imp_rel_choice H)
| exact (funct_choice_imp_description H) ].
intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H).
Qed.
-End ChoiceEquivalences.
+(**********************************************************************)
+(** *** C. Connection between the guarded, non guarded and descriptive choices and *)
(** We show that the guarded relational formulation of the axiom of Choice
comes from the non guarded formulation in presence either of the
independance of premises or proof-irrelevance *)
-Definition GuardedRelationalChoice (A B:Type) :=
- forall (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')).
-
-Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.
+(**********************************************************************)
+(** **** C. 1. AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel *)
Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice :
- (forall A B, RelationalChoice A B)
- -> ProofIrrelevance -> (forall A B, GuardedRelationalChoice A B).
+ RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice.
Proof.
intros rel_choice proof_irrel.
red in |- *; intros A B P R H.
-destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as [R' H0].
-intros [x HPx].
-destruct (H x HPx) as [y HRxy].
+destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as (R',(HR'R,H0)).
+intros (x,HPx).
+destruct (H x HPx) as (y,HRxy).
exists y; exact HRxy.
set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y).
-exists R''; intros x HPx.
-destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]].
-exists y. split.
- exact HRxy.
- split.
- red in |- *; exists HPx; exact HR'xy.
- intros y' HR''xy'.
+exists R''; split.
+ intros x y (HPx,HR'xy).
+ change x with (projT1 (existT P x HPx)); apply HR'R; exact HR'xy.
+ intros x HPx.
+ destruct (H0 (existT P x HPx)) as (y,(HR'xy,Huniq)).
+ exists y; split. exists HPx; exact HR'xy.
+ intros y' (H'Px,HR'xy').
apply Huniq.
- unfold R'' in HR''xy'.
- destruct HR''xy' as [H'Px HR'xy'].
- rewrite proof_irrel with (a1 := HPx) (a2 := H'Px).
- exact HR'xy'.
+ rewrite proof_irrel with (a1 := HPx) (a2 := H'Px); exact HR'xy'.
Qed.
-Definition IndependenceOfGeneralPremises :=
- forall (A:Type) (P:A -> Prop) (Q:Prop),
- (Q -> exists x, P x) -> exists x, Q -> P x.
-
Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice :
- forall A B, RelationalChoice A B ->
- IndependenceOfGeneralPremises -> GuardedRelationalChoice A B.
-Proof.
-intros A B RelCh IndPrem.
-red in |- *; intros P R H.
-destruct (RelCh (fun x y => P x -> R x y)) as [R' H0].
- intro x. apply IndPrem.
- apply H.
- exists R'.
- intros x HPx.
- destruct (H0 x) as [y [H1 H2]].
- exists y. split.
- apply (H1 HPx).
- exact H2.
+ forall A B, inhabited B -> RelationalChoice_on A B ->
+ IndependenceOfGeneralPremises -> GuardedRelationalChoice_on A B.
+Proof.
+intros A B Inh AC_rel IndPrem P R H.
+destruct (AC_rel (fun x y => P x -> R x y)) as (R',(HR'R,H0)).
+ intro x. apply IndPrem. exact Inh. intro Hx.
+ apply H; assumption.
+ exists (fun x y => P x /\ R' x y).
+ firstorder.
+Qed.
+
+Lemma guarded_rel_choice_imp_rel_choice :
+ forall A B, GuardedRelationalChoice_on A B -> RelationalChoice_on A B.
+Proof.
+intros A B GAC_rel R H.
+destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)).
+ firstorder.
+exists R'; firstorder.
Qed.
+(** OAC_rel = GAC_rel *)
+
+Lemma guarded_iff_omniscient_rel_choice :
+ GuardedRelationalChoice <-> OmniscientRelationalChoice.
+Proof.
+split.
+ intros GAC_rel A B R.
+ apply (GAC_rel A B (fun x => exists y, R x y) R); auto.
+ intros OAC_rel A B P R H.
+ destruct (OAC_rel A B R) as (f,Hf); exists f; firstorder.
+Qed.
+
+(**********************************************************************)
+(** **** C. 2. AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker *)
+
+(** AC_fun + IGP = GAC_fun *)
+
+Lemma guarded_fun_choice_imp_indep_of_general_premises :
+ GuardedFunctionalChoice -> IndependenceOfGeneralPremises.
+Proof.
+intros GAC_fun A P Q Inh H.
+destruct (GAC_fun unit A (fun _ => Q) (fun _ => P) Inh) as (f,Hf).
+tauto.
+exists (f tt); auto.
+Qed.
+
+Lemma guarded_fun_choice_imp_fun_choice :
+ GuardedFunctionalChoice -> FunctionalChoiceOnInhabitedSet.
+Proof.
+intros GAC_fun A B Inh R H.
+destruct (GAC_fun A B (fun _ => True) R Inh) as (f,Hf).
+firstorder.
+exists f; auto.
+Qed.
+
+Lemma fun_choice_and_indep_general_prem_imp_guarded_fun_choice :
+ FunctionalChoiceOnInhabitedSet -> IndependenceOfGeneralPremises
+ -> GuardedFunctionalChoice.
+Proof.
+intros AC_fun IndPrem A B P R Inh H.
+apply (AC_fun A B Inh (fun x y => P x -> R x y)).
+intro x; apply IndPrem; eauto.
+Qed.
+
+(** AC_fun + Drinker = OAC_fun *)
+
+(** This was already observed by Bell [Bell] *)
+
+Lemma omniscient_fun_choice_imp_small_drinker :
+ OmniscientFunctionalChoice -> SmallDrinker'sParadox.
+Proof.
+intros OAC_fun A P Inh.
+destruct (OAC_fun unit A (fun _ => P)) as (f,Hf).
+auto.
+exists (f tt); firstorder.
+Qed.
+
+Lemma omniscient_fun_choice_imp_fun_choice :
+ OmniscientFunctionalChoice -> FunctionalChoiceOnInhabitedSet.
+Proof.
+intros OAC_fun A B Inh R H.
+destruct (OAC_fun A B R Inh) as (f,Hf).
+exists f; firstorder.
+Qed.
+
+Lemma fun_choice_and_small_drinker_imp_omniscient_fun_choice :
+ FunctionalChoiceOnInhabitedSet -> SmallDrinker'sParadox
+ -> OmniscientFunctionalChoice.
+Proof.
+intros AC_fun Drinker A B R Inh.
+destruct (AC_fun A B Inh (fun x y => (exists y, R x y) -> R x y)) as (f,Hf).
+ intro x; apply (Drinker B (R x) Inh).
+ exists f; assumption.
+Qed.
+
+(** OAC_fun = GAC_fun *)
+
+(** This is derivable from the intuitionistic equivalence between IGP and Drinker
+but we give a direct proof *)
+
+Lemma guarded_iff_omniscient_fun_choice :
+ GuardedFunctionalChoice <-> OmniscientFunctionalChoice.
+Proof.
+split.
+ intros GAC_fun A B R Inh.
+ apply (GAC_fun A B (fun x => exists y, R x y) R); auto.
+ intros OAC_fun A B P R Inh H.
+ destruct (OAC_fun A B R Inh) as (f,Hf).
+ exists f; firstorder.
+Qed.
+
+(**********************************************************************)
+(** *** D. Derivability of choice for decidable relations with well-ordered codomain *)
(** Countable codomains, such as [nat], can be equipped with a
well-order, which implies the existence of a least element on
inhabited decidable subsets. As a consequence, the relational form of
the axiom of choice is derivable on [nat] for decidable relations.
- We show instead that definite description and the functional form
- of the axiom of choice are equivalent on decidable relation with [nat]
- as codomain
+ We show instead that functional relation reification and the
+ functional form of the axiom of choice are equivalent on decidable
+ relation with [nat] as codomain
*)
Require Import Wf_nat.
@@ -163,12 +462,11 @@ Require Import Decidable.
Require Import Arith.
Definition has_unique_least_element (A:Type) (R:A->A->Prop) (P:A->Prop) :=
- (exists x, (P x /\ forall x', P x' -> R x x')
- /\ forall x', P x' /\ (forall x'', P x'' -> R x' x'') -> x=x').
+ exists! x, P x /\ forall x', P x' -> R x x'.
Lemma dec_inh_nat_subset_has_unique_least_element :
forall P:nat->Prop, (forall n, P n \/ ~ P n) ->
- (exists n, P n) -> has_unique_least_element nat le P.
+ (exists n, P n) -> has_unique_least_element le P.
Proof.
intros P Pdec (n0,HPn0).
assert
@@ -194,30 +492,228 @@ assert
assumption.
destruct H0.
rewrite Heqn; assumption.
-destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
- repeat split;
+ destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
+ repeat split;
assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
Qed.
-Definition FunctionalChoice_on (A B:Type) (R:A->B->Prop) :=
- (forall x:A, exists y : B, R x y) ->
- exists f : A -> B, (forall x:A, R x (f x)).
+Definition FunctionalChoice_on_rel (A B:Type) (R:A->B->Prop) :=
+ (forall x:A, exists y : B, R x y) ->
+ exists f : A -> B, (forall x:A, R x (f x)).
Lemma classical_denumerable_description_imp_fun_choice :
forall A:Type,
- ParamDefiniteDescription A nat ->
- forall R, (forall x y, decidable (R x y)) -> FunctionalChoice_on A nat R.
+ FunctionalRelReification_on A nat ->
+ forall R:A->nat->Prop,
+ (forall x y, decidable (R x y)) -> FunctionalChoice_on_rel R.
Proof.
intros A Descr.
red in |- *; intros R Rdec H.
set (R':= fun x y => R x y /\ forall y', R x y' -> y <= y').
-destruct (Descr R') as [f Hf].
+destruct (Descr R') as (f,Hf).
intro x.
apply (dec_inh_nat_subset_has_unique_least_element (R x)).
apply Rdec.
apply (H x).
exists f.
intros x.
-destruct (Hf x) as [Hfx _].
+destruct (Hf x) as (Hfx,_).
+assumption.
+Qed.
+
+(**********************************************************************)
+(** *** E. Choice on dependent and non dependent function types are equivalent *)
+
+(** **** E. 1. Choice on dependent and non dependent function types are equivalent *)
+
+Definition DependentFunctionalChoice_on (A:Type) (B:A -> Type) :=
+ forall R:forall x:A, B x -> Prop,
+ (forall x:A, exists y : B x, R x y) ->
+ (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+
+Notation DependentFunctionalChoice :=
+ (forall A (B:A->Type), DependentFunctionalChoice_on B).
+
+(** The easy part *)
+
+Theorem dep_non_dep_functional_choice :
+ DependentFunctionalChoice -> FunctionalChoice.
+Proof.
+intros AC_depfun A B R H.
+ destruct (AC_depfun A (fun _ => B) R H) as (f,Hf).
+ exists f; trivial.
+Qed.
+
+(** Deriving choice on product types requires some computation on
+ singleton propositional types, so we need computational
+ conjunction projections and dependent elimination of conjunction
+ and equality *)
+
+Scheme and_indd := Induction for and Sort Prop.
+Scheme eq_indd := Induction for eq Sort Prop.
+
+Definition proj1_inf (A B:Prop) (p : A/\B) :=
+ let (a,b) := p in a.
+
+Theorem non_dep_dep_functional_choice :
+ FunctionalChoice -> DependentFunctionalChoice.
+Proof.
+intros AC_fun A B R H.
+pose (B' := { x:A & B x }).
+pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)).
+destruct (AC_fun A B' R') as (f,Hf).
+intros x. destruct (H x) as (y,Hy).
+exists (existT (fun x => B x) x y). split; trivial.
+exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))).
+intro x; destruct (Hf x) as (Heq,HR) using and_indd.
+destruct (f x); simpl in *.
+destruct Heq using eq_indd; trivial.
+Qed.
+
+(** **** E. 2. Reification of dependent and non dependent functional relation are equivalent *)
+
+Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) :=
+ forall (R:forall x:A, B x -> Prop),
+ (forall x:A, exists! y : B x, R x y) ->
+ (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+
+Notation DependentFunctionalRelReification :=
+ (forall A (B:A->Type), DependentFunctionalRelReification_on B).
+
+(** The easy part *)
+
+Theorem dep_non_dep_functional_rel_reification :
+ DependentFunctionalRelReification -> FunctionalRelReification.
+Proof.
+intros DepFunReify A B R H.
+ destruct (DepFunReify A (fun _ => B) R H) as (f,Hf).
+ exists f; trivial.
+Qed.
+
+(** Deriving choice on product types requires some computation on
+ singleton propositional types, so we need computational
+ conjunction projections and dependent elimination of conjunction
+ and equality *)
+
+Theorem non_dep_dep_functional_rel_reification :
+ FunctionalRelReification -> DependentFunctionalRelReification.
+Proof.
+intros AC_fun A B R H.
+pose (B' := { x:A & B x }).
+pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)).
+destruct (AC_fun A B' R') as (f,Hf).
+intros x. destruct (H x) as (y,(Hy,Huni)).
+ exists (existT (fun x => B x) x y). repeat split; trivial.
+ intros (x',y') (Heqx',Hy').
+ simpl in *.
+ destruct Heqx'.
+ rewrite (Huni y'); trivial.
+exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))).
+intro x; destruct (Hf x) as (Heq,HR) using and_indd.
+destruct (f x); simpl in *.
+destruct Heq using eq_indd; trivial.
+Qed.
+
+(**********************************************************************)
+(** *** F. Non contradiction of constructive descriptions wrt functional axioms of choice *)
+
+(** **** F. 1. Non contradiction of indefinite description *)
+
+Lemma relative_non_contradiction_of_indefinite_desc :
+ (ConstructiveIndefiniteDescription -> False)
+ -> (FunctionalChoice -> False).
+Proof.
+intros H AC_fun.
+assert (AC_depfun := non_dep_dep_functional_choice AC_fun).
+pose (A0 := { A:Type & { P:A->Prop & exists x, P x }}).
+pose (B0 := fun x:A0 => projT1 x).
+pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 x) y).
+pose (H0 := fun x:A0 => projT2 (projT2 x)).
+destruct (AC_depfun A0 B0 R0 H0) as (f, Hf).
+apply H.
+intros A P H'.
+exists (f (existT (fun _ => sigT _) A
+ (existT (fun P => exists x, P x) P H'))).
+pose (Hf' :=
+ Hf (existT (fun _ => sigT _) A
+ (existT (fun P => exists x, P x) P H'))).
assumption.
Qed.
+
+Lemma constructive_indefinite_descr_fun_choice :
+ ConstructiveIndefiniteDescription -> FunctionalChoice.
+Proof.
+intros IndefDescr A B R H.
+exists (fun x => proj1_sig (IndefDescr B (R x) (H x))).
+intro x.
+apply (proj2_sig (IndefDescr B (R x) (H x))).
+Qed.
+
+(** **** F. 2. Non contradiction of definite description *)
+
+Lemma relative_non_contradiction_of_definite_descr :
+ (ConstructiveDefiniteDescription -> False)
+ -> (FunctionalRelReification -> False).
+Proof.
+intros H FunReify.
+assert (DepFunReify := non_dep_dep_functional_rel_reification FunReify).
+pose (A0 := { A:Type & { P:A->Prop & exists! x, P x }}).
+pose (B0 := fun x:A0 => projT1 x).
+pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 x) y).
+pose (H0 := fun x:A0 => projT2 (projT2 x)).
+destruct (DepFunReify A0 B0 R0 H0) as (f, Hf).
+apply H.
+intros A P H'.
+exists (f (existT (fun _ => sigT _) A
+ (existT (fun P => exists! x, P x) P H'))).
+pose (Hf' :=
+ Hf (existT (fun _ => sigT _) A
+ (existT (fun P => exists! x, P x) P H'))).
+assumption.
+Qed.
+
+Lemma constructive_definite_descr_fun_reification :
+ ConstructiveDefiniteDescription -> FunctionalRelReification.
+Proof.
+intros DefDescr A B R H.
+exists (fun x => proj1_sig (DefDescr B (R x) (H x))).
+intro x.
+apply (proj2_sig (DefDescr B (R x) (H x))).
+Qed.
+
+(**********************************************************************)
+(** *** G. Excluded-middle + definite description => computational excluded-middle *)
+
+(** The idea for the following proof comes from [ChicliPottierSimpson02] *)
+
+(** Classical logic and axiom of unique choice (i.e. functional
+ relation reification), as shown in [ChicliPottierSimpson02],
+ implies the double-negation of excluded-middle in [Set] (which is
+ incompatible with the impredicativity of [Set]).
+
+ We adapt the proof to show that constructive definite description
+ transports excluded-middle from [Prop] to [Set].
+
+ [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+ Simpson, Mathematical Quotients and Quotient Types in Coq,
+ Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
+ Springer Verlag. *)
+
+Require Import Setoid.
+
+Theorem constructive_definite_descr_excluded_middle :
+ ConstructiveDefiniteDescription ->
+ (forall P:Prop, P \/ ~ P) -> (forall P:Prop, {P} + {~ P}).
+Proof.
+intros Descr EM P.
+pose (select := fun b:bool => if b then P else ~P).
+assert { b:bool | select b } as ([|],HP).
+ apply Descr.
+ rewrite <- unique_existence; split.
+ destruct (EM P).
+ exists true; trivial.
+ exists false; trivial.
+ intros [|] [|] H1 H2; simpl in *; reflexivity || contradiction.
+left; trivial.
+right; trivial.
+Qed.
diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 5a633f84..bb8186ae 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -6,28 +6,40 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ClassicalChoice.v 6401 2004-12-05 16:44:57Z herbelin $ i*)
+(*i $Id: ClassicalChoice.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
-(** This file provides classical logic and functional choice *)
+(** This file provides classical logic, and functional choice *)
-(** This file extends ClassicalDescription.v with the axiom of choice.
- As ClassicalDescription.v, it implies the double-negation of
- excluded-middle in Set and implies a strongly classical
- world. Especially it conflicts with impredicativity of Set, knowing
- that true<>false in Set.
-*)
+(** This file extends ClassicalUniqueChoice.v with the axiom of choice.
+ As ClassicalUniqueChoice.v, it implies the double-negation of
+ excluded-middle in [Set] and leads to a classical world populated
+ with non computable functions. Especially it conflicts with the
+ impredicativity of [Set], knowing that [true<>false] in [Set]. *)
-Require Export ClassicalDescription.
+Require Export ClassicalUniqueChoice.
Require Export RelationalChoice.
Require Import ChoiceFacts.
+Set Implicit Arguments.
+
+Definition subset (U:Type) (P Q:U->Prop) : Prop := forall x, P x -> Q x.
+
+Theorem singleton_choice :
+ forall (A : Type) (P : A->Prop),
+ (exists x : A, P x) -> exists P' : A->Prop, subset P' P /\ exists! x, P' x.
+Proof.
+intros A P H.
+destruct (relational_choice unit A (fun _ => P) (fun _ => H)) as (R',(Hsub,HR')).
+exists (R' tt); firstorder.
+Qed.
+
Theorem choice :
- forall (A B:Type) (R:A -> B -> Prop),
- (forall x:A, exists y : B, R x y) ->
- exists f : A -> B, (forall x:A, R x (f x)).
+ forall (A B : Type) (R : A->B->Prop),
+ (forall x : A, exists y : B, R x y) ->
+ exists f : A->B, (forall x : A, R x (f x)).
Proof.
intros A B.
apply description_rel_choice_imp_funct_choice.
-exact (description A B).
+exact (unique_choice A B).
exact (relational_choice A B).
Qed.
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index ce3e279c..7053266a 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -6,73 +6,95 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ClassicalDescription.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: ClassicalDescription.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
(** This file provides classical logic and definite description *)
-(** Classical logic and definite description, as shown in [1],
- implies the double-negation of excluded-middle in Set, hence it
- implies a strongly classical world. Especially it conflicts with
- impredicativity of Set, knowing that true<>false in Set.
+(** Classical definite description operator (i.e. iota) implies
+ excluded-middle in [Set] and leads to a classical world populated
+ with non computable functions. It conflicts with the
+ impredicativity of [Set] *)
- [1] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical
- Quotients and Quotient Types in Coq, Proceedings of TYPES 2002,
- Lecture Notes in Computer Science 2646, Springer Verlag.
-*)
+Set Implicit Arguments.
Require Export Classical.
+Require Import ChoiceFacts.
-Axiom
- dependent_description :
- forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
- (forall x:A,
- exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) ->
- exists f : forall x:A, B x, (forall x:A, R x (f x)).
+Notation Local "'inhabited' A" := A (at level 200, only parsing).
+
+Axiom constructive_definite_description :
+ forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }.
+
+(** The idea for the following proof comes from [ChicliPottierSimpson02] *)
+
+Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.
+Proof.
+apply
+ (constructive_definite_descr_excluded_middle
+ constructive_definite_description classic).
+Qed.
+
+Theorem classical_definite_description :
+ forall (A : Type) (P : A->Prop), inhabited A ->
+ { x : A | (exists! x : A, P x) -> P x }.
+Proof.
+intros A P i.
+destruct (excluded_middle_informative (exists! x, P x)) as [Hex|HnonP].
+ apply constructive_definite_description with (P:= fun x => (exists! x : A, P x) -> P x).
+ destruct Hex as (x,(Hx,Huni)).
+ exists x; split.
+ intros _; exact Hx.
+ firstorder.
+exists i; tauto.
+Qed.
+
+(** Church's iota operator *)
-(** Principle of definite descriptions (aka axiom of unique choice) *)
+Definition iota (A : Type) (i:inhabited A) (P : A->Prop) : A
+ := proj1_sig (classical_definite_description P i).
+
+Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) :
+ (exists! x:A, P x) -> P (iota i P)
+ := proj2_sig (classical_definite_description P i).
+
+(** Weaker lemmas (compatibility lemmas) *)
+
+Unset Implicit Arguments.
+
+Lemma dependent_description :
+ forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
+ (forall x:A, exists! y : B x, R x y) ->
+ (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+Proof.
+intros A B R H.
+assert (Hexuni:forall x, exists! y, R x y).
+ intro x. apply H.
+exists (fun x => proj1_sig (constructive_definite_description (R x) (Hexuni x))).
+intro x.
+apply (proj2_sig (constructive_definite_description (R x) (Hexuni x))).
+Qed.
Theorem description :
forall (A B:Type) (R:A -> B -> Prop),
- (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) ->
- exists f : A -> B, (forall x:A, R x (f x)).
+ (forall x : A, exists! y : B, R x y) ->
+ (exists f : A->B, forall x:A, R x (f x)).
Proof.
intros A B.
apply (dependent_description A (fun _ => B)).
Qed.
-(** The followig proof comes from [1] *)
+(** Axiom of unique "choice" (functional reification of functional relations) *)
+
+Set Implicit Arguments.
-Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False.
+Require Import Setoid.
+
+Theorem unique_choice :
+ forall (A B:Type) (R:A -> B -> Prop),
+ (forall x:A, exists! y : B, R x y) ->
+ (exists f : A -> B, forall x:A, R x (f x)).
Proof.
-intro HnotEM.
-set (R := fun A b => A /\ true = b \/ ~ A /\ false = b).
-assert (H : exists f : Prop -> bool, (forall A:Prop, R A (f A))).
-apply description.
-intro A.
-destruct (classic A) as [Ha| Hnota].
- exists true; split.
- left; split; [ assumption | reflexivity ].
- intros y [[_ Hy]| [Hna _]].
- assumption.
- contradiction.
- exists false; split.
- right; split; [ assumption | reflexivity ].
- intros y [[Ha _]| [_ Hy]].
- contradiction.
- assumption.
-destruct H as [f Hf].
-apply HnotEM.
-intro P.
-assert (HfP := Hf P).
-(* Elimination from Hf to Set is not allowed but from f to Set yes ! *)
-destruct (f P).
- left.
- destruct HfP as [[Ha _]| [_ Hfalse]].
- assumption.
- discriminate.
- right.
- destruct HfP as [[_ Hfalse]| [Hna _]].
- discriminate.
- assumption.
+intros A B R H.
+apply (description A B).
+intro x. apply H.
Qed.
-
diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v
new file mode 100644
index 00000000..b7293bec
--- /dev/null
+++ b/theories/Logic/ClassicalEpsilon.v
@@ -0,0 +1,90 @@
+(************************************************************************)
+(* 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: ClassicalEpsilon.v 8933 2006-06-09 14:08:38Z herbelin $ i*)
+
+(** *** This file provides classical logic and indefinite description
+ (Hilbert's epsilon operator) *)
+
+(** Classical epsilon's operator (i.e. indefinite description) implies
+ excluded-middle in [Set] and leads to a classical world populated
+ with non computable functions. It conflicts with the
+ impredicativity of [Set] *)
+
+Require Export Classical.
+Require Import ChoiceFacts.
+
+Set Implicit Arguments.
+
+Notation Local "'inhabited' A" := A (at level 200, only parsing).
+
+Axiom constructive_indefinite_description :
+ forall (A : Type) (P : A->Prop),
+ (ex P) -> { x : A | P x }.
+
+Lemma constructive_definite_description :
+ forall (A : Type) (P : A->Prop),
+ (exists! x : A, P x) -> { x : A | P x }.
+Proof.
+intros; apply constructive_indefinite_description; firstorder.
+Qed.
+
+Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.
+Proof.
+apply
+ (constructive_definite_descr_excluded_middle
+ constructive_definite_description classic).
+Qed.
+
+Theorem classical_indefinite_description :
+ forall (A : Type) (P : A->Prop), inhabited A ->
+ { x : A | ex P -> P x }.
+Proof.
+intros A P i.
+destruct (excluded_middle_informative (exists x, P x)) as [Hex|HnonP].
+ apply constructive_indefinite_description with (P:= fun x => ex P -> P x).
+ destruct Hex as (x,Hx).
+ exists x; intros _; exact Hx.
+ firstorder.
+Qed.
+
+(** Hilbert's epsilon operator *)
+
+Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A
+ := proj1_sig (classical_indefinite_description P i).
+
+Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) :
+ (ex P) -> P (epsilon i P)
+ := proj2_sig (classical_indefinite_description P i).
+
+Opaque epsilon.
+
+(** Open question: is classical_indefinite_description constructively
+ provable from [relational_choice] and
+ [constructive_definite_description] (at least, using the fact that
+ [functional_choice] is provable from [relational_choice] and
+ [unique_choice], we know that the double negation of
+ [classical_indefinite_description] is provable (see
+ [relative_non_contradiction_of_indefinite_desc]). *)
+
+(** Remark: we use [ex P] rather than [exists x, P x] (which is [ex
+ (fun x => P x)] to ease unification *)
+
+(** *** Weaker lemmas (compatibility lemmas) *)
+
+Theorem choice :
+ forall (A B : Type) (R : A->B->Prop),
+ (forall x : A, exists y : B, R x y) ->
+ (exists f : A->B, forall x : A, R x (f x)).
+Proof.
+intros A B R H.
+exists (fun x => proj1_sig (constructive_indefinite_description (H x))).
+intro x.
+apply (proj2_sig (constructive_indefinite_description (H x))).
+Qed.
+
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 91056250..70da74d3 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ClassicalFacts.v 8136 2006-03-05 21:57:47Z herbelin $ i*)
+(*i $Id: ClassicalFacts.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
(** ** Some facts and definitions about classical logic
diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
new file mode 100644
index 00000000..79bef2af
--- /dev/null
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -0,0 +1,79 @@
+(************************************************************************)
+(* 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: ClassicalUniqueChoice.v 8893 2006-06-04 18:04:53Z herbelin $ i*)
+
+(** This file provides classical logic and unique choice *)
+
+(** Classical logic and unique choice, as shown in
+ [ChicliPottierSimpson02], implies the double-negation of
+ excluded-middle in [Set], hence it implies a strongly classical
+ world. Especially it conflicts with the impredicativity of [Set].
+
+ [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+ Simpson, Mathematical Quotients and Quotient Types in Coq,
+ Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
+ Springer Verlag. *)
+
+Require Export Classical.
+
+Axiom
+ dependent_unique_choice :
+ forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
+ (forall x : A, exists! y : B x, R x y) ->
+ (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+
+(** Unique choice reifies functional relations into functions *)
+
+Theorem unique_choice :
+ forall (A B:Type) (R:A -> B -> Prop),
+ (forall x:A, exists! y : B, R x y) ->
+ (exists f:A->B, forall x:A, R x (f x)).
+Proof.
+intros A B.
+apply (dependent_unique_choice A (fun _ => B)).
+Qed.
+
+(** The followig proof comes from [ChicliPottierSimpson02] *)
+
+Require Import Setoid.
+
+Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False.
+Proof.
+intro HnotEM.
+set (R := fun A b => A /\ true = b \/ ~ A /\ false = b).
+assert (H : exists f : Prop -> bool, (forall A:Prop, R A (f A))).
+apply unique_choice.
+intro A.
+destruct (classic A) as [Ha| Hnota].
+ exists true; split.
+ left; split; [ assumption | reflexivity ].
+ intros y [[_ Hy]| [Hna _]].
+ assumption.
+ contradiction.
+ exists false; split.
+ right; split; [ assumption | reflexivity ].
+ intros y [[Ha _]| [_ Hy]].
+ contradiction.
+ assumption.
+destruct H as [f Hf].
+apply HnotEM.
+intro P.
+assert (HfP := Hf P).
+(* Elimination from Hf to Set is not allowed but from f to Set yes ! *)
+destruct (f P).
+ left.
+ destruct HfP as [[Ha _]| [_ Hfalse]].
+ assumption.
+ discriminate.
+ right.
+ destruct HfP as [[_ Hfalse]| [Hna _]].
+ discriminate.
+ assumption.
+Qed.
+
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index f8b0e65b..ce3e84a7 100644
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Classical_Prop.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Classical_Prop.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
(** Classical Propositional Logic *)
@@ -22,6 +22,15 @@ unfold not in |- *; intros; elim (classic p); auto.
intro NP; elim (H NP).
Qed.
+(** Peirce's law states [forall P Q:Prop, ((P -> Q) -> P) -> P].
+ Thanks to [forall P, False -> P], it is equivalent to the
+ following form *)
+
+Lemma Peirce : forall P:Prop, ((P -> False) -> P) -> P.
+Proof.
+intros P H; destruct (classic P); auto.
+Qed.
+
Lemma not_imply_elim : forall P Q:Prop, ~ (P -> Q) -> P.
Proof.
intros; apply NNPP; red in |- *.
diff --git a/theories/Logic/DecidableType.v b/theories/Logic/DecidableType.v
new file mode 100644
index 00000000..a38b111f
--- /dev/null
+++ b/theories/Logic/DecidableType.v
@@ -0,0 +1,156 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id: DecidableType.v 8933 2006-06-09 14:08:38Z herbelin $ *)
+
+Require Export SetoidList.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Types with decidable Equalities (but no ordering) *)
+
+Module Type DecidableType.
+
+ Parameter t : Set.
+
+ Parameter eq : t -> t -> Prop.
+
+ Axiom eq_refl : forall x : t, eq x x.
+ Axiom eq_sym : forall x y : t, eq x y -> eq y x.
+ Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
+
+ Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
+
+ Hint Immediate eq_sym.
+ Hint Resolve eq_refl eq_trans.
+
+End DecidableType.
+
+(** * Additional notions about keys and datas used in FMap *)
+
+Module KeyDecidableType(D:DecidableType).
+ Import D.
+
+ Section Elt.
+ Variable elt : Set.
+ Notation key:=t.
+
+ Definition eqk (p p':key*elt) := eq (fst p) (fst p').
+ Definition eqke (p p':key*elt) :=
+ eq (fst p) (fst p') /\ (snd p) = (snd p').
+
+ Hint Unfold eqk eqke.
+ Hint Extern 2 (eqke ?a ?b) => split.
+
+ (* eqke is stricter than eqk *)
+
+ Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'.
+ Proof.
+ unfold eqk, eqke; intuition.
+ Qed.
+
+ (* eqk, eqke are equalities *)
+
+ Lemma eqk_refl : forall e, eqk e e.
+ Proof. auto. Qed.
+
+ Lemma eqke_refl : forall e, eqke e e.
+ Proof. auto. Qed.
+
+ Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e.
+ Proof. auto. Qed.
+
+ Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e.
+ Proof. unfold eqke; intuition. Qed.
+
+ Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''.
+ Proof. eauto. Qed.
+
+ Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''.
+ Proof.
+ unfold eqke; intuition; [ eauto | congruence ].
+ Qed.
+
+ Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
+ Hint Immediate eqk_sym eqke_sym.
+
+ Lemma InA_eqke_eqk :
+ forall x m, InA eqke x m -> InA eqk x m.
+ Proof.
+ unfold eqke; induction 1; intuition.
+ Qed.
+ Hint Resolve InA_eqke_eqk.
+
+ Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
+ Proof.
+ intros; apply InA_eqA with p; auto; apply eqk_trans; auto.
+ Qed.
+
+ Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
+ Definition In k m := exists e:elt, MapsTo k e m.
+
+ Hint Unfold MapsTo In.
+
+ (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
+
+ Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
+ Proof.
+ firstorder.
+ exists x; auto.
+ induction H.
+ destruct y.
+ exists e; auto.
+ destruct IHInA as [e H0].
+ exists e; auto.
+ Qed.
+
+ Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
+ Proof.
+ intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto.
+ Qed.
+
+ Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
+ Proof.
+ destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto.
+ Qed.
+
+ Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
+ Proof.
+ inversion 1.
+ inversion_clear H0; eauto.
+ destruct H1; simpl in *; intuition.
+ Qed.
+
+ Lemma In_inv_2 : forall k k' e e' l,
+ InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
+ Proof.
+ inversion_clear 1; compute in H0; intuition.
+ Qed.
+
+ Lemma In_inv_3 : forall x x' l,
+ InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
+ Proof.
+ inversion_clear 1; compute in H0; intuition.
+ Qed.
+
+ End Elt.
+
+ Hint Unfold eqk eqke.
+ Hint Extern 2 (eqke ?a ?b) => split.
+ Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
+ Hint Immediate eqk_sym eqke_sym.
+ Hint Resolve InA_eqke_eqk.
+ Hint Unfold MapsTo In.
+ Hint Resolve In_inv_2 In_inv_3.
+
+End KeyDecidableType.
+
+
+
+
+
diff --git a/theories/Logic/DecidableTypeEx.v b/theories/Logic/DecidableTypeEx.v
new file mode 100644
index 00000000..a4f99de2
--- /dev/null
+++ b/theories/Logic/DecidableTypeEx.v
@@ -0,0 +1,50 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id: DecidableTypeEx.v 8933 2006-06-09 14:08:38Z herbelin $ *)
+
+Require Import DecidableType OrderedType OrderedTypeEx.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Examples of Decidable Type structures. *)
+
+(** A particular case of [DecidableType] where
+ the equality is the usual one of Coq. *)
+
+Module Type UsualDecidableType.
+ Parameter t : Set.
+ Definition eq := @eq t.
+ Definition eq_refl := @refl_equal t.
+ Definition eq_sym := @sym_eq t.
+ Definition eq_trans := @trans_eq t.
+ Parameter eq_dec : forall x y, { eq x y }+{~eq x y }.
+End UsualDecidableType.
+
+(** a [UsualDecidableType] is in particular an [DecidableType]. *)
+
+Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U.
+
+(** An OrderedType can be seen as a DecidableType *)
+
+Module OT_as_DT (O:OrderedType) <: DecidableType.
+ Module OF := OrderedTypeFacts O.
+ Definition t := O.t.
+ Definition eq := O.eq.
+ Definition eq_refl := O.eq_refl.
+ Definition eq_sym := O.eq_sym.
+ Definition eq_trans := O.eq_trans.
+ Definition eq_dec := OF.eq_dec.
+End OT_as_DT.
+
+(** (Usual) Decidable Type for [nat], [positive], [N], [Z] *)
+
+Module Nat_as_DT <: UsualDecidableType := OT_as_DT (Nat_as_OT).
+Module Positive_as_DT <: UsualDecidableType := OT_as_DT (Positive_as_OT).
+Module N_as_DT <: UsualDecidableType := OT_as_DT (N_as_OT).
+Module Z_as_DT <: UsualDecidableType := OT_as_DT (Z_as_OT).
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 3e94deda..19d5d7ec 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,26 +7,46 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Diaconescu.v 6401 2004-12-05 16:44:57Z herbelin $ i*)
+(*i $Id: Diaconescu.v 8892 2006-06-04 17:59:53Z 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.
+(** Diaconescu showed that the Axiom of Choice entails Excluded-Middle
+ in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show
+ that the axiom of choice in equivalence classes entails
+ Excluded-Middle in Type Theory [LacasWerner99].
- 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
+ Three variants of Diaconescu's result in type theory are shown below.
- [Diaconescu] R. Diaconescu, Axiom of Choice and Complementation, in
- Proceedings of AMS, vol 51, pp 176-178, 1975.
+ A. A proof that the relational form of the Axiom of Choice +
+ Extensionality for Predicates entails Excluded-Middle (by Hugo
+ Herbelin)
- [LacasWerner] S. Lacas, B Werner, Which Choices imply the excluded middle?,
- preprint, 1999.
+ B. A proof that the relational form of the Axiom of Choice + Proof
+ Irrelevance entails Excluded-Middle for Equality Statements (by
+ Benjamin Werner)
+ C. A proof that extensional Hilbert epsilon's description operator
+ entails excluded-middle (taken from Bell [Bell93])
+
+ See also [Carlström] for a discussion of the connection between the
+ Extensional Axiom of Choice and Excluded-Middle
+
+ [Diaconescu75] Radu Diaconescu, Axiom of Choice and Complementation,
+ in Proceedings of AMS, vol 51, pp 176-178, 1975.
+
+ [LacasWerner99] Samuel Lacas, Benjamin Werner, Which Choices imply
+ the excluded middle?, preprint, 1999.
+
+ [Bell93] John L. Bell, Hilbert's epsilon operator and classical
+ logic, Journal of Philosophical Logic, 22: 1-18, 1993
+
+ [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext,
+ Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.
*)
-Section PredExt_GuardRelChoice_imp_EM.
+(**********************************************************************)
+(** *** A. Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle *)
+
+Section PredExt_RelChoice_imp_EM.
(** The axiom of extensionality for predicates *)
@@ -59,15 +80,9 @@ Qed.
Require Import ChoiceFacts.
-Variable rel_choice : forall A B:Type, RelationalChoice A B.
+Variable rel_choice : RelationalChoice.
-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')).
+Lemma guarded_rel_choice : GuardedRelationalChoice.
Proof.
apply
(rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
@@ -78,16 +93,19 @@ Qed.
Require Import Bool.
-Lemma AC :
+Lemma AC_bool_subset_to_bool :
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).
+ destruct (guarded_rel_choice _ _
+ (fun Q:bool -> Prop => exists y : _, Q y)
+ (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)).
+ exact (fun _ H => H).
+ exists R; intros P HP.
+ destruct (HR P HP) as (y,(Hy,Huni)).
+ exists y; firstorder.
Qed.
(** The proof of the excluded middle *)
@@ -98,7 +116,7 @@ Proof.
intro P.
(** first we exhibit the choice functional relation R *)
-destruct AC as [R H].
+destruct AC_bool_subset_to_bool as [R H].
set (class_of_true := fun b => b = true \/ P).
set (class_of_false := fun b => b = false \/ P).
@@ -135,4 +153,152 @@ left; assumption.
Qed.
-End PredExt_GuardRelChoice_imp_EM.
+End PredExt_RelChoice_imp_EM.
+
+(**********************************************************************)
+(** *** B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *)
+
+(** This is an adaptation of Diaconescu's paradox exploiting that
+ proof-irrelevance is some form of extensionality *)
+
+Section ProofIrrel_RelChoice_imp_EqEM.
+
+Variable rel_choice : RelationalChoice.
+
+Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y.
+
+(** Let [a1] and [a2] be two elements in some type [A] *)
+
+Variable A :Type.
+Variables a1 a2 : A.
+
+(** We build the subset [A'] of [A] made of [a1] and [a2] *)
+
+Definition A' := sigT (fun x => x=a1 \/ x=a2).
+
+Definition a1':A'.
+exists a1 ; auto.
+Defined.
+
+Definition a2':A'.
+exists a2 ; auto.
+Defined.
+
+(** By proof-irrelevance, projection is a retraction *)
+
+Lemma projT1_injective : a1=a2 -> a1'=a2'.
+Proof.
+ intro Heq ; unfold a1', a2', A'.
+ rewrite Heq.
+ replace (or_introl (a2=a2) (refl_equal a2))
+ with (or_intror (a2=a2) (refl_equal a2)).
+ reflexivity.
+ apply proof_irrelevance.
+Qed.
+
+(** But from the actual proofs of being in [A'], we can assert in the
+ proof-irrelevant world the existence of relevant boolean witnesses *)
+
+Lemma decide : forall x:A', exists y:bool ,
+ (projT1 x = a1 /\ y = true ) \/ (projT1 x = a2 /\ y = false).
+Proof.
+ intros [a [Ha1|Ha2]]; [exists true | exists false]; auto.
+Qed.
+
+(** Thanks to the axiom of choice, the boolean witnesses move from the
+ propositional world to the relevant world *)
+
+Theorem proof_irrel_rel_choice_imp_eq_dec : a1=a2 \/ ~a1=a2.
+Proof.
+ destruct
+ (rel_choice A' bool
+ (fun x y => projT1 x = a1 /\ y = true \/ projT1 x = a2 /\ y = false))
+ as (R,(HRsub,HR)).
+ apply decide.
+ destruct (HR a1') as (b1,(Ha1'b1,_Huni1)).
+ destruct (HRsub a1' b1 Ha1'b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)].
+ destruct (HR a2') as (b2,(Ha2'b2,Huni2)).
+ destruct (HRsub a2' b2 Ha2'b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)].
+ left; symmetry; assumption.
+ right; intro H.
+ subst b1; subst b2.
+ rewrite (projT1_injective H) in Ha1'b1.
+ assert (false = true) by auto using Huni2.
+ discriminate.
+ left; assumption.
+Qed.
+
+(** An alternative more concise proof can be done by directly using
+ the guarded relational choice *)
+
+Declare Implicit Tactic auto.
+
+Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2.
+Proof.
+ assert (decide: forall x:A, x=a1 \/ x=a2 ->
+ exists y:bool, x=a1 /\ y=true \/ x=a2 /\ y=false).
+ intros a [Ha1|Ha2]; [exists true | exists false]; auto.
+ assert (guarded_rel_choice :=
+ rel_choice_and_proof_irrel_imp_guarded_rel_choice
+ rel_choice
+ proof_irrelevance).
+ destruct
+ (guarded_rel_choice A bool
+ (fun x => x=a1 \/ x=a2)
+ (fun x y => x=a1 /\ y=true \/ x=a2 /\ y=false))
+ as (R,(HRsub,HR)).
+ apply decide.
+ destruct (HR a1) as (b1,(Ha1b1,_Huni1)). left; reflexivity.
+ destruct (HRsub a1 b1 Ha1b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)].
+ destruct (HR a2) as (b2,(Ha2b2,Huni2)). right; reflexivity.
+ destruct (HRsub a2 b2 Ha2b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)].
+ left; symmetry; assumption.
+ right; intro H.
+ subst b1; subst b2; subst a1.
+ assert (false = true) by auto using Huni2, Ha1b1.
+ discriminate.
+ left; assumption.
+Qed.
+
+End ProofIrrel_RelChoice_imp_EqEM.
+
+(**********************************************************************)
+(** *** B. Extensional Hilbert's epsilon description operator -> Excluded-Middle *)
+
+(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *)
+
+Notation Local "'inhabited' A" := A (at level 10, only parsing).
+
+Section ExtensionalEpsilon_imp_EM.
+
+Variable epsilon : forall A : Type, inhabited A -> (A -> Prop) -> A.
+
+Hypothesis epsilon_spec :
+ forall (A:Type) (i:inhabited A) (P:A->Prop),
+ (exists x, P x) -> P (epsilon A i P).
+
+Hypothesis epsilon_extensionality :
+ forall (A:Type) (i:inhabited A) (P Q:A->Prop),
+ (forall a, P a <-> Q a) -> epsilon A i P = epsilon A i Q.
+
+Notation Local eps := (epsilon bool true) (only parsing).
+
+Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P.
+Proof.
+intro P.
+pose (B := fun y => y=false \/ P).
+pose (C := fun y => y=true \/ P).
+assert (B (eps B)) as [Hfalse|HP]
+ by (apply epsilon_spec; exists false; left; reflexivity).
+assert (C (eps C)) as [Htrue|HP]
+ by (apply epsilon_spec; exists true; left; reflexivity).
+ right; intro HP.
+ assert (forall y, B y <-> C y) by (intro y; split; intro; right; assumption).
+ rewrite epsilon_extensionality with (1:=H) in Hfalse.
+ rewrite Htrue in Hfalse.
+ discriminate.
+auto.
+auto.
+Qed.
+
+End ExtensionalEpsilon_imp_EM.
diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v
index 11979057..ec168f09 100644
--- a/theories/Logic/RelationalChoice.v
+++ b/theories/Logic/RelationalChoice.v
@@ -6,15 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RelationalChoice.v 6001 2004-08-01 09:27:26Z herbelin $ i*)
+(*i $Id: RelationalChoice.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
(** This file axiomatizes the relational form of the axiom of choice *)
-Axiom
- relational_choice :
- forall (A B:Type) (R:A -> B -> Prop),
- (forall x:A, exists y : B, R x y) ->
- exists R' : A -> B -> Prop,
- (forall x:A,
- exists y : B,
- R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+Axiom relational_choice :
+ forall (A B : Type) (R : A->B->Prop),
+ (forall x : A, exists y : B, R x y) ->
+ exists R' : A->B->Prop,
+ subrelation R' R /\ forall x : A, exists! y : B, R' x y.