From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- theories/ZArith/Int.v | 204 ++++++++++++++++++++++++-------------------------- 1 file changed, 98 insertions(+), 106 deletions(-) (limited to 'theories/ZArith/Int.v') diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index fcb44d6f..30c08fdc 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -6,23 +6,17 @@ (* * 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$ *) -(* $Id: Int.v 10739 2008-04-01 14:45:20Z herbelin $ *) +(** * An light axiomatization of integers (used in FSetAVL). *) -(** 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). +(** 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. +Require Import ZArith. Delimit Scope Int_scope with I. @@ -31,33 +25,33 @@ Delimit Scope Int_scope with I. Module Type Int. Open Scope Int_scope. - - Parameter int : Set. - + + Parameter int : Set. + Parameter i2z : int -> Z. Arguments Scope i2z [ Int_scope ]. - - Parameter _0 : int. - Parameter _1 : int. - Parameter _2 : int. + + Parameter _0 : int. + Parameter _1 : int. + Parameter _2 : int. Parameter _3 : int. - Parameter plus : int -> int -> int. + Parameter plus : int -> int -> int. Parameter opp : int -> int. - Parameter minus : int -> int -> int. + Parameter minus : int -> int -> int. Parameter mult : int -> int -> int. - Parameter max : int -> int -> int. - + Parameter max : int -> int -> int. + Notation "0" := _0 : Int_scope. - Notation "1" := _1 : Int_scope. - Notation "2" := _2 : 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 + (** 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) @@ -70,22 +64,22 @@ Module Type Int. 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 [==] + (** 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 + 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. @@ -99,25 +93,25 @@ Module Type Int. 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. +End Int. (** * 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] + (** A magic (but costly) tactic that goes from [int] back to the [Z] friendly world ... *) - Hint Rewrite -> + 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); + 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 @@ -126,39 +120,39 @@ Module MoreInt (I:Int). (** 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. + (** 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 + + Ltac i2z_gen := match goal with | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); i2z_gen - | H : (eq (A:=int) ?a ?b) |- _ => + | 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 |- _ => + | H : (eq (A:=Z) ?a ?b) |- _ => revert H; i2z_gen + | H : (Zlt ?a ?b) |- _ => revert H; i2z_gen + | H : (Zle ?a ?b) |- _ => revert H; i2z_gen + | H : (Zgt ?a ?b) |- _ => revert H; i2z_gen + | H : (Zge ?a ?b) |- _ => revert H; i2z_gen + | H : _ -> ?X |- _ => (* A [Set] or [Type] part cannot be dealt with easily - using the [ExprP] datatype. So we forget it, leaving + using the [ExprP] datatype. So we forget it, leaving a goal that can be weaker than the original. *) - match type of X with + match type of X with | Type => clear H; i2z_gen - | Prop => generalize H; clear H; i2z_gen + | Prop => revert 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 + | H : _ <-> _ |- _ => revert H; i2z_gen + | H : _ /\ _ |- _ => revert H; i2z_gen + | H : _ \/ _ |- _ => revert H; i2z_gen + | H : ~ _ |- _ => revert H; i2z_gen | _ => idtac end. - Inductive ExprI : Set := + Inductive ExprI : Set := | EI0 : ExprI | EI1 : ExprI - | EI2 : ExprI + | EI2 : ExprI | EI3 : ExprI | EIplus : ExprI -> ExprI -> ExprI | EIopp : ExprI -> ExprI @@ -167,7 +161,7 @@ Module MoreInt (I:Int). | EImax : ExprI -> ExprI -> ExprI | EIraw : int -> ExprI. - Inductive ExprZ : Set := + Inductive ExprZ : Set := | EZplus : ExprZ -> ExprZ -> ExprZ | EZopp : ExprZ -> ExprZ | EZminus : ExprZ -> ExprZ -> ExprZ @@ -176,12 +170,12 @@ Module MoreInt (I:Int). | 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 + 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 @@ -191,8 +185,8 @@ Module MoreInt (I:Int). (** [int] to [ExprI] *) - Ltac i2ei trm := - match constr:trm with + Ltac i2ei trm := + match constr:trm with | 0 => constr:EI0 | 1 => constr:EI1 | 2 => constr:EI2 @@ -207,8 +201,8 @@ Module MoreInt (I:Int). (** [Z] to [ExprZ] *) - with z2ez trm := - match constr:trm with + 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) @@ -219,7 +213,7 @@ Module MoreInt (I:Int). 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) @@ -229,11 +223,11 @@ Module MoreInt (I:Int). | (~ ?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 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:(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. + end. (** [ExprI] to [int] *) @@ -242,19 +236,19 @@ Module MoreInt (I:Int). | EI0 => 0 | EI1 => 1 | EI2 => 2 - | EI3 => 3 + | 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. + | EIraw i => i + end. (** [ExprZ] to [Z] *) - Fixpoint ez2z (e:ExprZ) : Z := - match e with + 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 @@ -266,8 +260,8 @@ Module MoreInt (I:Int). (** [ExprP] to [Prop] *) - Fixpoint ep2p (e:ExprP) : Prop := - match e with + 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 @@ -282,25 +276,25 @@ Module MoreInt (I:Int). end. (** [ExprI] (supposed under a [i2z]) to a simplified [ExprZ] *) - - Fixpoint norm_ei (e:ExprI) : ExprZ := - match e with + + 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) + | 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) + | EIraw i => EZofI (EIraw i) end. (** [ExprZ] to a simplified [ExprZ] *) - Fixpoint norm_ez (e:ExprZ) : ExprZ := - match e with + 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) @@ -311,9 +305,9 @@ Module MoreInt (I:Int). end. (** [ExprP] to a simplified [ExprP] *) - - Fixpoint norm_ep (e:ExprP) : ExprP := - match e with + + 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) @@ -328,38 +322,36 @@ Module MoreInt (I:Int). end. Lemma norm_ei_correct : forall e:ExprI, ez2z (norm_ei e) = i2z (ei2i e). - Proof. + 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. + Qed. - Lemma norm_ep_correct : + 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 : + 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 := + Ltac i2z_refl := i2z_gen; - match goal with |- ?t => - let e := p2ep t in + match goal with |- ?t => + let e := p2ep t in change (ep2p e); apply norm_ep_correct2; simpl end. - (* i2z_refl can be replaced below by (simpl in *; i2z). + (* i2z_refl can be replaced below by (simpl in *; i2z). The reflexive version improves compilation of AVL files by about 15% *) - - Ltac omega_max := i2z_refl; romega with Z. End MoreInt. @@ -381,7 +373,7 @@ Module Z_as_Int <: Int. Definition minus := Zminus. Definition mult := Zmult. Definition max := Zmax. - Definition gt_le_dec := Z_gt_le_dec. + 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. -- cgit v1.2.3