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, 0 insertions, 627 deletions

diff --git a/theories/FSets/DecidableType.v b/theories/FSets/DecidableType.v
deleted file mode 100644
index a4de6ca7fe..0000000000
--- a/theories/FSets/DecidableType.v
+++ /dev/null
@@ -1,156 +0,0 @@
-(***********************************************************************)
-(*  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/FSets/DecidableTypeEx.v b/theories/FSets/DecidableTypeEx.v
deleted file mode 100644
index dcca370953..0000000000
--- a/theories/FSets/DecidableTypeEx.v
+++ /dev/null
@@ -1,50 +0,0 @@
-(***********************************************************************)
-(*  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).
diff --git a/theories/FSets/Int.v b/theories/FSets/Int.v
deleted file mode 100644
index ee8b245619..0000000000
--- a/theories/FSets/Int.v
+++ /dev/null
@@ -1,421 +0,0 @@
-(***********************************************************************)
-(*  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       *)
-(***********************************************************************)
-
-(* Finite sets library.  
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre 
- * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
- *              91405 Orsay, France *)
-
-(* $Id$ *)
-
-(** * An axiomatization of integers. *) 
-
-(** We define a signature for an integer datatype based on [Z]. 
-   The goal is to allow a switch after extraction to ocaml's 
-   [big_int] or even [int] when finiteness isn't a problem 
-   (typically : when mesuring the height of an AVL tree). 
-*)
-
-Require Import ZArith. 
-Require Import ROmega. 
-Delimit Scope Int_scope with I.
-
-Module Type Int.
-
- Open Scope Int_scope.
-
- Parameter int : Set. 
-
- Parameter i2z : int -> Z.
- Arguments Scope i2z [ Int_scope ].
-
- Parameter _0 : int. 
- Parameter _1 : int. 
- Parameter _2 : int. 
- Parameter _3 : int.
- Parameter plus : int -> int -> int. 
- Parameter opp : int -> int.
- Parameter minus : int -> int -> int. 
- Parameter mult : int -> int -> int.
- Parameter max : int -> int -> int. 
-
- Notation "0" := _0 : Int_scope.
- Notation "1" := _1 : Int_scope. 
- Notation "2" := _2 : Int_scope. 
- Notation "3" := _3 : Int_scope.
- Infix "+" := plus : Int_scope.
- Infix "-" := minus : Int_scope.
- Infix "*" := mult : Int_scope.
- Notation "- x" := (opp x) : Int_scope.
-
-(** For logical relations, we can rely on their counterparts in Z, 
-   since they don't appear after extraction. Moreover, using tactics 
-   like omega is easier this way. *)
-
- Notation "x == y" := (i2z x = i2z y)
-   (at level 70, y at next level, no associativity) : Int_scope.
- Notation "x <= y" := (Zle (i2z x) (i2z y)): Int_scope.
- Notation "x < y" := (Zlt (i2z x) (i2z y)) : Int_scope.
- Notation "x >= y" := (Zge (i2z x) (i2z y)) : Int_scope.
- Notation "x > y" := (Zgt (i2z x) (i2z y)): Int_scope.
- Notation "x <= y <= z" := (x <= y /\ y <= z) : Int_scope.
- Notation "x <= y < z" := (x <= y /\ y < z) : Int_scope.
- Notation "x < y < z" := (x < y /\ y < z) : Int_scope.
- Notation "x < y <= z" := (x < y /\ y <= z) : Int_scope.
-
- (** Some decidability fonctions (informative). *)
-
- Axiom gt_le_dec : forall x y: int, {x > y} + {x <= y}.
- Axiom ge_lt_dec :  forall x y : int, {x >= y} + {x < y}.
- Axiom eq_dec : forall x y : int, { x == y } + {~ x==y }.
-
- (** Specifications *)
-
- (** First, we ask [i2z] to be injective. Said otherwise, our ad-hoc equality 
-    [==] and the generic [=] are in fact equivalent. We define [==] 
-    nonetheless since the translation to [Z] for using automatic tactic is easier. *)
-
- Axiom i2z_eq : forall n p : int, n == p -> n = p. 
-
- (** Then, we express the specifications of the above parameters using their 
-    Z counterparts. *)
-
- Open Scope Z_scope.
- Axiom i2z_0 : i2z _0 = 0.
- Axiom i2z_1 : i2z _1 = 1.
- Axiom i2z_2 : i2z _2 = 2.
- Axiom i2z_3 : i2z _3 = 3.
- Axiom i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p.
- Axiom i2z_opp : forall n, i2z (-n) = -i2z n.
- Axiom i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p.
- Axiom i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p.
- Axiom i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p).
-
-End Int. 
-
-Module MoreInt (I:Int).
- Import I.
-
- Open Scope Int_scope.
-
- (** A magic (but costly) tactic that goes from [int] back to the [Z] 
-     friendly world ... *)
-
- Hint Rewrite -> 
-   i2z_0 i2z_1 i2z_2 i2z_3 i2z_plus i2z_opp i2z_minus i2z_mult i2z_max : i2z.
-
- Ltac i2z := match goal with 
-  | H : (eq (A:=int) ?a ?b) |- _ => 
-       generalize (f_equal i2z H); 
-       try autorewrite with i2z; clear H; intro H; i2z
-  | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); try autorewrite with i2z; i2z
-  | H : _ |- _ => progress autorewrite with i2z in H; i2z
-  | _ => try autorewrite with i2z
- end.
-
- (** A reflexive version of the [i2z] tactic *)
-
- (** this [i2z_refl] is actually weaker than [i2z]. For instance, if a 
-      [i2z] is buried deep inside a subterm, [i2z_refl] may miss it. 
-      See also the limitation about [Set] or [Type] part below. 
-      Anyhow, [i2z_refl] is enough for applying [romega]. *)
- 
-  Ltac i2z_gen := match goal with 
-    | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); i2z_gen
-    | H : (eq (A:=int) ?a ?b) |- _ => 
-       generalize (f_equal i2z H); clear H; i2z_gen
-    | H : (eq (A:=Z) ?a ?b) |- _ => generalize H; clear H; i2z_gen
-    | H : (Zlt ?a ?b) |- _ => generalize H; clear H; i2z_gen
-    | H : (Zle ?a ?b) |- _ => generalize H; clear H; i2z_gen
-    | H : (Zgt ?a ?b) |- _ => generalize H; clear H; i2z_gen
-    | H : (Zge ?a ?b) |- _ => generalize H; clear H; i2z_gen
-    | H : _ -> ?X |- _ => 
-      (* A [Set] or [Type] part cannot be dealt with easily
-         using the [ExprP] datatype. So we forget it, leaving 
-         a goal that can be weaker than the original. *)
-      match type of X with 
-       | Type => clear H; i2z_gen
-       | Prop => generalize H; clear H; i2z_gen
-      end
-    | H : _ <-> _ |- _ => generalize H; clear H; i2z_gen
-    | H : _ /\ _ |- _ => generalize H; clear H; i2z_gen
-    | H : _ \/ _ |- _ => generalize H; clear H; i2z_gen
-    | H : ~ _ |- _ => generalize H; clear H; i2z_gen
-    | _ => idtac
-   end.
-
-  Inductive ExprI : Set := 
-   | EI0 : ExprI
-   | EI1 : ExprI
-   | EI2 : ExprI 
-   | EI3 : ExprI
-   | EIplus : ExprI -> ExprI -> ExprI
-   | EIopp : ExprI -> ExprI
-   | EIminus : ExprI -> ExprI -> ExprI
-   | EImult : ExprI -> ExprI -> ExprI
-   | EImax : ExprI -> ExprI -> ExprI
-   | EIraw : int -> ExprI.
-
-  Inductive ExprZ : Set :=  
-   | EZplus : ExprZ -> ExprZ -> ExprZ
-   | EZopp : ExprZ -> ExprZ
-   | EZminus : ExprZ -> ExprZ -> ExprZ
-   | EZmult : ExprZ -> ExprZ -> ExprZ
-   | EZmax : ExprZ -> ExprZ -> ExprZ
-   | EZofI : ExprI -> ExprZ
-   | EZraw : Z -> ExprZ.
-
-  Inductive ExprP : Type := 
-   | EPeq : ExprZ -> ExprZ -> ExprP 
-   | EPlt : ExprZ -> ExprZ -> ExprP 
-   | EPle : ExprZ -> ExprZ -> ExprP 
-   | EPgt : ExprZ -> ExprZ -> ExprP 
-   | EPge : ExprZ -> ExprZ -> ExprP 
-   | EPimpl : ExprP -> ExprP -> ExprP
-   | EPequiv : ExprP -> ExprP -> ExprP
-   | EPand : ExprP -> ExprP -> ExprP
-   | EPor : ExprP -> ExprP -> ExprP
-   | EPneg : ExprP -> ExprP
-   | EPraw : Prop -> ExprP.
-
- (** [int] to [ExprI] *)
-
- Ltac i2ei trm := 
-  match constr:trm with 
-    | 0 => constr:EI0
-    | 1 => constr:EI1
-    | 2 => constr:EI2
-    | 3 => constr:EI3
-    | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIplus ex ey)
-    | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIminus ex ey)
-    | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImult ex ey)
-    | max ?x ?y => let ex := i2ei x with ey := i2ei y in constr:(EImax ex ey)
-    | - ?x => let ex := i2ei x in constr:(EIopp ex)
-    | ?x => constr:(EIraw x)
-   end
-
- (** [Z] to [ExprZ] *)
-
- with z2ez trm := 
-   match constr:trm with 
-    | (?x+?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZplus ex ey)
-    | (?x-?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZminus ex ey)
-    | (?x*?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmult ex ey)
-    | (Zmax ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EZmax ex ey)
-    | (-?x)%Z =>  let ex := z2ez x in constr:(EZopp ex)
-    | i2z ?x => let ex := i2ei x in constr:(EZofI ex)
-    | ?x => constr:(EZraw x)
-   end.
-
- (** [Prop] to [ExprP] *)
-
- Ltac p2ep trm :=
-  match constr:trm with
-    | (?x <-> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPequiv ex ey)
-    | (?x -> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPimpl ex ey)
-    | (?x /\ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPand ex ey)
-    | (?x \/ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPor ex ey)
-    | (~ ?x) => let ex := p2ep x in constr:(EPneg ex)
-    | (eq (A:=Z) ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EPeq ex ey)
-    | (?x<?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPlt ex ey)
-    | (?x<=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPle ex ey)   
-    | (?x>?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPgt ex ey)   
-    | (?x>=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPge ex ey)
-    | ?x =>  constr:(EPraw x)
-   end.   
-
- (** [ExprI] to [int] *)
-
- Fixpoint ei2i (e:ExprI) : int :=
-  match e with
-  | EI0 => 0
-  | EI1 => 1
-  | EI2 => 2
-  | EI3 => 3 
-  | EIplus e1 e2 => (ei2i e1)+(ei2i e2)
-  | EIminus e1 e2 => (ei2i e1)-(ei2i e2)
-  | EImult e1 e2 => (ei2i e1)*(ei2i e2)
-  | EImax e1 e2 => max (ei2i e1) (ei2i e2)
-  | EIopp e => -(ei2i e)
-  | EIraw i => i 
-  end. 
- 
- (** [ExprZ] to [Z] *)
-
- Fixpoint ez2z (e:ExprZ) : Z := 
-  match e with 
-  | EZplus e1 e2 => ((ez2z e1)+(ez2z e2))%Z
-  | EZminus e1 e2 => ((ez2z e1)-(ez2z e2))%Z
-  | EZmult e1 e2 => ((ez2z e1)*(ez2z e2))%Z
-  | EZmax e1 e2 => Zmax (ez2z e1) (ez2z e2)
-  | EZopp e => (-(ez2z e))%Z
-  | EZofI e => i2z (ei2i e)
-  | EZraw z => z
-  end.
-
- (** [ExprP] to [Prop] *)
-
- Fixpoint ep2p (e:ExprP) : Prop := 
-  match e with 
-   | EPeq e1 e2 => (ez2z e1) = (ez2z e2)
-   | EPlt e1 e2 => ((ez2z e1)<(ez2z e2))%Z
-   | EPle e1 e2 => ((ez2z e1)<=(ez2z e2))%Z
-   | EPgt e1 e2 => ((ez2z e1)>(ez2z e2))%Z
-   | EPge e1 e2 => ((ez2z e1)>=(ez2z e2))%Z
-   | EPimpl e1 e2 => (ep2p e1) -> (ep2p e2)
-   | EPequiv e1 e2 => (ep2p e1) <-> (ep2p e2)
-   | EPand e1 e2 => (ep2p e1) /\ (ep2p e2)
-   | EPor e1 e2 => (ep2p e1) \/ (ep2p e2)
-   | EPneg e => ~ (ep2p e)
-   | EPraw p => p
- end.
-
- (** [ExprI] (supposed under a [i2z]) to a simplified [ExprZ] *)
-   
- Fixpoint norm_ei (e:ExprI) : ExprZ := 
- match e with 
-  | EI0 => EZraw (0%Z)
-  | EI1 => EZraw (1%Z)
-  | EI2 => EZraw (2%Z)
-  | EI3 => EZraw (3%Z) 
-  | EIplus e1 e2 => EZplus (norm_ei e1) (norm_ei e2)
-  | EIminus e1 e2 => EZminus (norm_ei e1) (norm_ei e2)
-  | EImult e1 e2 => EZmult (norm_ei e1) (norm_ei e2)
-  | EImax e1 e2 => EZmax (norm_ei e1) (norm_ei e2)
-  | EIopp e => EZopp (norm_ei e)
-  | EIraw i => EZofI (EIraw i) 
- end.
-
- (** [ExprZ] to a simplified [ExprZ] *)
-
- Fixpoint norm_ez (e:ExprZ) : ExprZ := 
-  match e with 
-  | EZplus e1 e2 => EZplus (norm_ez e1) (norm_ez e2)
-  | EZminus e1 e2 => EZminus (norm_ez e1) (norm_ez e2)
-  | EZmult e1 e2 => EZmult (norm_ez e1) (norm_ez e2)
-  | EZmax e1 e2 => EZmax (norm_ez e1) (norm_ez e2)
-  | EZopp e => EZopp (norm_ez e)
-  | EZofI e =>  norm_ei e
-  | EZraw z => EZraw z
- end.
-
- (** [ExprP] to a simplified [ExprP] *)
-
- Fixpoint norm_ep (e:ExprP) : ExprP := 
-  match e with 
-   | EPeq e1 e2 => EPeq (norm_ez e1) (norm_ez e2)
-   | EPlt e1 e2 => EPlt (norm_ez e1) (norm_ez e2)
-   | EPle e1 e2 => EPle (norm_ez e1) (norm_ez e2)
-   | EPgt e1 e2 => EPgt (norm_ez e1) (norm_ez e2)
-   | EPge e1 e2 => EPge (norm_ez e1) (norm_ez e2)
-   | EPimpl e1 e2 => EPimpl (norm_ep e1) (norm_ep e2)
-   | EPequiv e1 e2 => EPequiv (norm_ep e1) (norm_ep e2)
-   | EPand e1 e2 => EPand (norm_ep e1) (norm_ep e2)
-   | EPor e1 e2 => EPor (norm_ep e1) (norm_ep e2)
-   | EPneg e => EPneg (norm_ep e)
-   | EPraw p => EPraw p
- end.
-
- Lemma norm_ei_correct : forall e:ExprI, ez2z (norm_ei e) = i2z (ei2i e).
- Proof. 
- induction e; simpl; intros; i2z; auto; try congruence.
- Qed.
-
- Lemma norm_ez_correct : forall e:ExprZ, ez2z (norm_ez e) = ez2z e.
- Proof.
- induction e; simpl; intros; i2z; auto; try congruence; apply norm_ei_correct.
- Qed. 
-
- Lemma norm_ep_correct : 
-  forall e:ExprP, ep2p (norm_ep e) <-> ep2p e.
- Proof.
-  induction e; simpl; repeat (rewrite norm_ez_correct); intuition.
- Qed.
-
- Lemma norm_ep_correct2 : 
-  forall e:ExprP, ep2p (norm_ep e) -> ep2p e.
- Proof.
-  intros; destruct (norm_ep_correct e); auto.
- Qed.
-
- Ltac i2z_refl := 
-  i2z_gen;
-  match goal with |- ?t => 
-     let e := p2ep t 
-     in 
-     (change (ep2p e); 
-      apply norm_ep_correct2; 
-      simpl)
-   end.
-
- Ltac iauto := i2z_refl; auto.
- Ltac iomega := i2z_refl; intros; romega.
-
- Open Scope Z_scope.
-
- Lemma max_spec : forall (x y:Z), 
-  x >= y /\ Zmax x y = x  \/
-  x < y /\ Zmax x y = y.
- Proof.
-  intros; unfold Zmax, Zlt, Zge.
-  destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate.
- Qed.
-
- Ltac omega_max_genspec x y := 
-    generalize (max_spec x y); 
-    let z := fresh "z" in let Hz := fresh "Hz" in 
-    (set (z:=Zmax x y); clearbody z).
-
- Ltac omega_max_loop := 
-    match goal with 
-      (* hack: we don't want [i2z (height ...)] to be reduced by romega later... *)
-      | |- context [ i2z (?f ?x) ] => 
-          let i := fresh "i2z" in (set (i:=i2z (f x)); clearbody i); omega_max_loop
-      | |- context [ Zmax ?x ?y ] => omega_max_genspec x y; omega_max_loop
-      | _ => intros
-    end.
-
- Ltac omega_max := i2z_refl; omega_max_loop; try romega.
-
- Ltac false_omega := i2z_refl; intros; romega.
- Ltac false_omega_max := elimtype False; omega_max.
-
- Open Scope Int_scope.
-End MoreInt.
-
-
-(** It's always nice to know that our [Int] interface is realizable :-) *)
-
-Module Z_as_Int <: Int.
- Open Scope Z_scope.
- Definition int := Z.
- Definition _0 := 0.
- Definition _1 := 1.
- Definition _2 := 2.
- Definition _3 := 3.
- Definition plus := Zplus.
- Definition opp := Zopp.
- Definition minus := Zminus.
- Definition mult := Zmult.
- Definition max := Zmax.
- Definition gt_le_dec := Z_gt_le_dec. 
- Definition ge_lt_dec := Z_ge_lt_dec.
- Definition eq_dec := Z_eq_dec.
- Definition i2z : int -> Z := fun n => n.
- Lemma i2z_eq : forall n p, i2z n=i2z p -> n = p. Proof. auto. Qed.
- Lemma i2z_0 : i2z _0 = 0.  Proof. auto. Qed.
- Lemma i2z_1 : i2z _1 = 1.  Proof. auto. Qed.
- Lemma i2z_2 : i2z _2 = 2.  Proof. auto. Qed.
- Lemma i2z_3 : i2z _3 = 3.  Proof. auto. Qed.
- Lemma i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p.  Proof. auto. Qed.
- Lemma i2z_opp : forall n, i2z (- n)  = - i2z n.  Proof. auto. Qed.
- Lemma i2z_minus : forall n p, i2z (n - p)  = i2z n - i2z p.  Proof. auto. Qed.
- Lemma i2z_mult : forall n p, i2z (n * p)  = i2z n * i2z p.  Proof. auto. Qed.
- Lemma i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p). Proof. auto. Qed.
-End Z_as_Int.
-