1 files changed, 112 insertions, 28 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 87d8a70e..bc892ca9 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ChoiceFacts.v,v 1.7.2.2 2004/08/01 09:29:59 herbelin Exp $ i*)
+(*i $Id: ChoiceFacts.v 8132 2006-03-05 10:59:47Z herbelin $ i*)
 
 (** We show that the functional formulation of the axiom of Choice
    (usual formulation in type theory) is equivalent to its relational
@@ -17,29 +17,33 @@
    relational formulation) without known inconsistency with classical logic,
    though definite description conflicts with classical logic *)
 
+Section ChoiceEquivalences.
+
+Variables A B :Type.
+
 Definition RelationalChoice :=
-  forall (A B:Type) (R:A -> B -> Prop),
-    (forall x:A,  exists y : B, R x y) ->
+  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')).
+         exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
 
 Definition FunctionalChoice :=
-  forall (A B:Type) (R:A -> B -> Prop),
-    (forall x:A,  exists y : B, R x y) ->
+  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)).
 
 Definition ParamDefiniteDescription :=
-  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')) ->
+  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)).
 
 Lemma description_rel_choice_imp_funct_choice :
  ParamDefiniteDescription -> RelationalChoice -> FunctionalChoice.
 intros Descr RelCh.
-red in |- *; intros A B R H.
-destruct (RelCh A B R H) as [R' H0].
-destruct (Descr A B R') as [f H1].
+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 ].
 exists f; intro x.
@@ -50,8 +54,8 @@ Qed.
 
 Lemma funct_choice_imp_rel_choice : FunctionalChoice -> RelationalChoice.
 intros FunCh.
-red in |- *; intros A B R H.
-destruct (FunCh A B R H) as [f H0].
+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
@@ -61,8 +65,8 @@ Qed.
 Lemma funct_choice_imp_description :
  FunctionalChoice -> ParamDefiniteDescription.
 intros FunCh.
-red in |- *; intros A B R H.
-destruct (FunCh A B R) as [f H0].
+red in |- *; intros R H.
+destruct (FunCh R) as [f H0].
 (* 1 *)
 intro x.
 elim (H x); intros y [H0 H1].
@@ -80,22 +84,25 @@ intro H; split;
 intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H).
 Qed.
 
+End ChoiceEquivalences.
+
 (** 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 :=
-  forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop),
-    (forall x:A, P x ->  exists y : B, R x y) ->
+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')).
+         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.
 
 Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice :
- RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice.
+  (forall A B, RelationalChoice A B)
+    -> ProofIrrelevance -> (forall A B, GuardedRelationalChoice A B).
 Proof.
 intros rel_choice proof_irrel.
 red in |- *; intros A B P R H.
@@ -103,7 +110,7 @@ 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].
 exists y; exact HRxy.
-set (R'' := fun (x:A) (y:B) =>  exists H : P x, R' (existT P x H) y).
+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.
@@ -118,16 +125,17 @@ exists y. split.
       exact HR'xy'.
 Qed.
 
-Definition IndependenceOfPremises :=
+Definition IndependenceOfGeneralPremises :=
   forall (A:Type) (P:A -> Prop) (Q:Prop),
-    (Q ->  exists x : _, P x) ->  exists x : _, Q -> P x.
+    (Q -> exists x, P x) -> exists x, Q -> P x.
 
-Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice :
- RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice.
+Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice :
+ forall A B, RelationalChoice A B -> 
+   IndependenceOfGeneralPremises -> GuardedRelationalChoice A B.
 Proof.
-intros RelCh IndPrem.
-red in |- *; intros A B P R H.
-destruct (RelCh A B (fun x y => P x -> R x y)) as [R' H0].
+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'.
@@ -137,3 +145,79 @@ destruct (RelCh A B (fun x y => P x -> R x y)) as [R' H0].
       apply (H1 HPx).
       exact H2.
 Qed.
+
+
+(** 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 
+*)
+
+Require Import Wf_nat.
+Require Import Compare_dec.
+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').
+
+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.
+Proof.
+intros P Pdec (n0,HPn0).
+assert
+   (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'')
+              \/(forall n', P n' -> n<=n')).
+  induction n.
+  right.
+  intros n' Hn'.
+  apply le_O_n.
+  destruct IHn.
+  left; destruct H as (n', (Hlt', HPn')).
+  exists n'; split.
+  apply lt_S; assumption.
+  assumption.
+  destruct (Pdec n).
+  left; exists n; split.
+  apply lt_n_Sn.
+  split; assumption.
+  right.
+  intros n' Hltn'.
+  destruct (le_lt_eq_dec n n') as [Hltn|Heqn].
+  apply H; assumption.
+  assumption.
+  destruct H0.
+  rewrite Heqn; assumption.
+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)).
+
+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.
+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].
+  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 _].
+assumption.
+Qed.