blob: 95efde7f5632a90832e03360093037f55082cf14 (
plain)
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
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
Set Implicit Arguments.
Require Import Setoid.
Require Import BinPos.
Require Import Ring_polynom.
Require Import BinList.
Declare ML Module "newring".
(* adds a definition id' on the normal form of t and an hypothesis id
stating that t = id' (tries to produces a proof as small as possible) *)
Ltac compute_assertion id id' t :=
let t' := eval vm_compute in t in
(pose (id' := t');
assert (id : t = id');
[exact_no_check (refl_equal id')|idtac]).
(********************************************************************)
(* Tacticals to build reflexive tactics *)
Ltac OnEquation req :=
match goal with
| |- req ?lhs ?rhs => (fun f => f lhs rhs)
| _ => fail 1 "Goal is not an equation (of expected equality)"
end.
Ltac OnMainSubgoal H ty :=
match ty with
| _ -> ?ty' =>
let subtac := OnMainSubgoal H ty' in
fun tac => lapply H; [clear H; intro H; subtac tac | idtac]
| _ => (fun tac => tac)
end.
Ltac ApplyLemmaAndSimpl tac lemma pe:=
let npe := fresh "ast_nf" in
let H := fresh "eq_nf" in
let Heq := fresh "thm" in
let npe_spec :=
match type of (lemma pe) with
forall npe, ?npe_spec = npe -> _ => npe_spec
| _ => fail 1 "ApplyLemmaAndSimpl: cannot find norm expression"
end in
(compute_assertion H npe npe_spec;
(assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma");
clear H;
OnMainSubgoal Heq ltac:(type of Heq)
ltac:(tac Heq; rewrite Heq; clear Heq npe)).
(* General scheme of reflexive tactics using of correctness lemma
that involves normalisation of one expression *)
Ltac ReflexiveRewriteTactic FV_tac SYN_tac SIMPL_tac lemma2 req rl :=
let R := match type of req with ?R -> _ => R end in
(* build the atom list *)
let fv := list_fold_left FV_tac (@List.nil R) rl in
(* some type-checking to avoid late errors *)
(check_fv fv;
(* rewrite steps *)
list_iter
ltac:(fun r =>
let ast := SYN_tac r fv in
try ApplyLemmaAndSimpl SIMPL_tac (lemma2 fv) ast)
rl).
(********************************************************)
(* An object to return when an expression is not recognized as a constant *)
Definition NotConstant := false.
(* Building the atom list of a ring expression *)
Ltac FV Cst add mul sub opp t fv :=
let rec TFV t fv :=
match Cst t with
| NotConstant =>
match t with
| (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
| (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
| (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
| (opp ?t1) => TFV t1 fv
| _ => AddFvTail t fv
end
| _ => fv
end
in TFV t fv.
(* syntaxification of ring expressions *)
Ltac mkPolexpr C Cst radd rmul rsub ropp t fv :=
let rec mkP t :=
match Cst t with
| NotConstant =>
match t with
| (radd ?t1 ?t2) =>
let e1 := mkP t1 in
let e2 := mkP t2 in constr:(PEadd e1 e2)
| (rmul ?t1 ?t2) =>
let e1 := mkP t1 in
let e2 := mkP t2 in constr:(PEmul e1 e2)
| (rsub ?t1 ?t2) =>
let e1 := mkP t1 in
let e2 := mkP t2 in constr:(PEsub e1 e2)
| (ropp ?t1) =>
let e1 := mkP t1 in constr:(PEopp e1)
| _ =>
let p := Find_at t fv in constr:(PEX C p)
end
| ?c => constr:(PEc c)
end
in mkP t.
(* ring tactics *)
Ltac Ring Cst_tac lemma1 req :=
let Make_tac :=
match type of lemma1 with
| forall (l:list ?R) (pe1 pe2:PExpr ?C),
_ = true ->
req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe1) _ =>
let mkFV := FV Cst_tac add mul sub opp in
let mkPol := mkPolexpr C Cst_tac add mul sub opp in
fun f => f R mkFV mkPol
| _ => fail 1 "ring anomaly: bad correctness lemma"
end in
let Main r1 r2 R mkFV mkPol :=
let fv := mkFV r1 (@List.nil R) in
let fv := mkFV r2 fv in
check_fv fv;
(let pe1 := mkPol r1 fv in
let pe2 := mkPol r2 fv in
apply (lemma1 fv pe1 pe2) || fail "typing error while applying ring";
vm_compute;
exact (refl_equal true) || fail "not a valid ring equation") in
Make_tac ltac:(OnEquation req Main).
Ltac Ring_simplify Cst_tac lemma2 req rl :=
let Make_tac :=
match type of lemma2 with
forall (l:list ?R) (pe:PExpr ?C) (npe:Pol ?C),
_ = npe ->
req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ =>
let mkFV := FV Cst_tac add mul sub opp in
let mkPol := mkPolexpr C Cst_tac add mul sub opp in
let simpl_ring H := protect_fv "ring" in H in
(fun tac => tac mkFV mkPol simpl_ring lemma2 req rl)
| _ => fail 1 "ring anomaly: bad correctness lemma"
end in
Make_tac ReflexiveRewriteTactic.
Tactic Notation (at level 0) "ring" :=
ring_lookup
(fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl =>
pre(); Ring cst_tac lemma1 req).
Tactic Notation (at level 0) "ring_simplify" constr_list(rl) :=
ring_lookup
(fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl =>
pre(); Ring_simplify cst_tac lemma2 req rl; post()) rl.
(* A simple macro tactic to be prefered to ring_simplify *)
Ltac ring_replace t1 t2 := replace t1 with t2 by ring.
|
