summaryrefslogtreecommitdiff
path: root/theories/ZArith/Int.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Int.v')
-rw-r--r--theories/ZArith/Int.v204
1 files changed, 98 insertions, 106 deletions
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<?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:(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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 02:45:43 +0000