diff options
Diffstat (limited to 'theories/ZArith/Int.v')
| -rw-r--r-- | theories/ZArith/Int.v | 193 |
1 files changed, 131 insertions, 62 deletions
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 99ecd150..d210792f 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(** * An light axiomatization of integers (used in FSetAVL). *) +(** * An light axiomatization of integers (used in MSetAVL). *) (** We define a signature for an integer datatype based on [Z]. The goal is to allow a switch after extraction to ocaml's @@ -14,11 +14,11 @@ (typically : when mesuring the height of an AVL tree). *) -Require Import ZArith. +Require Import BinInt. Delimit Scope Int_scope with I. Local Open Scope Int_scope. -(** * a specification of integers *) +(** * A specification of integers *) Module Type Int. @@ -31,19 +31,19 @@ Module Type Int. Parameter _1 : t. Parameter _2 : t. Parameter _3 : t. - Parameter plus : t -> t -> t. + Parameter add : t -> t -> t. Parameter opp : t -> t. - Parameter minus : t -> t -> t. - Parameter mult : t -> t -> t. + Parameter sub : t -> t -> t. + Parameter mul : t -> t -> t. Parameter max : t -> t -> t. 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. + Infix "+" := add : Int_scope. + Infix "-" := sub : Int_scope. + Infix "*" := mul : Int_scope. Notation "- x" := (opp x) : Int_scope. (** For logical relations, we can rely on their counterparts in Z, @@ -61,7 +61,17 @@ Module Type Int. Notation "x < y < z" := (x < y /\ y < z) : Int_scope. Notation "x < y <= z" := (x < y /\ y <= z) : Int_scope. - (** Some decidability fonctions (informative). *) + (** Informative comparisons. *) + + Axiom eqb : t -> t -> bool. + Axiom ltb : t -> t -> bool. + Axiom leb : t -> t -> bool. + + Infix "=?" := eqb. + Infix "<?" := ltb. + Infix "<=?" := leb. + + (** For compatibility, some decidability fonctions (informative). *) Axiom gt_le_dec : forall x y : t, {x > y} + {x <= y}. Axiom ge_lt_dec : forall x y : t, {x >= y} + {x < y}. @@ -83,11 +93,14 @@ Module Type Int. Axiom i2z_1 : i2z _1 = 1%Z. Axiom i2z_2 : i2z _2 = 2%Z. Axiom i2z_3 : i2z _3 = 3%Z. - Axiom i2z_plus : forall n p, i2z (n + p) = (i2z n + i2z p)%Z. + Axiom i2z_add : forall n p, i2z (n + p) = (i2z n + i2z p)%Z. Axiom i2z_opp : forall n, i2z (-n) = (-i2z n)%Z. - Axiom i2z_minus : forall n p, i2z (n - p) = (i2z n - i2z p)%Z. - Axiom i2z_mult : forall n p, i2z (n * p) = (i2z n * i2z p)%Z. + Axiom i2z_sub : forall n p, i2z (n - p) = (i2z n - i2z p)%Z. + Axiom i2z_mul : forall n p, i2z (n * p) = (i2z n * i2z p)%Z. Axiom i2z_max : forall n p, i2z (max n p) = Z.max (i2z n) (i2z p). + Axiom i2z_eqb : forall n p, eqb n p = Z.eqb (i2z n) (i2z p). + Axiom i2z_ltb : forall n p, ltb n p = Z.ltb (i2z n) (i2z p). + Axiom i2z_leb : forall n p, leb n p = Z.leb (i2z n) (i2z p). End Int. @@ -97,11 +110,42 @@ End Int. Module MoreInt (Import I:Int). Local Notation int := I.t. + Lemma eqb_eq n p : (n =? p) = true <-> n == p. + Proof. + now rewrite i2z_eqb, Z.eqb_eq. + Qed. + + Lemma eqb_neq n p : (n =? p) = false <-> ~(n == p). + Proof. + rewrite <- eqb_eq. destruct (n =? p); intuition. + Qed. + + Lemma ltb_lt n p : (n <? p) = true <-> n < p. + Proof. + now rewrite i2z_ltb, Z.ltb_lt. + Qed. + + Lemma ltb_nlt n p : (n <? p) = false <-> ~(n < p). + Proof. + rewrite <- ltb_lt. destruct (n <? p); intuition. + Qed. + + Lemma leb_le n p : (n <=? p) = true <-> n <= p. + Proof. + now rewrite i2z_leb, Z.leb_le. + Qed. + + Lemma leb_nle n p : (n <=? p) = false <-> ~(n <= p). + Proof. + rewrite <- leb_le. destruct (n <=? p); intuition. + Qed. + (** 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. + i2z_0 i2z_1 i2z_2 i2z_3 i2z_add i2z_opp i2z_sub i2z_mul i2z_max + i2z_eqb i2z_ltb i2z_leb : i2z. Ltac i2z := match goal with | H : ?a = ?b |- _ => @@ -149,18 +193,18 @@ Module MoreInt (Import I:Int). | EI1 : ExprI | EI2 : ExprI | EI3 : ExprI - | EIplus : ExprI -> ExprI -> ExprI + | EIadd : ExprI -> ExprI -> ExprI | EIopp : ExprI -> ExprI - | EIminus : ExprI -> ExprI -> ExprI - | EImult : ExprI -> ExprI -> ExprI + | EIsub : ExprI -> ExprI -> ExprI + | EImul : ExprI -> ExprI -> ExprI | EImax : ExprI -> ExprI -> ExprI | EIraw : int -> ExprI. Inductive ExprZ : Set := - | EZplus : ExprZ -> ExprZ -> ExprZ + | EZadd : ExprZ -> ExprZ -> ExprZ | EZopp : ExprZ -> ExprZ - | EZminus : ExprZ -> ExprZ -> ExprZ - | EZmult : ExprZ -> ExprZ -> ExprZ + | EZsub : ExprZ -> ExprZ -> ExprZ + | EZmul : ExprZ -> ExprZ -> ExprZ | EZmax : ExprZ -> ExprZ -> ExprZ | EZofI : ExprI -> ExprZ | EZraw : Z -> ExprZ. @@ -186,9 +230,9 @@ Module MoreInt (Import I:Int). | 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) + | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIadd ex ey) + | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIsub ex ey) + | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImul 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) @@ -198,9 +242,9 @@ Module MoreInt (Import I:Int). 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) + | (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZadd ex ey) + | (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZsub ex ey) + | (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmul ex ey) | (Z.max ?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) @@ -232,9 +276,9 @@ Module MoreInt (Import I:Int). | 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) + | EIadd e1 e2 => (ei2i e1)+(ei2i e2) + | EIsub e1 e2 => (ei2i e1)-(ei2i e2) + | EImul e1 e2 => (ei2i e1)*(ei2i e2) | EImax e1 e2 => max (ei2i e1) (ei2i e2) | EIopp e => -(ei2i e) | EIraw i => i @@ -244,9 +288,9 @@ Module MoreInt (Import I:Int). 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 + | EZadd e1 e2 => ((ez2z e1)+(ez2z e2))%Z + | EZsub e1 e2 => ((ez2z e1)-(ez2z e2))%Z + | EZmul e1 e2 => ((ez2z e1)*(ez2z e2))%Z | EZmax e1 e2 => Z.max (ez2z e1) (ez2z e2) | EZopp e => (-(ez2z e))%Z | EZofI e => i2z (ei2i e) @@ -278,9 +322,9 @@ Module MoreInt (Import I:Int). | 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) + | EIadd e1 e2 => EZadd (norm_ei e1) (norm_ei e2) + | EIsub e1 e2 => EZsub (norm_ei e1) (norm_ei e2) + | EImul e1 e2 => EZmul (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) @@ -290,9 +334,9 @@ Module MoreInt (Import I:Int). 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) + | EZadd e1 e2 => EZadd (norm_ez e1) (norm_ez e2) + | EZsub e1 e2 => EZsub (norm_ez e1) (norm_ez e2) + | EZmul e1 e2 => EZmul (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 @@ -316,24 +360,22 @@ Module MoreInt (Import I:Int). | EPraw p => EPraw p end. - Lemma norm_ei_correct : forall e:ExprI, ez2z (norm_ei e) = i2z (ei2i e). + Lemma norm_ei_correct (e:ExprI) : ez2z (norm_ei e) = i2z (ei2i e). Proof. - induction e; simpl; intros; i2z; auto; try congruence. + induction e; simpl; i2z; auto; try congruence. Qed. - Lemma norm_ez_correct : forall e:ExprZ, ez2z (norm_ez e) = ez2z e. + Lemma norm_ez_correct (e:ExprZ) : ez2z (norm_ez e) = ez2z e. Proof. - induction e; simpl; intros; i2z; auto; try congruence; apply norm_ei_correct. + induction e; simpl; i2z; auto; try congruence; apply norm_ei_correct. Qed. - Lemma norm_ep_correct : - forall e:ExprP, ep2p (norm_ep e) <-> ep2p e. + Lemma norm_ep_correct (e:ExprP) : ep2p (norm_ep e) <-> ep2p e. Proof. - induction e; simpl; repeat (rewrite norm_ez_correct); intuition. + induction e; simpl; rewrite ?norm_ez_correct; intuition. Qed. - Lemma norm_ep_correct2 : - forall e:ExprP, ep2p (norm_ep e) -> ep2p e. + Lemma norm_ep_correct2 (e:ExprP) : ep2p (norm_ep e) -> ep2p e. Proof. intros; destruct (norm_ep_correct e); auto. Qed. @@ -363,23 +405,50 @@ Module Z_as_Int <: Int. Definition _1 := 1. Definition _2 := 2. Definition _3 := 3. - Definition plus := Z.add. + Definition add := Z.add. Definition opp := Z.opp. - Definition minus := Z.sub. - Definition mult := Z.mul. + Definition sub := Z.sub. + Definition mul := Z.mul. Definition max := Z.max. - Definition gt_le_dec := Z_gt_le_dec. - Definition ge_lt_dec := Z_ge_lt_dec. + Definition eqb := Z.eqb. + Definition ltb := Z.ltb. + Definition leb := Z.leb. + Definition eq_dec := Z.eq_dec. + Definition gt_le_dec i j : {i > j} + { i <= j }. + Proof. + generalize (Z.ltb_spec j i). + destruct (j <? i); [left|right]; inversion H; trivial. + now apply Z.lt_gt. + Defined. + Definition ge_lt_dec i j : {i >= j} + { i < j }. + Proof. + generalize (Z.ltb_spec i j). + destruct (i <? j); [right|left]; inversion H; trivial. + now apply Z.le_ge. + Defined. + Definition i2z : t -> 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 n p : i2z (n + p) = i2z n + i2z p. Proof. auto. Qed. - Lemma i2z_opp n : i2z (- n) = - i2z n. Proof. auto. Qed. - Lemma i2z_minus n p : i2z (n - p) = i2z n - i2z p. Proof. auto. Qed. - Lemma i2z_mult n p : i2z (n * p) = i2z n * i2z p. Proof. auto. Qed. - Lemma i2z_max n p : i2z (max n p) = Z.max (i2z n) (i2z p). Proof. auto. Qed. + Lemma i2z_eq n p : i2z n = i2z p -> n = p. Proof. trivial. Qed. + Lemma i2z_0 : i2z _0 = 0. Proof. reflexivity. Qed. + Lemma i2z_1 : i2z _1 = 1. Proof. reflexivity. Qed. + Lemma i2z_2 : i2z _2 = 2. Proof. reflexivity. Qed. + Lemma i2z_3 : i2z _3 = 3. Proof. reflexivity. Qed. + Lemma i2z_add n p : i2z (n + p) = i2z n + i2z p. + Proof. reflexivity. Qed. + Lemma i2z_opp n : i2z (- n) = - i2z n. + Proof. reflexivity. Qed. + Lemma i2z_sub n p : i2z (n - p) = i2z n - i2z p. + Proof. reflexivity. Qed. + Lemma i2z_mul n p : i2z (n * p) = i2z n * i2z p. + Proof. reflexivity. Qed. + Lemma i2z_max n p : i2z (max n p) = Z.max (i2z n) (i2z p). + Proof. reflexivity. Qed. + Lemma i2z_eqb n p : eqb n p = Z.eqb (i2z n) (i2z p). + Proof. reflexivity. Qed. + Lemma i2z_leb n p : leb n p = Z.leb (i2z n) (i2z p). + Proof. reflexivity. Qed. + Lemma i2z_ltb n p : ltb n p = Z.ltb (i2z n) (i2z p). + Proof. reflexivity. Qed. + End Z_as_Int. |