summaryrefslogtreecommitdiff
path: root/plugins/setoid_ring/Ring_tac.v
blob: d33e9a82a1937cdbac9c926b63c897707ecf7bc7 (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
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
Set Implicit Arguments.
Require Import Setoid.
Require Import BinPos.
Require Import Ring_polynom.
Require Import BinList.
Require Import InitialRing.
Require Import Quote.
Declare ML Module "newring_plugin".


(* adds a definition t' on the normal form of t and an hypothesis id
   stating that t = t' (tries to produces a proof as small as possible) *)
Ltac compute_assertion eqn t' t :=
  let nft := eval vm_compute in t in
  pose (t' := nft);
  assert (eqn : t = t');
  [vm_cast_no_check (refl_equal t')|idtac].

Ltac relation_carrier req :=
  let ty := type of req in
  match eval hnf in ty with
   ?R -> _ => R
  | _ => fail 1000 "Equality has no relation type"
  end.

Ltac Get_goal := match goal with [|- ?G] => G end.

(********************************************************************)
(* Tacticals to build reflexive tactics *)

Ltac OnEquation req :=
  match goal with
  | |- req ?lhs ?rhs => (fun f => f lhs rhs)
  | _ => (fun _ => fail "Goal is not an equation (of expected equality)")
  end.

Ltac OnEquationHyp req h :=
  match type of h with
  | req ?lhs ?rhs => fun f => f lhs rhs
  | _ => (fun _ => fail "Hypothesis is not an equation (of expected equality)")
  end.

(* Note: auxiliary subgoals in reverse order *)
Ltac OnMainSubgoal H ty :=
  match ty with
  | _ -> ?ty' =>
     let subtac := OnMainSubgoal H ty' in
     fun kont => lapply H; [clear H; intro H; subtac kont | idtac]
  | _ => (fun kont => kont())
  end.

(* A generic pattern to have reflexive tactics do some computation:
   lemmas of the form [forall x', x=x' -> P(x')] are understood as:
   compute the normal form of x, instantiate x' with it, prove
   hypothesis x=x' with vm_compute and reflexivity, and pass the
   instantiated lemma to the continuation.
 *)
Ltac ProveLemmaHyp lemma :=
  match type of lemma with
    forall x', ?x = x' -> _ =>
      (fun kont =>
        let x' := fresh "res" in
        let H := fresh "res_eq" in
        compute_assertion H x' x;
        let lemma' := constr:(lemma x' H) in
        kont lemma';
        (clear H||idtac"ProveLemmaHyp: cleanup failed");
        subst x')
  | _ => (fun _ => fail "ProveLemmaHyp: lemma not of the expected form")
  end.

Ltac ProveLemmaHyps lemma :=
  match type of lemma with
    forall x', ?x = x' -> _ =>
      (fun kont =>
        let x' := fresh "res" in
        let H := fresh "res_eq" in
        compute_assertion H x' x;
        let lemma' := constr:(lemma x' H) in
        ProveLemmaHyps lemma' kont;
        (clear H||idtac"ProveLemmaHyps: cleanup failed");
        subst x')
  | _ => (fun kont => kont lemma)
  end.

(*
Ltac ProveLemmaHyps lemma := (* expects a continuation *)
  let try_step := ProveLemmaHyp lemma in
  (fun kont =>
    try_step ltac:(fun lemma' => ProveLemmaHyps lemma' kont) ||
    kont lemma).
*)
Ltac ApplyLemmaThen lemma expr kont :=
  let lem := constr:(lemma expr) in
  ProveLemmaHyp lem ltac:(fun lem' =>
    let Heq := fresh "thm" in
    assert (Heq:=lem');
    OnMainSubgoal Heq ltac:(type of Heq) ltac:(fun _ => kont Heq);
    (clear Heq||idtac"ApplyLemmaThen: cleanup failed")).
(*
Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg :=
  let pe :=
    match type of (lemma expr) with
      forall pe', ?pe = pe' -> _ => pe
    | _ => fail 1 "ApplyLemmaThenAndCont: cannot find norm expression"
    end in
  let pe' := fresh "expr_nf" in
  let nf_pe := fresh "pe_eq" in
  compute_assertion nf_pe pe' pe;
  let Heq := fresh "thm" in
  (assert (Heq:=lemma pe pe' H) || fail "anomaly: failed to apply lemma");
  clear nf_pe;
  OnMainSubgoal Heq ltac:(type of Heq)
    ltac:(try tac Heq; clear Heq pe';CONT_tac cont_arg)).
*)
Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac :=
  ApplyLemmaThen lemma expr
    ltac:(fun lemma' => try tac lemma'; CONT_tac()).

(* General scheme of reflexive tactics using of correctness lemma
   that involves normalisation of one expression
   - [FV_tac term fv] is a tactic that adds the atomic expressions
       of [term] into [fv]
   - [SYN_tac term fv] reifies [term] given the list of atomic expressions
   - [LEMMA_tac fv kont] computes the correctness lemma and passes it to
       continuation kont
   - [MAIN_tac H] process H which is the conclusion of the correctness lemma
       instantiated with each reified term
   - [fv] is the initial value of atomic expressions (to be completed by
       the reification of the terms
   - [terms] the list (a constr of type list) of terms to reify and process.
 *)
Ltac ReflexiveRewriteTactic
     FV_tac SYN_tac LEMMA_tac MAIN_tac fv terms :=
  (* extend the atom list *)
  let fv := list_fold_left FV_tac fv terms in
  let RW_tac lemma :=
     let fcons term CONT_tac :=
      let expr := SYN_tac term fv in
      let main H :=
        match type of H with
        | (?req _ ?rhs) => change (req term rhs) in H
        end;
        MAIN_tac H in
      (ApplyLemmaThenAndCont lemma expr main CONT_tac) in
     (* rewrite steps *)
     lazy_list_fold_right fcons ltac:(fun _=>idtac) terms in
  LEMMA_tac fv RW_tac.

(********************************************************)

Ltac FV_hypo_tac mkFV req lH :=
  let R := relation_carrier req in
  let FV_hypo_l_tac h :=
    match h with @mkhypo (req ?pe _) _ => mkFV pe end in
  let FV_hypo_r_tac h :=
    match h with @mkhypo (req _ ?pe) _ => mkFV pe end in
  let fv := list_fold_right FV_hypo_l_tac (@nil R) lH in
  list_fold_right FV_hypo_r_tac fv lH.

Ltac mkHyp_tac C req Reify lH :=
  let mkHyp h res :=
   match h with
   | @mkhypo (req ?r1 ?r2) _ =>
     let pe1 := Reify r1 in
     let pe2 := Reify r2 in
     constr:(cons (pe1,pe2) res)
   | _ => fail 1 "hypothesis is not a ring equality"
   end in
  list_fold_right mkHyp (@nil (PExpr C * PExpr C)) lH.

Ltac proofHyp_tac lH :=
  let get_proof h :=
    match h with
    | @mkhypo _ ?p => p
    end in
  let rec bh l :=
    match l with
    | nil => constr:(I)
    | cons ?h nil => get_proof h
    | cons ?h ?tl =>
      let l := get_proof h in
      let r := bh tl in
      constr:(conj l r)
    end in
  bh lH.

Ltac get_MonPol lemma :=
  match type of lemma with
  | context [(mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?cdiv ?ceqb _)] =>
      constr:(mk_monpol_list cO cI cadd cmul csub copp cdiv ceqb)
  | _ => fail 1 "ring/field anomaly: bad correctness lemma (get_MonPol)"
  end.

(********************************************************)

(* Building the atom list of a ring expression *)
Ltac FV Cst CstPow add mul sub opp pow t fv :=
 let rec TFV t fv :=
  let f :=
  match Cst t with
  | NotConstant =>
      match t with
      | (add ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
      | (mul ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
      | (sub ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
      | (opp ?t1) => fun _ => TFV t1 fv
      | (pow ?t1 ?n) =>
        match CstPow n with
        | InitialRing.NotConstant => fun _ => AddFvTail t fv
        | _ => fun _ => TFV t1 fv
        end
      | _ => fun _ => AddFvTail t fv
      end
  | _ => fun _ => fv
  end in
  f()
 in TFV t fv.

 (* syntaxification of ring expressions *)
Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv :=
 let rec mkP t :=
    let f :=
    match Cst t with
    | InitialRing.NotConstant =>
        match t with
        | (radd ?t1 ?t2) =>
          fun _ =>
          let e1 := mkP t1 in
          let e2 := mkP t2 in constr:(PEadd e1 e2)
        | (rmul ?t1 ?t2) =>
          fun _ =>
          let e1 := mkP t1 in
          let e2 := mkP t2 in constr:(PEmul e1 e2)
        | (rsub ?t1 ?t2) =>
          fun _ =>
          let e1 := mkP t1 in
          let e2 := mkP t2 in constr:(PEsub e1 e2)
        | (ropp ?t1) =>
          fun _ =>
          let e1 := mkP t1 in constr:(PEopp e1)
        | (rpow ?t1 ?n) =>
          match CstPow n with
          | InitialRing.NotConstant =>
            fun _ => let p := Find_at t fv in constr:(PEX C p)
          | ?c => fun _ => let e1 := mkP t1 in constr:(PEpow e1 c)
          end
        | _ =>
          fun _ => let p := Find_at t fv in constr:(PEX C p)
        end
    | ?c => fun _ => constr:(@PEc C c)
    end in
    f ()
 in mkP t.

(* packaging the ring structure *)

Ltac PackRing F req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post :=
  let RNG :=
    match type of lemma1 with
    | context
       [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
        (fun proj => proj
             cst_tac pow_tac pre post
             R req add mul sub opp C Cpow powphi pow lemma1 lemma2)
    | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
    end in
  F RNG.

Ltac get_Carrier RNG :=
  RNG ltac:(fun cst_tac pow_tac pre post
             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
            R).

Ltac get_Eq RNG :=
  RNG ltac:(fun cst_tac pow_tac pre post
             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
            req).

Ltac get_Pre RNG :=
  RNG ltac:(fun cst_tac pow_tac pre post
             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
            pre).

Ltac get_Post RNG :=
  RNG ltac:(fun cst_tac pow_tac pre post
             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
            post).

Ltac get_NormLemma RNG :=
  RNG ltac:(fun cst_tac pow_tac pre post
             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
            lemma1).

Ltac get_SimplifyLemma RNG :=
  RNG ltac:(fun cst_tac pow_tac pre post
             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
            lemma2).

Ltac get_RingFV RNG :=
  RNG ltac:(fun cst_tac pow_tac pre post
             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
            FV cst_tac pow_tac add mul sub opp pow).

Ltac get_RingMeta RNG :=
  RNG ltac:(fun cst_tac pow_tac pre post
             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
            mkPolexpr C cst_tac pow_tac add mul sub opp pow).

Ltac get_RingHypTac RNG :=
  RNG ltac:(fun cst_tac pow_tac pre post
             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
       let mkPol := mkPolexpr C cst_tac pow_tac add mul sub opp pow in
       fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH).

(* ring tactics *)

Definition ring_subst_niter := (10*10*10)%nat.

Ltac Ring RNG lemma lH :=
  let req := get_Eq RNG in
  OnEquation req ltac:(fun lhs rhs =>
    let mkFV := get_RingFV RNG in
    let mkPol := get_RingMeta RNG in
    let mkHyp := get_RingHypTac RNG in
    let fv := FV_hypo_tac mkFV ltac:(get_Eq RNG) lH in
    let fv := mkFV lhs fv in
    let fv := mkFV rhs fv in
    check_fv fv;
    let pe1 := mkPol lhs fv in
    let pe2 := mkPol rhs fv in
    let lpe := mkHyp fv lH in
    let vlpe := fresh "hyp_list" in
    let vfv := fresh "fv_list" in
    pose (vlpe := lpe);
    pose (vfv := fv);
    (apply (lemma vfv vlpe pe1 pe2)
      || fail "typing error while applying ring");
    [ ((let prh := proofHyp_tac lH in exact prh)
        || idtac "can not automatically proof hypothesis :";
           idtac " maybe a left member of a hypothesis is not a monomial")
    | vm_compute;
      (exact (refl_equal true) || fail "not a valid ring equation")]).

Ltac Ring_norm_gen f RNG lemma lH rl :=
  let mkFV := get_RingFV RNG in
  let mkPol := get_RingMeta RNG in
  let mkHyp := get_RingHypTac RNG in
  let mk_monpol := get_MonPol lemma in
  let fv := FV_hypo_tac mkFV ltac:(get_Eq RNG) lH in
  let lemma_tac fv kont :=
    let lpe := mkHyp fv lH in
    let vlpe := fresh "list_hyp" in
    let vlmp := fresh "list_hyp_norm" in
    let vlmp_eq := fresh "list_hyp_norm_eq" in
    let prh := proofHyp_tac lH in
    pose (vlpe := lpe);
    compute_assertion vlmp_eq vlmp (mk_monpol vlpe);
    let H := fresh "ring_lemma" in
    (assert (H := lemma vlpe fv prh vlmp vlmp_eq)
      || fail "type error when build the rewriting lemma");
    clear vlmp_eq;
    kont H;
    (clear H||idtac"Ring_norm_gen: cleanup failed");
    subst vlpe vlmp in
  let simpl_ring H := (protect_fv "ring" in H; f H) in
  ReflexiveRewriteTactic mkFV mkPol lemma_tac simpl_ring fv rl.

Ltac Ring_gen RNG lH rl :=
  let lemma := get_NormLemma RNG in
  get_Pre RNG ();
  Ring RNG (lemma ring_subst_niter) lH.

Tactic Notation (at level 0) "ring" :=
  let G := Get_goal in
  ring_lookup (PackRing Ring_gen) [] G.

Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" :=
  let G := Get_goal in
  ring_lookup (PackRing Ring_gen) [lH] G.

(* Simplification *)

Ltac Ring_simplify_gen f RNG lH rl :=
  let lemma := get_SimplifyLemma RNG in
  let l := fresh "to_rewrite" in
  pose (l:= rl);
  generalize (refl_equal l);
  unfold l at 2;
  get_Pre RNG ();
  let rl :=
    match goal with
    | [|- l = ?RL -> _ ] => RL
    | _ => fail 1 "ring_simplify anomaly: bad goal after pre"
    end in
  let Heq := fresh "Heq" in
  intros Heq;clear Heq l;
  Ring_norm_gen f RNG (lemma ring_subst_niter) lH rl;
  get_Post RNG ().

Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H).

Tactic Notation (at level 0) "ring_simplify" constr_list(rl) :=
  let G := Get_goal in
  ring_lookup (PackRing Ring_simplify) [] rl G.

Tactic Notation (at level 0)
  "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
  let G := Get_goal in
  ring_lookup (PackRing Ring_simplify) [lH] rl G.

(* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *)

Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):=
  let G := Get_goal in
  let t := type of H in
  let g := fresh "goal" in
  set (g:= G);
  generalize H;clear H;
  ring_lookup (PackRing Ring_simplify) [] rl t;
  intro H;
  unfold g;clear g.

Tactic Notation
  "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):=
  let G := Get_goal in
  let t := type of H in
  let g := fresh "goal" in
  set (g:= G);
  generalize H;clear H;
  ring_lookup (PackRing Ring_simplify) [lH] rl t;
  intro H;
  unfold g;clear g.