1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
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 :=
(* Let's introduce the specification theorem for t *)
pose proof (thm a);
(* Then we replace (t a) everywhere with a fresh variable *)
let z := fresh "z" in set (z:=t a) in *; clearbody z.
Ltac zify_unop_var_or_term t thm a :=
(* If a is a variable, no need for aliasing *)
let za := fresh "z" in
(rename a into za; rename za into a; zify_unop_core t thm a) ||
(* Otherwise, a is a complex term: we alias it. *)
(remember a as za; zify_unop_core t thm za).
Ltac zify_unop t thm a :=
(* If a is a scalar, we can simply reduce the unop. *)
(* Note that simpl wasn't enough to reduce [Z.max 0 0] (#5439) *)
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 :=
(* in this version, we don't try to reduce the unop (that can be (Z.add x)) *)
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:=
(* works as zify_unop, except that we should be careful when
dealing with b, since it can be equal to a *)
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.
(* end from PreOmega *)
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.
|
