diff options
Diffstat (limited to 'theories/ZArith/Int.v')
| -rw-r--r-- | theories/ZArith/Int.v | 673 |
1 files changed, 341 insertions, 332 deletions
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index cb51b9d2..3cee9190 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -7,120 +7,126 @@ (***********************************************************************) (* Finite sets library. - * Authors: Pierre Letouzey and Jean-Christophe Filliâtre - * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id: Int.v 8933 2006-06-09 14:08:38Z herbelin $ *) +(* $Id: Int.v 9319 2006-10-30 12:41:21Z barras $ *) -(** * An axiomatization of integers. *) +(** 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). + 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. + +(** * a specification of integers *) + 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). + 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. +(** * Facts and tactics using [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 ... *) + (** 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. + 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. + 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 *) + (** A reflexive version of the [i2z] tactic *) - (** this [i2z_refl] is actually weaker than [i2z]. For instance, if a + (** 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]. *) @@ -150,228 +156,228 @@ Module MoreInt (I:Int). 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. + | 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. + | 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. + | 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] *) + (** [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. + 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. + Ltac iauto := i2z_refl; auto. + Ltac iomega := i2z_refl; intros; romega. - Open Scope Z_scope. + 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. + 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 := + 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). + (let z := fresh "z" in let Hz := fresh "Hz" in + set (z:=Zmax x y); clearbody z). - Ltac omega_max_loop := + Ltac omega_max_loop := match goal with (* hack: we don't want [i2z (height ...)] to be reduced by romega later... *) | |- context [ i2z (?f ?x) ] => @@ -380,42 +386,45 @@ Module MoreInt (I:Int). | _ => intros end. - Ltac omega_max := i2z_refl; omega_max_loop; try romega. + 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. - Ltac false_omega := i2z_refl; intros; romega. - Ltac false_omega_max := elimtype False; omega_max. - - Open Scope Int_scope. + Open Scope Int_scope. End MoreInt. + +(** * An implementation of [Int] *) + (** 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. + 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. |