1
Set Implicit Arguments.
4
Require Import Ring_polynom.
5
Require Import BinList.
6
Require Import InitialRing.
9
(* adds a definition id' on the normal form of t and an hypothesis id
10
stating that t = id' (tries to produces a proof as small as possible) *)
11
Ltac compute_assertion id id' t :=
12
let t' := eval vm_compute in t in
14
assert (id : t = id');
15
[vm_cast_no_check (refl_equal id')|idtac].
16
(* [exact_no_check (refl_equal id'<: t = id')|idtac]). *)
18
(********************************************************************)
19
(* Tacticals to build reflexive tactics *)
21
Ltac OnEquation req :=
23
| |- req ?lhs ?rhs => (fun f => f lhs rhs)
24
| _ => fail 1 "Goal is not an equation (of expected equality)"
27
Ltac OnMainSubgoal H ty :=
30
let subtac := OnMainSubgoal H ty' in
31
fun tac => lapply H; [clear H; intro H; subtac tac | idtac]
32
| _ => (fun tac => tac)
35
Ltac ApplyLemmaThen lemma expr tac :=
36
let nexpr := fresh "expr_nf" in
37
let H := fresh "eq_nf" in
38
let Heq := fresh "thm" in
40
match type of (lemma expr) with
41
forall x, ?nf_spec = x -> _ => nf_spec
42
| _ => fail 1 "ApplyLemmaThen: cannot find norm expression"
44
compute_assertion H nexpr nf_spec;
45
assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma";
47
OnMainSubgoal Heq ltac:(type of Heq) ltac:(tac Heq; clear Heq nexpr).
49
Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg :=
50
let npe := fresh "expr_nf" in
51
let H := fresh "eq_nf" in
52
let Heq := fresh "thm" in
54
match type of (lemma expr) with
55
forall npe, ?npe_spec = npe -> _ => npe_spec
56
| _ => fail 1 "ApplyLemmaThenAndCont: cannot find norm expression"
58
(compute_assertion H npe npe_spec;
59
(assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma");
61
OnMainSubgoal Heq ltac:(type of Heq)
62
ltac:(try tac Heq; clear Heq npe;CONT_tac cont_arg)).
64
(* General scheme of reflexive tactics using of correctness lemma
65
that involves normalisation of one expression *)
67
Ltac ReflexiveRewriteTactic FV_tac SYN_tac MAIN_tac LEMMA_tac fv terms :=
68
(* extend the atom list *)
69
let fv := list_fold_left FV_tac fv terms in
71
let fcons term CONT_tac cont_arg :=
72
let expr := SYN_tac term fv in
73
(ApplyLemmaThenAndCont lemma expr MAIN_tac CONT_tac cont_arg) in
75
lazy_list_fold_right fcons ltac:(idtac) terms in
78
(********************************************************)
81
(* Building the atom list of a ring expression *)
82
Ltac FV Cst CstPow add mul sub opp pow t fv :=
87
| (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
88
| (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
89
| (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
90
| (opp ?t1) => TFV t1 fv
93
| InitialRing.NotConstant => AddFvTail t fv
102
(* syntaxification of ring expressions *)
103
Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv :=
107
| InitialRing.NotConstant =>
112
let e2 := mkP t2 in constr:(PEadd e1 e2)
116
let e2 := mkP t2 in constr:(PEmul e1 e2)
120
let e2 := mkP t2 in constr:(PEsub e1 e2)
123
let e1 := mkP t1 in constr:(PEopp e1)
126
| InitialRing.NotConstant =>
127
fun _ => let p := Find_at t fv in constr:(PEX C p)
128
| ?c => fun _ => let e1 := mkP t1 in constr:(PEpow e1 c)
131
fun _ => let p := Find_at t fv in constr:(PEX C p)
133
| ?c => fun _ => constr:(@PEc C c)
138
Ltac ParseRingComponents lemma :=
139
match type of lemma with
140
| context [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
141
(fun f => f R add mul sub opp pow C)
142
| _ => fail 1 "ring anomaly: bad correctness lemma (parse)"
147
Ltac relation_carrier req :=
148
let ty := type of req in
149
match eval hnf in ty with
151
| _ => fail 1000 "Equality has no relation type"
154
Ltac FV_hypo_tac mkFV req lH :=
155
let R := relation_carrier req in
156
let FV_hypo_l_tac h :=
157
match h with @mkhypo (req ?pe _) _ => mkFV pe end in
158
let FV_hypo_r_tac h :=
159
match h with @mkhypo (req _ ?pe) _ => mkFV pe end in
160
let fv := list_fold_right FV_hypo_l_tac (@nil R) lH in
161
list_fold_right FV_hypo_r_tac fv lH.
163
Ltac mkHyp_tac C req mkPE lH :=
166
| @mkhypo (req ?r1 ?r2) _ =>
167
let pe1 := mkPE r1 in
168
let pe2 := mkPE r2 in
169
constr:(cons (pe1,pe2) res)
170
| _ => fail 1 "hypothesis is not a ring equality"
172
list_fold_right mkHyp (@nil (PExpr C * PExpr C)) lH.
174
Ltac proofHyp_tac lH :=
182
| cons ?h nil => get_proof h
184
let l := get_proof h in
190
Definition ring_subst_niter := (10*10*10)%nat.
192
Ltac Ring Cst_tac CstPow_tac lemma1 req n lH :=
193
let Main lhs rhs R radd rmul rsub ropp rpow C :=
194
let mkFV := FV Cst_tac CstPow_tac radd rmul rsub ropp rpow in
195
let mkPol := mkPolexpr C Cst_tac CstPow_tac radd rmul rsub ropp rpow in
196
let fv := FV_hypo_tac mkFV req lH in
197
let fv := mkFV lhs fv in
198
let fv := mkFV rhs fv in
200
let pe1 := mkPol lhs fv in
201
let pe2 := mkPol rhs fv in
202
let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
203
let vlpe := fresh "hyp_list" in
204
let vfv := fresh "fv_list" in
207
(apply (lemma1 n vfv vlpe pe1 pe2)
208
|| fail "typing error while applying ring");
209
[ ((let prh := proofHyp_tac lH in exact prh)
210
|| idtac "can not automatically proof hypothesis : maybe a left member of a hypothesis is not a monomial")
212
(exact (refl_equal true) || fail "not a valid ring equation")] in
213
ParseRingComponents lemma1 ltac:(OnEquation req Main).
215
Ltac Ring_norm_gen f Cst_tac CstPow_tac lemma2 req n lH rl :=
216
let Main R add mul sub opp pow C :=
217
let mkFV := FV Cst_tac CstPow_tac add mul sub opp pow in
218
let mkPol := mkPolexpr C Cst_tac CstPow_tac add mul sub opp pow in
219
let fv := FV_hypo_tac mkFV req lH in
220
let simpl_ring H := (protect_fv "ring" in H; f H) in
221
let lemma_tac fv RW_tac :=
222
let rr_lemma := fresh "r_rw_lemma" in
223
let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
224
let vlpe := fresh "list_hyp" in
225
let vlmp := fresh "list_hyp_norm" in
226
let vlmp_eq := fresh "list_hyp_norm_eq" in
227
let prh := proofHyp_tac lH in
229
match type of lemma2 with
230
| context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?cdiv ?ceqb _]
232
compute_assertion vlmp_eq vlmp
233
(mk_monpol_list cO cI cadd cmul csub copp cdiv ceqb vlpe);
234
(assert (rr_lemma := lemma2 n vlpe fv prh vlmp vlmp_eq)
235
|| fail 1 "type error when build the rewriting lemma");
237
try clear rr_lemma vlmp_eq vlmp vlpe
238
| _ => fail 1 "ring_simplify anomaly: bad correctness lemma"
240
ReflexiveRewriteTactic mkFV mkPol simpl_ring lemma_tac fv rl in
241
ParseRingComponents lemma2 Main.
245
req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl :=
246
pre();Ring cst_tac pow_tac lemma1 req ring_subst_niter lH.
248
Ltac Get_goal := match goal with [|- ?G] => G end.
250
Tactic Notation (at level 0) "ring" :=
252
ring_lookup Ring_gen [] G.
254
Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" :=
256
ring_lookup Ring_gen [lH] G.
260
Ltac Ring_simplify_gen f :=
261
fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
262
let l := fresh "to_rewrite" in
264
generalize (refl_equal l);
268
let Heq := fresh "Heq" in
269
intros Heq;clear Heq l;
270
Ring_norm_gen f cst_tac pow_tac lemma2 req ring_subst_niter lH RL;
274
| [|- l = ?RL -> _ ] => (fun f => f RL)
275
| _ => fail 1 "ring_simplify anomaly: bad goal after pre"
279
Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H).
281
Tactic Notation (at level 0) "ring_simplify" constr_list(rl) :=
283
ring_lookup Ring_simplify [] rl G.
285
Tactic Notation (at level 0)
286
"ring_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
288
ring_lookup Ring_simplify [lH] rl G.
290
(* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *)
292
Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):=
294
let t := type of H in
295
let g := fresh "goal" in
297
generalize H;clear H;
298
ring_lookup Ring_simplify [] rl t;
303
"ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):=
305
let t := type of H in
306
let g := fresh "goal" in
308
generalize H;clear H;
309
ring_lookup Ring_simplify [lH] rl t;
315
(* LE RESTE MARCHE PAS DOMMAGE ..... *)
340
Ltac Ring_simplify_in hyp:= Ring_simplify_gen ltac:(fun H => rewrite H in hyp).
343
Tactic Notation (at level 0)
344
"ring_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
345
match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl G end.
347
Tactic Notation (at level 0)
348
"ring_simplify" constr_list(rl) :=
349
match goal with [|- ?G] => ring_lookup Ring_simplify [] rl G end.
351
Tactic Notation (at level 0)
352
"ring_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h):=
353
let t := type of h in
355
(fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
357
Ring_norm_gen ltac:(fun EQ => rewrite EQ in h) cst_tac pow_tac lemma2 req ring_subst_niter lH rl;
360
(* ring_lookup ltac:(Ring_simplify_in h) [lH] rl [t]. NE MARCHE PAS ??? *)
362
Ltac Ring_simpl_in hyp := Ring_norm_gen ltac:(fun H => rewrite H in hyp).
364
Tactic Notation (at level 0)
365
"ring_simplify" constr_list(rl) "in" constr(h):=
366
let t := type of h in
368
(fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
370
Ring_simpl_in h cst_tac pow_tac lemma2 req ring_subst_niter lH rl;
374
Ltac rw_in H Heq := rewrite Heq in H.
377
let t := type of H in
379
(fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
381
Ring_norm_gen ltac:(fun Heq => rewrite Heq in H) cst_tac pow_tac lemma2 req ring_subst_niter lH rl;
added
removed
contrib/setoid_ring/Ring_tac.v
