Some lemmas about dependent choice + extensions of Compare_dec +

synonyms in Le.v, Lt.v, Gt.v.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12527 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 140 insertions, 38 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 1dc74af73..deb6f229b 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -56,27 +56,47 @@ Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}.
   intros; absurd (m < n); auto with arith.
 Defined.
 
+Theorem le_dec : forall n m, {n <= m} + {~ n <= m}.
+Proof.
+  intros x y; elim (le_gt_dec x y);
+    [ auto with arith | intro; right; apply gt_not_le; assumption ].
+Qed.
+
+Theorem lt_dec : forall n m, {n < m} + {~ n < m}.
+Proof.
+  intros; apply le_dec.
+Qed.
+
+Theorem gt_dec : forall n m, {n > m} + {~ n > m}.
+Proof.
+  intros; apply lt_dec.
+Qed.
+
+Theorem ge_dec : forall n m, {n >= m} + {~ n >= m}.
+Proof.
+  intros; apply le_dec.
+Qed.
+
 (** Proofs of decidability *)
 
 Theorem dec_le : forall n m, decidable (n <= m).
 Proof.
-  intros x y; unfold decidable in |- *; elim (le_gt_dec x y);
-    [ auto with arith | intro; right; apply gt_not_le; assumption ].
+  intros x y; destruct (le_dec x y); unfold decidable; auto.
 Qed.
 
 Theorem dec_lt : forall n m, decidable (n < m).
 Proof.
-  intros x y; unfold lt in |- *; apply dec_le.
+  intros; apply dec_le.
 Qed.
 
 Theorem dec_gt : forall n m, decidable (n > m).
 Proof.
-  intros x y; unfold gt in |- *; apply dec_lt.
+  intros; apply dec_lt.
 Qed.
 
 Theorem dec_ge : forall n m, decidable (n >= m).
 Proof.
-  intros x y; unfold ge in |- *; apply dec_le.
+  intros; apply dec_le.
 Qed.
 
 Theorem not_eq : forall n m, n <> m -> n < m \/ m < n.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index c2ed678cb..70169f52a 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -135,7 +135,7 @@ Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62.
 
 (** * Comparison to 0 *)
 
-Theorem gt_O_eq : forall n, n > 0 \/ 0 = n.
+Theorem gt_0_eq : forall n, n > 0 \/ 0 = n.
 Proof.
   intro n; apply gt_S; auto with arith.
 Qed.
@@ -151,4 +151,8 @@ Lemma plus_gt_compat_l : forall n m p, n > m -> p + n > p + m.
 Proof.
   auto with arith.
 Qed.
-Hint Resolve plus_gt_compat_l: arith v62.
\ No newline at end of file
+Hint Resolve plus_gt_compat_l: arith v62.
+
+(* begin hide *)
+Notation gt_O_eq := gt_0_eq (only parsing).
+(* end hide *)
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 1c00d7ec9..d85178dea 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -41,25 +41,25 @@ Hint Resolve le_trans: arith v62.
 
 (** Comparison to 0 *)
 
-Theorem le_O_n : forall n, 0 <= n.
+Theorem le_0_n : forall n, 0 <= n.
 Proof.
   induction n; auto.
 Qed.
 
-Theorem le_Sn_O : forall n, ~ S n <= 0.
+Theorem le_Sn_0 : forall n, ~ S n <= 0.
 Proof.
   red in |- *; intros n H.
   change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith.
 Qed.
 
-Hint Resolve le_O_n le_Sn_O: arith v62.
+Hint Resolve le_0_n le_Sn_0: arith v62.
 
-Theorem le_n_O_eq : forall n, n <= 0 -> 0 = n.
+Theorem le_n_0_eq : forall n, n <= 0 -> 0 = n.
 Proof.
   induction n; auto with arith.
-  intro; contradiction le_Sn_O with n.
+  intro; contradiction le_Sn_0 with n.
 Qed.
-Hint Immediate le_n_O_eq: arith v62.
+Hint Immediate le_n_0_eq: arith v62.
 
 
 (** [le] and successor *)
@@ -135,3 +135,9 @@ Proof.
   intros m Le.
   elim Le; auto with arith.
 Qed.
