OrderedType implementation for various numerical datatypes + min/max structures

 - A richer OrderedTypeFull interface : OrderedType + predicate "le"
 - Implementations {Nat,N,P,Z,Q}OrderedType.v, also providing "order" tactics
 - By the way: as suggested by S. Lescuyer, specification of compare is
   now inductive
 - GenericMinMax: axiomatisation + properties of min and max out of
    OrderedTypeFull structures.
 - MinMax.v, {Z,P,N,Q}minmax.v are specialization of GenericMinMax,
    with also some domain-specific results, and compatibility layer
    with already existing results.
 - Some ML code of plugins had to be adapted, otherwise wrong "eq",
   "lt" or simimlar constants were found by functions like coq_constant.
 - Beware of the aliasing problems: for instance eq:=@eq t instead of
   eq:=@eq M.t in Make_UDT made (r)omega stopped working (Z_as_OT.t
   instead of Z in statement of Zmax_spec).
 - Some Morphism declaration are now ambiguous: switch to new syntax
   anyway.
 - Misc adaptations of FSets/MSets
 - Classes/RelationPairs.v: from two relations over A and B, we
   inspect relations over A*B and their properties in terms of classes.

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

1 files changed, 141 insertions, 0 deletions

diff --git a/theories/Structures/DecidableType2Facts.v b/theories/Structures/DecidableType2Facts.v
new file mode 100644
index 0000000000..5a5caaab8b
--- /dev/null
+++ b/theories/Structures/DecidableType2Facts.v
@@ -0,0 +1,141 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+Require Import DecidableType2 SetoidList.
+
+
+(** * Keys and datas used in FMap *)
+
+Module KeyDecidableType(D:DecidableType).
+ Import D.
+
+ Section Elt.
+ Variable elt : Type.
+ 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 *)
+
+  Instance eqk_equiv : Equivalence eqk.
+  Proof.
+   constructor; eauto.
+  Qed.
+
+  Instance eqke_equiv : Equivalence eqke.
+  Proof.
+   constructor. auto.
+   red; unfold eqke; intuition.
+   red; unfold eqke; intuition; [ eauto | congruence ].
+  Qed.
+
+  Hint Resolve (@Equivalence_Reflexive _ _ eqk_equiv).
+  Hint Resolve (@Equivalence_Transitive _ _ eqk_equiv).
+  Hint Immediate (@Equivalence_Symmetric _ _ eqk_equiv).
+  Hint Resolve (@Equivalence_Reflexive _ _ eqke_equiv).
+  Hint Resolve (@Equivalence_Transitive _ _ eqke_equiv).
+  Hint Immediate (@Equivalence_Symmetric _ _ eqke_equiv).
+
+  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. rewrite <- H; 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.
+
+  Global Instance MapsTo_compat :
+    Proper (eq==>Logic.eq==>Logic.eq==>iff) MapsTo.
+  Proof.
+  intros x x' Hxx' e e' Hee' l l' Hll'; subst.
+  unfold MapsTo.
+  assert (EQN : eqke (x,e') (x',e')) by (compute;auto).
+  rewrite EQN; intuition.
+  Qed.
+
+  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
+  Proof.
+  intros; rewrite <- H; auto.
+  Qed.
+
+  Global Instance In_compat : Proper (eq==>Logic.eq==>iff) In.
+  Proof.
+  intros x x' Hxx' l l' Hll'; subst l.
+  unfold In.
+  split; intros (e,He); exists e.
+  rewrite <- Hxx'; auto.
+  rewrite Hxx'; auto.
+  Qed.
+
+  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
+  Proof.
+  intros; rewrite <- H; auto.
+  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 Resolve In_inv_2 In_inv_3.
+ (* TODO: (re-)populate with more hints after failed attempt of Global Hint *)
+
+End KeyDecidableType.
+
+
+