Library Coq.ZArith.Int
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).
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.
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.
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 ...
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.
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.
Anyhow, i2z_refl is enough for applying romega.
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
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
ExprZ to Z
ExprP to Prop
ExprI (supposed under a i2z) to a simplified ExprZ
ExprZ to a simplified ExprZ
ExprP to a simplified ExprP
It's always nice to know that our Int interface is realizable :-)