+
+(* begin hide *)
+Notation le_O_n := le_0_n (only parsing).
+Notation le_Sn_O := le_Sn_0 (only parsing).
+Notation le_n_O_eq := le_n_0_eq (only parsing).
+(* end hide *)
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index bdd7ce092..af435e54b 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -90,11 +90,11 @@ Proof.
 Qed.
 Hint Immediate lt_S_n: arith v62.
 
-Theorem lt_O_Sn : forall n, 0 < S n.
+Theorem lt_0_Sn : forall n, 0 < S n.
 Proof.
   auto with arith.
 Qed.
-Hint Resolve lt_O_Sn: arith v62.
+Hint Resolve lt_0_Sn: arith v62.
 
 Theorem lt_n_O : forall n, ~ n < 0.
 Proof le_Sn_O.
@@ -175,15 +175,21 @@ Qed.
 
 (** * Comparison to 0 *)
 
-Theorem neq_O_lt : forall n, 0 <> n -> 0 < n.
+Theorem neq_0_lt : forall n, 0 <> n -> 0 < n.
 Proof.
   induction n; auto with arith.
   intros; absurd (0 = 0); trivial with arith.
 Qed.
-Hint Immediate neq_O_lt: arith v62.
+Hint Immediate neq_0_lt: arith v62.
 
-Theorem lt_O_neq : forall n, 0 < n -> 0 <> n.
+Theorem lt_0_neq : forall n, 0 < n -> 0 <> n.
 Proof.
   induction 1; auto with arith.
 Qed.
-Hint Immediate lt_O_neq: arith v62.
\ No newline at end of file
+Hint Immediate lt_0_neq: arith v62.
+
+(* begin hide *)
+Notation lt_O_Sn := lt_0_Sn (only parsing).
+Notation neq_O_lt := neq_0_lt (only parsing).
+Notation lt_O_neq := lt_0_neq (only parsing).
+(* end hide *)
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 748229b17..7141f26cb 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -148,44 +148,51 @@ Section Choice_lemmas.
   Variables R1 R2 : S -> Prop.
 
   Lemma Choice :
