Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

4 files changed, 195 insertions, 70 deletions

diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 7053266a..1f1c34bf 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalDescription.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
+(*i $Id: ClassicalDescription.v 9514 2007-01-22 14:58:50Z herbelin $ i*)
 
 (** This file provides classical logic and definite description *)
 
@@ -57,14 +57,11 @@ 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)).
+(** Axiom of unique "choice" (functional reification of functional relations) *)
+Theorem 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)).
 Proof.
 intros A B R H.
 assert (Hexuni:forall x, exists! y, R x y).
@@ -74,27 +71,18 @@ 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) ->
-   (exists f : A->B, forall x:A, R x (f x)).
+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_description A (fun _ => B)).
+apply dependent_unique_choice with (B:=fun _:A => B).
 Qed.
 
-(** Axiom of unique "choice" (functional reification of functional relations) *)
+(** Compatibility lemmas *)
 
-Set Implicit Arguments.
-
-Require Import Setoid.
+Unset Implicit Arguments.
 
-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 R H.
-apply (description A B).
-intro x. apply H.
-Qed.
+Definition dependent_description := dependent_unique_choice.
+Definition description := unique_choice.
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
new file mode 100644
index 00000000..61e377ea
--- /dev/null
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -0,0 +1,155 @@
+(************************************************************************)
+(*  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:$ i*)
+
+(** This module proves the constructive description schema, which
+infers the sigma-existence (i.e., [Set]-existence) of a witness to a
+predicate from the regular existence (i.e., [Prop]-existence). One
+requires that the underlying set is countable and that the predicate
+is decidable. *)
+
+(** Coq does not allow case analysis on sort [Set] when the goal is in
+[Prop]. Therefore, one cannot eliminate [exists n, P n] in order to
+show [{n : nat | P n}]. However, one can perform a recursion on an
+inductive predicate in sort [Prop] so that the returning type of the
+recursion is in [Set]. This trick is described in Coq'Art book, Sect.
+14.2.3 and 15.4. In particular, this trick is used in the proof of
+[Acc_iter] in the module Coq.Init.Wf. There, recursion is done on an
+inductive predicate [Acc] and the resulting type is in [Type].
+
+The predicate [Acc] delineates elements that are accessible via a
+given relation [R]. An element is accessible if there are no infinite
+[R]-descending chains starting from it.
+
+To use [Acc_iter], we define a relation R and prove that if [exists n,
+P n] then 0 is accessible with respect to R. Then, by induction on the
+definition of [Acc R 0], we show [{n : nat | P n}]. *)
+
+(** Contributed by Yevgeniy Makarov *)
+
+Require Import Arith.
+
+Section ConstructiveIndefiniteDescription.
+
+Variable P : nat -> Prop.
+
+Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}.
+
+(** To find a witness of [P] constructively, we define an algorithm
+that tries P on all natural numbers starting from 0 and going up. The
+relation [R] describes the connection between the two successive
+numbers we try. Namely, [y] is [R]-less then [x] if we try [y] after
+[x], i.e., [y = S x] and [P x] is false. Then the absence of an
+infinite [R]-descending chain from 0 is equivalent to the termination
+of our searching algorithm. *)
+
+Let R (x y : nat) := (x = S y /\ ~ P y).
+Notation Local "'acc' x" := (Acc R x) (at level 10).
+
+Lemma P_implies_acc : forall x : nat, P x -> acc x.
+Proof.
+intros x H. constructor.
+intros y [_ not_Px]. absurd (P x); assumption.
+Qed.
+
+Lemma P_eventually_implies_acc : forall (x : nat) (n : nat), P (n + x) -> acc x.
+Proof.
+intros x n; generalize x; clear x; induction n as [|n IH]; simpl.
+apply P_implies_acc.
+intros x H. constructor. intros y [fxy _].
+apply IH. rewrite fxy.
+replace (n + S x) with (S (n + x)); auto with arith.
+Defined.
+
+Corollary P_eventually_implies_acc_ex : (exists n : nat, P n) -> acc 0.
+Proof.
+intros H; elim H. intros x Px. apply P_eventually_implies_acc with (n := x).
+replace (x + 0) with x; auto with arith.
+Defined.
+
+(** In the following statement, we use the trick with recursion on
+[Acc]. This is also where decidability of [P] is used. *)
+
+Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}.
+Proof.
+intros Acc_0. pattern 0. apply Acc_iter with (R := R); [| assumption].
+clear Acc_0; intros x IH.
+destruct (P_decidable x) as [Px | not_Px].
+exists x; simpl; assumption.
+set (y := S x).
+assert (Ryx : R y x). unfold R; split; auto.
+destruct (IH y Ryx) as [n Hn].
+exists n; assumption.
+Defined.
+
+Theorem constructive_indefinite_description_nat : (exists n : nat, P n) -> {n : nat | P n}.
+Proof.
+intros H; apply acc_implies_P_eventually.
+apply P_eventually_implies_acc_ex; assumption.
+Defined.
+
+End ConstructiveIndefiniteDescription.
+
+Section ConstructiveEpsilon.
+
+(** For the current purpose, we say that a set [A] is countable if
+there are functions [f : A -> nat] and [g : nat -> A] such that [g] is
+a left inverse of [f]. *)
+
+Variable A : Type.
+Variable f : A -> nat.
+Variable g : nat -> A.
+
+Hypothesis gof_eq_id : forall x : A, g (f x) = x.
+
+Variable P : A -> Prop.
+
+Hypothesis P_decidable : forall x : A, {P x} + {~ P x}.
+
+Definition P' (x : nat) : Prop := P (g x).
+
+Lemma P'_decidable : forall n : nat, {P' n} + {~ P' n}.
+Proof.
+intro n; unfold P'; destruct (P_decidable (g n)); auto.
+Defined.
+
+Lemma constructive_indefinite_description : (exists x : A, P x) -> {x : A | P x}.
+Proof.
+intro H. assert (H1 : exists n : nat, P' n).
+destruct H as [x Hx]. exists (f x); unfold P'. rewrite gof_eq_id; assumption.
+apply (constructive_indefinite_description_nat P' P'_decidable)  in H1.
+destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption.
+Defined.
+
+Lemma constructive_definite_description : (exists! x : A, P x) -> {x : A | P x}.
+Proof.
+  intros; apply constructive_indefinite_description; firstorder.
+Defined.
+
+Definition epsilon (E : exists x : A, P x) : A
+  := proj1_sig (constructive_indefinite_description E).
+
+Definition epsilon_spec (E : (exists x, P x)) : P (epsilon E)
+  := proj2_sig (constructive_indefinite_description E).
+
+End ConstructiveEpsilon.
+
+Theorem choice :
+  forall (A B : Type) (f : B -> nat) (g : nat -> B),
+    (forall x : B, g (f x) = x) ->
+    forall (R : A -> B -> Prop),
+    (forall (x : A) (y : B), {R x y} + {~ R x y}) ->
+    (forall x : A, exists y : B, R x y) ->
+    (exists f : A -> B, forall x : A, R x (f x)).
+Proof.
+intros A B f g gof_eq_id R R_dec H.
+exists (fun x : A => epsilon B f g gof_eq_id (R x) (R_dec x) (H x)).
+intro x.
+apply (epsilon_spec B f g gof_eq_id (R x) (R_dec x) (H x)).
+Qed.
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index a257ef55..94a577ca 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: EqdepFacts.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: EqdepFacts.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
 
 (** This file defines dependent equality and shows its equivalence with
     equality on dependent pairs (inhabiting sigma-types). It derives
@@ -105,8 +105,8 @@ Implicit Arguments eq_dep1 [U P].
 (** Dependent equality is equivalent to equality on dependent pairs *)
 
 Lemma eq_sigS_eq_dep :
-  forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q),
-    existS P p x = existS P q y -> eq_dep p x q y.
+  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
+    existT P p x = existT P q y -> eq_dep p x q y.
 Proof.
   intros.
   dependent rewrite H.
@@ -114,7 +114,7 @@ Proof.
 Qed.
 
 Lemma equiv_eqex_eqdep :
-  forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q),
+  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
    existS P p x = existS P q y <-> eq_dep p x q y.
 Proof.
   split. 
@@ -248,28 +248,13 @@ End Equivalences.
 Section Corollaries.
   
   Variable U:Type.
-  Variable V:Set.
   
   (** UIP implies the injectivity of equality on dependent pairs in Type *)
-
-  Definition Inj_dep_pairT :=
-    forall (P:U -> Type) (p:U) (x y:P p),
-      existT P p x = existT P p y -> x = y.
-  
-  Lemma eq_dep_eq__inj_pairT2 : Eq_dep_eq U -> Inj_dep_pairT.
-  Proof.
-    intro eq_dep_eq; red; intros.
-    apply eq_dep_eq.
-    apply eq_sigT_eq_dep.
-    assumption.
- Qed.
- 
-  (** UIP implies the injectivity of equality on dependent pairs in Set *)
  
- Definition Inj_dep_pairS :=
-   forall (P:V -> Set) (p:V) (x y:P p), existS P p x = existS P p y -> x = y.
+ Definition Inj_dep_pair :=
+   forall (P:U -> Type) (p:U) (x y:P p), existT P p x = existT P p y -> x = y.
  
- Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq V -> Inj_dep_pairS.
+ Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq U -> Inj_dep_pair.
  Proof.
    intro eq_dep_eq; red; intros.
    apply eq_dep_eq.
@@ -279,6 +264,11 @@ Section Corollaries.
 
 End Corollaries.
 
+Notation Inj_dep_pairS := Inj_dep_pair.
+Notation Inj_dep_pairT := Inj_dep_pair.
+Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2.
+ 
+
 (************************************************************************)
 (** *** C. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *)
 
@@ -303,7 +293,7 @@ Lemma eq_rect_eq :
 Proof M.eq_rect_eq U.
 
 Lemma eq_rec_eq :
-  forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+  forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rec p Q x p h.
 Proof (fun p Q => M.eq_rect_eq U p Q).
 
 (** Injectivity of Dependent Equality *)
@@ -333,18 +323,13 @@ End Axioms.
 
 (** UIP implies the injectivity of equality on dependent pairs in Type *)
 
-Lemma inj_pairT2 :
+Lemma inj_pair2 :
  forall (U:Type) (P:U -> Type) (p:U) (x y:P p),
    existT P p x = existT P p y -> x = y.
-Proof (fun U => eq_dep_eq__inj_pairT2 U (eq_dep_eq U)).
-
-(** UIP implies the injectivity of equality on dependent pairs in Set *)
-
-Lemma inj_pair2 :
- forall (U:Set) (P:U -> Set) (p:U) (x y:P p),
-   existS P p x = existS P p y -> x = y.
 Proof (fun U => eq_dep_eq__inj_pair2 U (eq_dep_eq U)).
 
+Notation inj_pairT2 := inj_pair2.
+
 End EqdepTheory.
 
 Implicit Arguments eq_dep [].
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 740fcfcf..103efd22 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Eqdep_dec.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Eqdep_dec.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
 
 (** We prove that there is only one proof of [x=x], i.e [refl_equal x].
     This holds if the equality upon the set of [x] is decidable.
@@ -235,7 +235,7 @@ End DecidableEqDep.
 
 Module Type DecidableSet.
 
-  Parameter U:Set.
+  Parameter U:Type.
   Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
 
 End DecidableSet.
@@ -276,14 +276,6 @@ Module DecidableEqDepSet (M:DecidableSet).
     forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
   Proof N.Streicher_K.
 
-  (** Injectivity of equality on dependent pairs with second component
-      in [Type] *)
-
-  Lemma inj_pairT2 :
-    forall (P:U -> Type) (p:U) (x y:P p),
-      existT P p x = existT P p y -> x = y.
-  Proof N.inj_pairT2.
-
   (** Proof-irrelevance on subsets of decidable sets *)
 
   Lemma inj_pairP2 :
@@ -291,11 +283,16 @@ Module DecidableEqDepSet (M:DecidableSet).
       ex_intro P x p = ex_intro P x q -> p = q.
   Proof N.inj_pairP2.
 
-  (** Injectivity of equality on dependent pairs in [Set] *)
+  (** Injectivity of equality on dependent pairs in [Type] *)
 
   Lemma inj_pair2 :
-    forall (P:U -> Set) (p:U) (x y:P p),
+    forall (P:U -> Type) (p:U) (x y:P p),
       existS P p x = existS P p y -> x = y.
   Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq.
 
+  (** Injectivity of equality on dependent pairs with second component
+      in [Type] *)
+
+  Notation inj_pairT2 := inj_pair2.
+
 End DecidableEqDepSet.