Library Coq.micromega.Zify
Require
Import
ZifyClasses
.
Require
Export
ZifyInst
.
Require
Import
InitialRing
.
From PreOmega
I) translation of Z.max, Z.min, Z.abs, Z.sgn into recognized equations
Ltac
zify_unop_core
t
thm
a
:=
pose
proof
(
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
=>
let
u
:=
eval
compute
in
(
t
a
)
in
change
(
t
a
)
with
u
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
applySpec
S
:=
let
t
:=
type
of
S
in
match
t
with
| @
BinOpSpec
_
_
?
Op
_
=>
let
Spec
:= (
eval
unfold
S
,
BSpec
in
(@
BSpec
_
_
Op
_
S
))
in
repeat
match
goal
with
|
H
:
context
[
Op
?
X
?
Y
] |-
_
=>
zify_binop
Op
Spec
X
Y
| |-
context
[
Op
?
X
?
Y
] =>
zify_binop
Op
Spec
X
Y
end
| @
UnOpSpec
_
_
?
Op
_
=>
let
Spec
:= (
eval
unfold
S
,
USpec
in
(@
USpec
_
_
Op
_
S
))
in
repeat
match
goal
with
|
H
:
context
[
Op
?
X
] |-
_
=>
zify_unop
Op
Spec
X
| |-
context
[
Op
?
X
] =>
zify_unop
Op
Spec
X
end
end
.
zify_post_hook
is there to be redefined.
Ltac
zify_post_hook
:=
idtac
.
Ltac
zify
:=
zify_op
; (
iter_specs
applySpec
) ;
zify_post_hook
.