-   (forall x:S, sig (fun y:S' => R x y)) ->
-   sig (fun f:S -> S' => forall z:S, R z (f z)).
+   (forall x:S, {y:S' | R x y}) -> {f:S -> S' | forall z:S, R z (f z)}.
   Proof.
    intro H.
-   exists (fun z:S => match H z with
-                      | exist y _ => y
-                      end).
+   exists (fun z => proj1_sig (H z)).
    intro z; destruct (H z); trivial.
   Qed.
 
   Lemma Choice2 :
-   (forall x:S, sigT (fun y:S' => R' x y)) ->
-   sigT (fun f:S -> S' => forall z:S, R' z (f z)).
+   (forall x:S, {y:S' & R' x y}) -> {f:S -> S' & forall z:S, R' z (f z)}.
   Proof.
     intro H.
-    exists (fun z:S => match H z with
-                       | existT y _ => y
-                       end).
+    exists (fun z => projT1 (H z)).
     intro z; destruct (H z); trivial.
   Qed.
 
   Lemma bool_choice :
    (forall x:S, {R1 x} + {R2 x}) ->
-   sig
-     (fun f:S -> bool =>
-        forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x).
+     {f:S -> bool | forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}.
   Proof.
     intro H.
-    exists
-     (fun z:S => match H z with
-                 | left _ => true
-                 | right _ => false
-                 end).
+    exists (fun z:S => if H z then true else false).
     intro z; destruct (H z); auto.
   Qed.
 
 End Choice_lemmas.
 
+Section Dependent_choice_lemmas.
+
+  Variables X : Set.
+  Variable R : X -> X -> Prop.
+
+  Lemma dependent_choice :
+    (forall x:X, {y | R x y}) ->
+    forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}.
+  Proof.
+    intros H x0.
+    set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end).
+    exists f.
+    split. reflexivity.
+    induction n; simpl; apply proj2_sig.
+  Qed.
+
+End Dependent_choice_lemmas.
+
+
  (** A result of type [(Exc A)] is either a normal value of type [A] or
      an [error] :
 
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 02e6d3daf..ef59a4e69 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: ChoiceFacts.v 12363 2009-09-28 15:04:07Z letouzey $ i*)
 
 (** Some facts and definitions concerning choice and description in
        intuitionistic logic.
@@ -19,6 +19,8 @@ description principles
             (a "set-theoretic" axiom of choice)
 - AC_fun  = functional form of the (non extensional) axiom of choice
             (a "type-theoretic" axiom of choice)
+- DC_fun  = functional form of the dependent axiom of choice
+- ACw_fun = functional form of the countable axiom of choice
 - AC!     = functional relation reification
             (known as axiom of unique choice in topos theory,
              sometimes called principle of definite description in
@@ -74,6 +76,8 @@ Table of contents
 
 7. Definite description transports classical logic to the computational world
 
+8. Choice -> Dependent choice -> Countable choice
+
 References:
 
 [[Bell]] John L. Bell, Choice principles in intuitionistic set theory,
@@ -117,6 +121,20 @@ Definition FunctionalChoice_on :=
     (forall x : A, exists y : B, R x y) ->
     (exists f : A->B, forall x : A, R x (f x)).
 
+(** DC_fun *)
+
+Definition FunctionalDependentChoice_on :=
+  forall (R:A->A->Prop),
+    (forall x, exists y, R x y) -> forall x0,
+    (exists f : nat -> A, f 0 = x0 /\ forall n, R (f n) (f (S n))).
+
+(** ACw_fun *)
+
+Definition FunctionalCountableChoice_on :=
+  forall (R:nat->A->Prop),
+    (forall n, exists y, R n y) ->
+    (exists f : nat -> A, forall n, R n (f n)).
+
 (** AC! or Functional Relation Reification (known as Axiom of Unique Choice
     in topos theory; also called principle of definite description *)
 
@@ -203,6 +221,10 @@ Notation RelationalChoice :=
   (forall A B, RelationalChoice_on A B).
 Notation FunctionalChoice :=
   (forall A B, FunctionalChoice_on A B).
+Definition FunctionalDependentChoice :=
+  (forall A, FunctionalDependentChoice_on A).
+Definition FunctionalCountableChoice :=
+  (forall A, FunctionalCountableChoice_on A).
 Notation FunctionalChoiceOnInhabitedSet :=
   (forall A B, inhabited B -> FunctionalChoice_on A B).
 Notation FunctionalRelReification :=
@@ -798,3 +820,40 @@ Proof.
     constructive_definite_descr_excluded_middle,
     (relative_non_contradiction_of_definite_descr (C:=C)).
 Qed.
+
+(**********************************************************************)
+(** * Choice => Dependent choice => Countable choice *)
+
+(* The implications below are standard *)
+
+Require Import Arith.
+
+Theorem functional_choice_imp_functional_dependent_choice :
+   FunctionalChoice -> FunctionalDependentChoice.
+Proof.
+  intros FunChoice A R HRfun x0.
+  apply FunChoice in HRfun as (g,Rg).
+  set (f:=fix f n := match n with 0 => x0 | S n' => g (f n') end).
+  exists f; firstorder.
+Qed.
+
+Theorem functional_dependent_choice_imp_functional_countable_choice :
+   FunctionalDependentChoice -> FunctionalCountableChoice.
+Proof.
+  intros H A R H0.
+  set (R' (p q:nat*A) := fst q = S (fst p) /\ R (fst p) (snd q)).
+  destruct (H0 0) as (y0,Hy0).
+  destruct H with (R:=R') (x0:=(0,y0)) as (f,(Hf0,HfS)).
+    intro x; destruct (H0 (fst x)) as (y,Hy).
+    exists (S (fst x),y).
+    red. auto.
+  assert (Heq:forall n, fst (f n) = n).
+    induction n.
+      rewrite Hf0; reflexivity.
+      specialize HfS with n; destruct HfS as (->,_); congruence.
+  exists (fun n => snd (f (S n))).
+  intro n'. specialize HfS with n'.
+  destruct HfS as (_,HR).
+  rewrite Heq in HR.
+  assumption.
+Qed.