1
(***********************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
4
(* \VV/ *************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(***********************************************************************)
9
(* Finite sets library.
10
* Authors: Pierre Letouzey and Jean-Christophe Filliâtre
11
* Institution: LRI, CNRS UMR 8623 - Université Paris Sud
12
* 91405 Orsay, France *)
14
(* $Id: Int.v 10739 2008-04-01 14:45:20Z herbelin $ *)
16
(** An axiomatization of integers. *)
18
(** We define a signature for an integer datatype based on [Z].
19
The goal is to allow a switch after extraction to ocaml's
20
[big_int] or even [int] when finiteness isn't a problem
21
(typically : when mesuring the height of an AVL tree).
24
Require Import ZArith.
25
Require Import ROmega.
26
Delimit Scope Int_scope with I.
29
(** * a specification of integers *)
37
Parameter i2z : int -> Z.
38
Arguments Scope i2z [ Int_scope ].
44
Parameter plus : int -> int -> int.
45
Parameter opp : int -> int.
46
Parameter minus : int -> int -> int.
47
Parameter mult : int -> int -> int.
48
Parameter max : int -> int -> int.
50
Notation "0" := _0 : Int_scope.
51
Notation "1" := _1 : Int_scope.
52
Notation "2" := _2 : Int_scope.
53
Notation "3" := _3 : Int_scope.
54
Infix "+" := plus : Int_scope.
55
Infix "-" := minus : Int_scope.
56
Infix "*" := mult : Int_scope.
57
Notation "- x" := (opp x) : Int_scope.
59
(** For logical relations, we can rely on their counterparts in Z,
60
since they don't appear after extraction. Moreover, using tactics
61
like omega is easier this way. *)
63
Notation "x == y" := (i2z x = i2z y)
64
(at level 70, y at next level, no associativity) : Int_scope.
65
Notation "x <= y" := (Zle (i2z x) (i2z y)): Int_scope.
66
Notation "x < y" := (Zlt (i2z x) (i2z y)) : Int_scope.
67
Notation "x >= y" := (Zge (i2z x) (i2z y)) : Int_scope.
68
Notation "x > y" := (Zgt (i2z x) (i2z y)): Int_scope.
69
Notation "x <= y <= z" := (x <= y /\ y <= z) : Int_scope.
70
Notation "x <= y < z" := (x <= y /\ y < z) : Int_scope.
71
Notation "x < y < z" := (x < y /\ y < z) : Int_scope.
72
Notation "x < y <= z" := (x < y /\ y <= z) : Int_scope.
74
(** Some decidability fonctions (informative). *)
76
Axiom gt_le_dec : forall x y: int, {x > y} + {x <= y}.
77
Axiom ge_lt_dec : forall x y : int, {x >= y} + {x < y}.
78
Axiom eq_dec : forall x y : int, { x == y } + {~ x==y }.
82
(** First, we ask [i2z] to be injective. Said otherwise, our ad-hoc equality
83
[==] and the generic [=] are in fact equivalent. We define [==]
84
nonetheless since the translation to [Z] for using automatic tactic is easier. *)
86
Axiom i2z_eq : forall n p : int, n == p -> n = p.
88
(** Then, we express the specifications of the above parameters using their
92
Axiom i2z_0 : i2z _0 = 0.
93
Axiom i2z_1 : i2z _1 = 1.
94
Axiom i2z_2 : i2z _2 = 2.
95
Axiom i2z_3 : i2z _3 = 3.
96
Axiom i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p.
97
Axiom i2z_opp : forall n, i2z (-n) = -i2z n.
98
Axiom i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p.
99
Axiom i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p.
100
Axiom i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p).
105
(** * Facts and tactics using [Int] *)
107
Module MoreInt (I:Int).
110
Open Scope Int_scope.
112
(** A magic (but costly) tactic that goes from [int] back to the [Z]
113
friendly world ... *)
116
i2z_0 i2z_1 i2z_2 i2z_3 i2z_plus i2z_opp i2z_minus i2z_mult i2z_max : i2z.
118
Ltac i2z := match goal with
119
| H : (eq (A:=int) ?a ?b) |- _ =>
120
generalize (f_equal i2z H);
121
try autorewrite with i2z; clear H; intro H; i2z
122
| |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); try autorewrite with i2z; i2z
123
| H : _ |- _ => progress autorewrite with i2z in H; i2z
124
| _ => try autorewrite with i2z
127
(** A reflexive version of the [i2z] tactic *)
129
(** this [i2z_refl] is actually weaker than [i2z]. For instance, if a
130
[i2z] is buried deep inside a subterm, [i2z_refl] may miss it.
131
See also the limitation about [Set] or [Type] part below.
132
Anyhow, [i2z_refl] is enough for applying [romega]. *)
134
Ltac i2z_gen := match goal with
135
| |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); i2z_gen
136
| H : (eq (A:=int) ?a ?b) |- _ =>
137
generalize (f_equal i2z H); clear H; i2z_gen
138
| H : (eq (A:=Z) ?a ?b) |- _ => generalize H; clear H; i2z_gen
139
| H : (Zlt ?a ?b) |- _ => generalize H; clear H; i2z_gen
140
| H : (Zle ?a ?b) |- _ => generalize H; clear H; i2z_gen
141
| H : (Zgt ?a ?b) |- _ => generalize H; clear H; i2z_gen
142
| H : (Zge ?a ?b) |- _ => generalize H; clear H; i2z_gen
143
| H : _ -> ?X |- _ =>
144
(* A [Set] or [Type] part cannot be dealt with easily
145
using the [ExprP] datatype. So we forget it, leaving
146
a goal that can be weaker than the original. *)
148
| Type => clear H; i2z_gen
149
| Prop => generalize H; clear H; i2z_gen
151
| H : _ <-> _ |- _ => generalize H; clear H; i2z_gen
152
| H : _ /\ _ |- _ => generalize H; clear H; i2z_gen
153
| H : _ \/ _ |- _ => generalize H; clear H; i2z_gen
154
| H : ~ _ |- _ => generalize H; clear H; i2z_gen
158
Inductive ExprI : Set :=
163
| EIplus : ExprI -> ExprI -> ExprI
164
| EIopp : ExprI -> ExprI
165
| EIminus : ExprI -> ExprI -> ExprI
166
| EImult : ExprI -> ExprI -> ExprI
167
| EImax : ExprI -> ExprI -> ExprI
168
| EIraw : int -> ExprI.
170
Inductive ExprZ : Set :=
171
| EZplus : ExprZ -> ExprZ -> ExprZ
172
| EZopp : ExprZ -> ExprZ
173
| EZminus : ExprZ -> ExprZ -> ExprZ
174
| EZmult : ExprZ -> ExprZ -> ExprZ
175
| EZmax : ExprZ -> ExprZ -> ExprZ
176
| EZofI : ExprI -> ExprZ
177
| EZraw : Z -> ExprZ.
179
Inductive ExprP : Type :=
180
| EPeq : ExprZ -> ExprZ -> ExprP
181
| EPlt : ExprZ -> ExprZ -> ExprP
182
| EPle : ExprZ -> ExprZ -> ExprP
183
| EPgt : ExprZ -> ExprZ -> ExprP
184
| EPge : ExprZ -> ExprZ -> ExprP
185
| EPimpl : ExprP -> ExprP -> ExprP
186
| EPequiv : ExprP -> ExprP -> ExprP
187
| EPand : ExprP -> ExprP -> ExprP
188
| EPor : ExprP -> ExprP -> ExprP
189
| EPneg : ExprP -> ExprP
190
| EPraw : Prop -> ExprP.
192
(** [int] to [ExprI] *)
195
match constr:trm with
200
| ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIplus ex ey)
201
| ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIminus ex ey)
202
| ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImult ex ey)
203
| max ?x ?y => let ex := i2ei x with ey := i2ei y in constr:(EImax ex ey)
204
| - ?x => let ex := i2ei x in constr:(EIopp ex)
205
| ?x => constr:(EIraw x)
208
(** [Z] to [ExprZ] *)
211
match constr:trm with
212
| (?x+?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZplus ex ey)
213
| (?x-?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZminus ex ey)
214
| (?x*?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmult ex ey)
215
| (Zmax ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EZmax ex ey)
216
| (-?x)%Z => let ex := z2ez x in constr:(EZopp ex)
217
| i2z ?x => let ex := i2ei x in constr:(EZofI ex)
218
| ?x => constr:(EZraw x)
221
(** [Prop] to [ExprP] *)
224
match constr:trm with
225
| (?x <-> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPequiv ex ey)
226
| (?x -> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPimpl ex ey)
227
| (?x /\ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPand ex ey)
228
| (?x \/ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPor ex ey)
229
| (~ ?x) => let ex := p2ep x in constr:(EPneg ex)
230
| (eq (A:=Z) ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EPeq ex ey)
231
| (?x<?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPlt ex ey)
232
| (?x<=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPle ex ey)
233
| (?x>?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPgt ex ey)
234
| (?x>=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPge ex ey)
235
| ?x => constr:(EPraw x)
238
(** [ExprI] to [int] *)
240
Fixpoint ei2i (e:ExprI) : int :=
246
| EIplus e1 e2 => (ei2i e1)+(ei2i e2)
247
| EIminus e1 e2 => (ei2i e1)-(ei2i e2)
248
| EImult e1 e2 => (ei2i e1)*(ei2i e2)
249
| EImax e1 e2 => max (ei2i e1) (ei2i e2)
250
| EIopp e => -(ei2i e)
254
(** [ExprZ] to [Z] *)
256
Fixpoint ez2z (e:ExprZ) : Z :=
258
| EZplus e1 e2 => ((ez2z e1)+(ez2z e2))%Z
259
| EZminus e1 e2 => ((ez2z e1)-(ez2z e2))%Z
260
| EZmult e1 e2 => ((ez2z e1)*(ez2z e2))%Z
261
| EZmax e1 e2 => Zmax (ez2z e1) (ez2z e2)
262
| EZopp e => (-(ez2z e))%Z
263
| EZofI e => i2z (ei2i e)
267
(** [ExprP] to [Prop] *)
269
Fixpoint ep2p (e:ExprP) : Prop :=
271
| EPeq e1 e2 => (ez2z e1) = (ez2z e2)
272
| EPlt e1 e2 => ((ez2z e1)<(ez2z e2))%Z
273
| EPle e1 e2 => ((ez2z e1)<=(ez2z e2))%Z
274
| EPgt e1 e2 => ((ez2z e1)>(ez2z e2))%Z
275
| EPge e1 e2 => ((ez2z e1)>=(ez2z e2))%Z
276
| EPimpl e1 e2 => (ep2p e1) -> (ep2p e2)
277
| EPequiv e1 e2 => (ep2p e1) <-> (ep2p e2)
278
| EPand e1 e2 => (ep2p e1) /\ (ep2p e2)
279
| EPor e1 e2 => (ep2p e1) \/ (ep2p e2)
280
| EPneg e => ~ (ep2p e)
284
(** [ExprI] (supposed under a [i2z]) to a simplified [ExprZ] *)
286
Fixpoint norm_ei (e:ExprI) : ExprZ :=
292
| EIplus e1 e2 => EZplus (norm_ei e1) (norm_ei e2)
293
| EIminus e1 e2 => EZminus (norm_ei e1) (norm_ei e2)
294
| EImult e1 e2 => EZmult (norm_ei e1) (norm_ei e2)
295
| EImax e1 e2 => EZmax (norm_ei e1) (norm_ei e2)
296
| EIopp e => EZopp (norm_ei e)
297
| EIraw i => EZofI (EIraw i)
300
(** [ExprZ] to a simplified [ExprZ] *)
302
Fixpoint norm_ez (e:ExprZ) : ExprZ :=
304
| EZplus e1 e2 => EZplus (norm_ez e1) (norm_ez e2)
305
| EZminus e1 e2 => EZminus (norm_ez e1) (norm_ez e2)
306
| EZmult e1 e2 => EZmult (norm_ez e1) (norm_ez e2)
307
| EZmax e1 e2 => EZmax (norm_ez e1) (norm_ez e2)
308
| EZopp e => EZopp (norm_ez e)
309
| EZofI e => norm_ei e
313
(** [ExprP] to a simplified [ExprP] *)
315
Fixpoint norm_ep (e:ExprP) : ExprP :=
317
| EPeq e1 e2 => EPeq (norm_ez e1) (norm_ez e2)
318
| EPlt e1 e2 => EPlt (norm_ez e1) (norm_ez e2)
319
| EPle e1 e2 => EPle (norm_ez e1) (norm_ez e2)
320
| EPgt e1 e2 => EPgt (norm_ez e1) (norm_ez e2)
321
| EPge e1 e2 => EPge (norm_ez e1) (norm_ez e2)
322
| EPimpl e1 e2 => EPimpl (norm_ep e1) (norm_ep e2)
323
| EPequiv e1 e2 => EPequiv (norm_ep e1) (norm_ep e2)
324
| EPand e1 e2 => EPand (norm_ep e1) (norm_ep e2)
325
| EPor e1 e2 => EPor (norm_ep e1) (norm_ep e2)
326
| EPneg e => EPneg (norm_ep e)
330
Lemma norm_ei_correct : forall e:ExprI, ez2z (norm_ei e) = i2z (ei2i e).
332
induction e; simpl; intros; i2z; auto; try congruence.
335
Lemma norm_ez_correct : forall e:ExprZ, ez2z (norm_ez e) = ez2z e.
337
induction e; simpl; intros; i2z; auto; try congruence; apply norm_ei_correct.
340
Lemma norm_ep_correct :
341
forall e:ExprP, ep2p (norm_ep e) <-> ep2p e.
343
induction e; simpl; repeat (rewrite norm_ez_correct); intuition.
346
Lemma norm_ep_correct2 :
347
forall e:ExprP, ep2p (norm_ep e) -> ep2p e.
349
intros; destruct (norm_ep_correct e); auto.
354
match goal with |- ?t =>
356
change (ep2p e); apply norm_ep_correct2; simpl
359
(* i2z_refl can be replaced below by (simpl in *; i2z).
360
The reflexive version improves compilation of AVL files by about 15% *)
362
Ltac omega_max := i2z_refl; romega with Z.
368
(** * An implementation of [Int] *)
370
(** It's always nice to know that our [Int] interface is realizable :-) *)
372
Module Z_as_Int <: Int.
379
Definition plus := Zplus.
380
Definition opp := Zopp.
381
Definition minus := Zminus.
382
Definition mult := Zmult.
383
Definition max := Zmax.
384
Definition gt_le_dec := Z_gt_le_dec.
385
Definition ge_lt_dec := Z_ge_lt_dec.
386
Definition eq_dec := Z_eq_dec.
387
Definition i2z : int -> Z := fun n => n.
388
Lemma i2z_eq : forall n p, i2z n=i2z p -> n = p. Proof. auto. Qed.
389
Lemma i2z_0 : i2z _0 = 0. Proof. auto. Qed.
390
Lemma i2z_1 : i2z _1 = 1. Proof. auto. Qed.
391
Lemma i2z_2 : i2z _2 = 2. Proof. auto. Qed.
392
Lemma i2z_3 : i2z _3 = 3. Proof. auto. Qed.
393
Lemma i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p. Proof. auto. Qed.
394
Lemma i2z_opp : forall n, i2z (- n) = - i2z n. Proof. auto. Qed.
395
Lemma i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p. Proof. auto. Qed.
396
Lemma i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p. Proof. auto. Qed.
397
Lemma i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p). Proof. auto. Qed.
added
removed
theories/ZArith/Int.v
