Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableTypeEx.v dans Logic

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

3 files changed, 221 insertions, 9 deletions

diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v
index b3efa5fadd..79c1e56d21 100644
--- a/theories/Logic/ClassicalEpsilon.v
+++ b/theories/Logic/ClassicalEpsilon.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
-(** This file provides classical logic and indefinite description
+(** *** This file provides classical logic and indefinite description
     (Hilbert's epsilon operator) *)
 
 (** Classical epsilon's operator (i.e. indefinite description) implies
@@ -25,7 +25,7 @@ Notation Local "'inhabited' A" := A (at level 200, only parsing).
 
 Axiom constructive_indefinite_description :
   forall (A : Type) (P : A->Prop), 
-  (exists x : A, P x) -> { x : A | P x }.
+  (ex P) -> { x : A | P x }.
 
 Lemma constructive_definite_description :
   forall (A : Type) (P : A->Prop), 
@@ -43,11 +43,11 @@ Qed.
 
 Theorem classical_indefinite_description : 
   forall (A : Type) (P : A->Prop), inhabited A ->
-  { x : A | (exists x : A, P x) -> P x }.
+  { 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 => (exists x, P x) -> P x).
+  apply constructive_indefinite_description with (P:= fun x => ex P -> P x).
   destruct Hex as (x,Hx).
     exists x; intros _; exact Hx.
     firstorder.
@@ -59,9 +59,11 @@ 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) : 
-  (exists x:A, P x) -> P (epsilon i P)
+  (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
@@ -70,7 +72,10 @@ Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) :
     [classical_indefinite_description] is provable (see
     [relative_non_contradiction_of_indefinite_desc]). *)
 
-(** Weaker lemmas (compatibility lemmas) *)
+(** 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),
@@ -78,7 +83,8 @@ Theorem choice :
    (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 (R x) (H x))).
+exists (fun x => proj1_sig (constructive_indefinite_description (H x))).
 intro x.
-apply (proj2_sig (constructive_indefinite_description (R x) (H x))).
+apply (proj2_sig (constructive_indefinite_description  (H x))).
 Qed.
+
diff --git a/theories/Logic/DecidableType.v b/theories/Logic/DecidableType.v
new file mode 100644
index 0000000000..a4de6ca7fe
--- /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$ *)
+
+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 0000000000..dcca370953
--- /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$ *)
+
+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).