Library Coq.omega.PreOmega
zify: the Z-ification tactic
I) translation of Zmax, Zmin, Zabs, Zsgn into recognized equations
Ltac zify_unop_core t thm a :=
let H:=
fresh "H"
in assert (
H:=
thm a);
let z :=
fresh "z"
in set (
z:=
t a)
in *;
clearbody z.
Ltac zify_unop_var_or_term t thm a :=
let za :=
fresh "z"
in
(
rename a into za;
rename za into a;
zify_unop_core t thm a) ||
(
remember a as za;
zify_unop_core t thm za).
Ltac zify_unop t thm a :=
let isz :=
isZcst a in
match isz with
|
true =>
simpl (
t a)
in *
|
_ =>
zify_unop_var_or_term t thm a
end.
Ltac zify_unop_nored t thm a :=
let isz :=
isZcst a in
match isz with
|
true =>
zify_unop_core t thm a
|
_ =>
zify_unop_var_or_term t thm a
end.
Ltac zify_binop t thm a b:=
let isza :=
isZcst a in
match isza with
|
true =>
zify_unop (
t a) (
thm a)
b
|
_ =>
let za :=
fresh "z"
in
(
rename a into za;
rename za into a;
zify_unop_nored (
t a) (
thm a)
b) ||
(
remember a as za;
match goal with
|
H :
za = b |-
_ =>
zify_unop_nored (
t za) (
thm za)
za
|
_ =>
zify_unop_nored (
t za) (
thm za)
b
end)
end.
Ltac zify_op_1 :=
match goal with
| |-
context [
Zmax ?
a ?
b ] =>
zify_binop Zmax Zmax_spec a b
|
H :
context [
Zmax ?
a ?
b ] |-
_ =>
zify_binop Zmax Zmax_spec a b
| |-
context [
Zmin ?
a ?
b ] =>
zify_binop Zmin Zmin_spec a b
|
H :
context [
Zmin ?
a ?
b ] |-
_ =>
zify_binop Zmin Zmin_spec a b
| |-
context [
Zsgn ?
a ] =>
zify_unop Zsgn Zsgn_spec a
|
H :
context [
Zsgn ?
a ] |-
_ =>
zify_unop Zsgn Zsgn_spec a
| |-
context [
Zabs ?
a ] =>
zify_unop Zabs Zabs_spec a
|
H :
context [
Zabs ?
a ] |-
_ =>
zify_unop Zabs Zabs_spec a
end.
Ltac zify_op :=
repeat zify_op_1.
II) Conversion from nat to Z
The complete Z-ification tactic
Ltac zify :=
repeat progress (zify_nat; zify_positive; zify_N); zify_op.