Library Coq.ZArith.Int
An light axiomatization of integers (used in FSetAVL).
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.
Delimit Scope Int_scope with I.
a specification of integers
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).
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.
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 ...
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
Z to ExprZ
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 :-)