aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrequality.ml
blob: 6032ed2af87c22ffd71ee9b2cc879c5868aefb11 (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
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)

open Ltac_plugin
open Util
open Names
open Term
open Constr
open Vars
open Locus
open Printer
open Globnames
open Termops
open Tacinterp

open Ssrmatching_plugin
open Ssrmatching

open Ssrast
open Ssrprinters
open Ssrcommon
open Tacticals
open Tacmach

let ssroldreworder = Summary.ref ~name:"SSR:oldreworder" false
let _ =
  Goptions.declare_bool_option
    { Goptions.optname  = "ssreflect 1.3 compatibility flag";
      Goptions.optkey   = ["SsrOldRewriteGoalsOrder"];
      Goptions.optread  = (fun _ -> !ssroldreworder);
      Goptions.optdepr  = false;
      Goptions.optwrite = (fun b -> ssroldreworder := b) }

(** The "simpl" tactic *)

(* We must avoid zeta-converting any "let"s created by the "in" tactical. *)

let tacred_simpl gl =
  let simpl_expr =
    Genredexpr.(
      Simpl(Redops.make_red_flag[FBeta;FMatch;FZeta;FDeltaBut []],None)) in
  let esimpl, _ = Redexpr.reduction_of_red_expr (pf_env gl) simpl_expr in
  let esimpl e sigma c =
    let (_,t) = esimpl e sigma c in
    t in
  let simpl env sigma c = (esimpl env sigma c) in
  simpl

let safe_simpltac n gl =
  if n = ~-1 then
    let cl= red_safe (tacred_simpl gl) (pf_env gl) (project gl) (pf_concl gl) in
    Proofview.V82.of_tactic (convert_concl_no_check cl) gl
  else
    ssr_n_tac "simpl" n gl

let simpltac = function
  | Simpl n -> safe_simpltac n
  | Cut n -> tclTRY (donetac n)
  | SimplCut (n,m) -> tclTHEN (safe_simpltac m) (tclTRY (donetac n))
  | Nop -> tclIDTAC

(** The "congr" tactic *)

let interp_congrarg_at ist gl n rf ty m =
  ppdebug(lazy Pp.(str"===interp_congrarg_at==="));
  let congrn, _ = mkSsrRRef "nary_congruence" in
  let args1 = mkRnat n :: mkRHoles n @ [ty] in
  let args2 = mkRHoles (3 * n) in
  let rec loop i =
    if i + n > m then None else
    try
      let rt = mkRApp congrn (args1 @  mkRApp rf (mkRHoles i) :: args2) in
      ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) rt));
      Some (interp_refine ist gl rt)
    with _ -> loop (i + 1) in
  loop 0

let pattern_id = mk_internal_id "pattern value"

let congrtac ((n, t), ty) ist gl =
  ppdebug(lazy (Pp.str"===congr==="));
  ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl)));
  let sigma, _ as it = interp_term ist gl t in
  let gl = pf_merge_uc_of sigma gl in
  let _, f, _, _ucst = pf_abs_evars gl it in
  let ist' = {ist with lfun =
    Id.Map.add pattern_id (Tacinterp.Value.of_constr f) Id.Map.empty } in
  let rf = mkRltacVar pattern_id in
  let m = pf_nbargs gl f in
  let _, cf = if n > 0 then
    match interp_congrarg_at ist' gl n rf ty m with
    | Some cf -> cf
    | None -> errorstrm Pp.(str "No " ++ int n ++ str "-congruence with "
                         ++ pr_term t)
    else let rec loop i =
      if i > m then errorstrm Pp.(str "No congruence with " ++ pr_term t)
      else match interp_congrarg_at ist' gl i rf ty m with
      | Some cf -> cf
      | None -> loop (i + 1) in
      loop 1 in
  tclTHEN (refine_with cf) (tclTRY (Proofview.V82.of_tactic Tactics.reflexivity)) gl

let newssrcongrtac arg ist gl =
  ppdebug(lazy Pp.(str"===newcongr==="));
  ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl)));
  (* utils *)
  let fs gl t = Reductionops.nf_evar (project gl) t in
  let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl =
    match try Some (pf_unify_HO gl_c (pf_concl gl) c) with _ -> None with  
    | Some gl_c ->
        tclTHEN (Proofview.V82.of_tactic (convert_concl (fs gl_c c)))
          (t_ok (proj gl_c)) gl
    | None -> t_fail () gl in 
  let mk_evar gl ty = 
    let env, sigma, si = pf_env gl, project gl, sig_it gl in
    let sigma = Evd.create_evar_defs sigma in
    let (sigma, x) = Evarutil.new_evar env sigma ty in
    x, re_sig si sigma in
  let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in
  let ssr_congr lr = EConstr.mkApp (arr, lr) in
  (* here thw two cases: simple equality or arrow *)
  let equality, _, eq_args, gl' =
    let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in
    pf_saturate gl (EConstr.of_constr eq) 3 in
  tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args))
  (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist)
  (fun () ->
    let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in
    let arrow = EConstr.mkArrow lhs (EConstr.Vars.lift 1 rhs) in
    tclMATCH_GOAL (arrow, gl') (fun gl' -> [|fs gl' lhs;fs gl' rhs|])
    (fun lr -> tclTHEN (Proofview.V82.of_tactic (Tactics.apply (ssr_congr lr))) (congrtac (arg, mkRType) ist))
    (fun _ _ -> errorstrm Pp.(str"Conclusion is not an equality nor an arrow")))
    gl

(** 7. Rewriting tactics (rewrite, unlock) *)

(** Coq rewrite compatibility flag *)


let _ =
  let ssr_strict_match = ref false in
  Goptions.declare_bool_option
    { Goptions.optname  = "strict redex matching";
      Goptions.optkey   = ["Match"; "Strict"];
      Goptions.optread  = (fun () -> !ssr_strict_match);
      Goptions.optdepr  = true; (* noop *)
      Goptions.optwrite = (fun b -> ssr_strict_match := b) }

(** Rewrite rules *)

type ssrwkind = RWred of ssrsimpl | RWdef | RWeq
type ssrrule = ssrwkind * ssrterm

(** Rewrite arguments *)

type ssrrwarg = (ssrdir * ssrmult) * ((ssrdocc * rpattern option) * ssrrule)

let notimes = 0
let nomult = 1, Once

let mkocc occ = None, occ
let noclr = mkocc None
let mkclr clr  = Some clr, None
let nodocc = mkclr []

let is_rw_cut = function RWred (Cut _) -> true | _ -> false

let mk_rwarg (d, (n, _ as m)) ((clr, occ as docc), rx) (rt, _ as r) : ssrrwarg =   
 if rt <> RWeq then begin
   if rt = RWred Nop && not (m = nomult && occ = None && rx = None)
                     && (clr = None || clr = Some []) then
     anomaly "Improper rewrite clear switch";
   if d = R2L && rt <> RWdef then
     CErrors.user_err (Pp.str "Right-to-left switch on simplification");
   if n <> 1 && is_rw_cut rt then
     CErrors.user_err (Pp.str "Bad or useless multiplier");
   if occ <> None && rx = None && rt <> RWdef then
     CErrors.user_err (Pp.str "Missing redex for simplification occurrence")
 end; (d, m), ((docc, rx), r)

let norwmult = L2R, nomult
let norwocc = noclr, None

let simplintac occ rdx sim gl = 
  let simptac m gl =
    if m <> ~-1 then
      CErrors.user_err (Pp.str "Localized custom simpl tactic not supported");
    let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
    let simp env c _ _ = EConstr.Unsafe.to_constr (red_safe Tacred.simpl env sigma0 (EConstr.of_constr c)) in
    Proofview.V82.of_tactic
      (convert_concl_no_check (EConstr.of_constr (eval_pattern env0 sigma0 (EConstr.Unsafe.to_constr concl0) rdx occ simp)))
      gl in
  match sim with
  | Simpl m -> simptac m gl
  | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (donetac n)) gl
  | _ -> simpltac sim gl

let rec get_evalref sigma c = match EConstr.kind sigma c with
  | Var id -> EvalVarRef id
  | Const (k,_) -> EvalConstRef k
  | App (c', _) -> get_evalref sigma c'
  | Cast (c', _, _) -> get_evalref sigma c'
  | Proj(c,_) -> EvalConstRef(Projection.constant c)
  | _ -> errorstrm Pp.(str "The term " ++ pr_constr_pat (EConstr.Unsafe.to_constr c) ++ str " is not unfoldable")

(* Strip a pattern generated by a prenex implicit to its constant. *)
let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with
  | App (f, a) when kt = xNoFlag && Array.for_all (EConstr.isEvar sigma) a && EConstr.isConst sigma f -> 
    (sigma, f), true
  | Const _ | Var _ -> p, true
  | Proj _ -> p, true
  | _ -> p, false

let same_proj sigma t1 t2 =
  match EConstr.kind sigma t1, EConstr.kind sigma t2 with
  | Proj(c1,_), Proj(c2, _) -> Projection.equal c1 c2
  | _ -> false

let all_ok _ _ = true

let fake_pmatcher_end () =
  mkProp, L2R, (Evd.empty, Evd.empty_evar_universe_context, mkProp)

let unfoldintac occ rdx t (kt,_) gl = 
  let fs sigma x = Reductionops.nf_evar sigma x in
  let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
  let (sigma, t), const = strip_unfold_term env0 t kt in
  let body env t c =
    Tacred.unfoldn [AllOccurrences, get_evalref sigma t] env sigma0 c in
  let easy = occ = None && rdx = None in
  let red_flags = if easy then CClosure.betaiotazeta else CClosure.betaiota in
  let beta env = Reductionops.clos_norm_flags red_flags env sigma0 in
  let unfold, conclude = match rdx with
  | Some (_, (In_T _ | In_X_In_T _)) | None ->
    let ise = Evd.create_evar_defs sigma in
    let ise, u = mk_tpattern env0 sigma0 (ise,EConstr.Unsafe.to_constr t) all_ok L2R (EConstr.Unsafe.to_constr t) in
    let find_T, end_T =
      mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in
    (fun env c _ h -> 
      try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c)))
      with NoMatch when easy -> c
      | NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of "
        ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)),
    (fun () -> try end_T () with 
      | NoMatch when easy -> fake_pmatcher_end () 
      | NoMatch -> anomaly "unfoldintac")
  | _ -> 
    (fun env (c as orig_c) _ h ->
      if const then
        let rec aux c = 
          match EConstr.kind sigma0 c with
          | Const _ when EConstr.eq_constr sigma0 c t -> body env t t
          | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a)
          | Proj _ when same_proj sigma0 c t -> body env t c
          | _ ->
            let c = Reductionops.whd_betaiotazeta sigma0 c in
            match EConstr.kind sigma0 c with
            | Const _ when EConstr.eq_constr sigma0 c t -> body env t t
            | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a)
            | Proj _ when same_proj sigma0 c t -> body env t c
            | Const f -> aux (body env c c)
            | App (f, a) -> aux (EConstr.mkApp (body env f f, a))
            | _ -> errorstrm Pp.(str "The term "++ pr_constr_env env sigma orig_c++
                str" contains no " ++ pr_econstr_env env sigma t ++ str" even after unfolding")
          in EConstr.Unsafe.to_constr @@ aux (EConstr.of_constr c)
      else
        try EConstr.Unsafe.to_constr @@ body env t (fs (unify_HO env sigma (EConstr.of_constr c) t) t)
        with _ -> errorstrm Pp.(str "The term " ++
          pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))),
    fake_pmatcher_end in
  let concl = 
    let concl0 = EConstr.Unsafe.to_constr concl0 in
    try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold)) 
    with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_constr_pat (EConstr.Unsafe.to_constr t)) in
  let _ = conclude () in
  Proofview.V82.of_tactic (convert_concl concl) gl
;;

let foldtac occ rdx ft gl = 
  let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
  let sigma, t = ft in
  let t = EConstr.to_constr sigma t in
  let fold, conclude = match rdx with
  | Some (_, (In_T _ | In_X_In_T _)) | None ->
    let ise = Evd.create_evar_defs sigma in
    let ut = EConstr.Unsafe.to_constr (red_product_skip_id env0 sigma (EConstr.of_constr t)) in
    let ise, ut = mk_tpattern env0 sigma0 (ise,t) all_ok L2R ut in
    let find_T, end_T =
      mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[ut]) in
    (fun env c _ h -> try find_T env c h ~k:(fun env t _ _ -> t) with NoMatch ->c),
    (fun () -> try end_T () with NoMatch -> fake_pmatcher_end ())
  | _ -> 
    (fun env c _ h -> try let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in EConstr.to_constr sigma (EConstr.of_constr t)
    with _ -> errorstrm Pp.(str "fold pattern " ++ pr_constr_pat t ++ spc ()
      ++ str "does not match redex " ++ pr_constr_pat c)), 
    fake_pmatcher_end in
  let concl0 = EConstr.Unsafe.to_constr concl0 in
  let concl = eval_pattern env0 sigma0 concl0 rdx occ fold in
  let _ = conclude () in
  Proofview.V82.of_tactic (convert_concl (EConstr.of_constr concl)) gl
;;

let converse_dir = function L2R -> R2L | R2L -> L2R

let rw_progress rhs lhs ise = not (EConstr.eq_constr ise lhs (Evarutil.nf_evar ise rhs))

(* Coq has a more general form of "equation" (any type with a single *)
(* constructor with no arguments with_rect_r elimination lemmas).    *)
(* However there is no clear way of determining the LHS and RHS of   *)
(* such a generic Leibnitz equation -- short of inspecting the type  *)
(* of the elimination lemmas.                                        *)

let rec strip_prod_assum c = match Constr.kind c with
  | Prod (_, _, c') -> strip_prod_assum c'
  | LetIn (_, v, _, c') -> strip_prod_assum (subst1 v c)
  | Cast (c', _, _) -> strip_prod_assum c'
  | _ -> c

let rule_id = mk_internal_id "rewrite rule"

exception PRtype_error

let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
(*   ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *)
  let env = pf_env gl in
  let beta = Reductionops.clos_norm_flags CClosure.beta env sigma in
  let sigma, p = 
    let sigma = Evd.create_evar_defs sigma in
    let (sigma, ev) = Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in
    (sigma, ev)
  in
  let pred = EConstr.mkNamedLambda pattern_id rdx_ty pred in
  let elim, gl = 
    let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
    let sort = elimination_sort_of_goal gl in
    let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in
    if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
    let elim, _ = destConst elim in
    let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical elim)) in
    let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r")  in 
    let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make3 mp dp l')) in
    mkConst c1', gl in
  let elim = EConstr.of_constr elim in
  let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in
  (* We check the proof is well typed *)
  let sigma, proof_ty =
    try Typing.type_of env sigma proof with _ -> raise PRtype_error in
  ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty));
  try refine_with 
    ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl
  with _ -> 
    (* we generate a msg like: "Unable to find an instance for the variable" *)
    let hd_ty, miss = match EConstr.kind sigma c with
    | App (hd, args) -> 
        let hd_ty = Retyping.get_type_of env sigma hd in
        let names = let rec aux t = function 0 -> [] | n ->
          let t = Reductionops.whd_all env sigma t in
          match EConstr.kind_of_type sigma t with
          | ProdType (name, _, t) -> name :: aux t (n-1)
          | _ -> assert false in aux hd_ty (Array.length args) in
        hd_ty, Util.List.map_filter (fun (t, name) ->
          let evs = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma t) in
          let open_evs = List.filter (fun k ->
            Sorts.InProp <> Retyping.get_sort_family_of
              env sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k))))
            evs in
          if open_evs <> [] then Some name else None)
          (List.combine (Array.to_list args) names)
    | _ -> anomaly "rewrite rule not an application" in
    errorstrm Pp.(Himsg.explain_refiner_error env sigma (Logic.UnresolvedBindings miss)++
      (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty))
;;

let is_construct_ref sigma c r =
  EConstr.isConstruct sigma c && eq_gr (ConstructRef (fst(EConstr.destConstruct sigma c))) r
let is_ind_ref sigma c r = EConstr.isInd sigma c && eq_gr (IndRef (fst(EConstr.destInd sigma c))) r

let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type x xs)

let rwcltac cl rdx dir sr gl =
  let n, r_n,_, ucst = pf_abs_evars gl sr in
  let r_n' = pf_abs_cterm gl n r_n in
  let r' = EConstr.Vars.subst_var pattern_id r_n' in
  let gl = pf_unsafe_merge_uc ucst gl in
  let rdxt = Retyping.get_type_of (pf_env gl) (fst sr) rdx in
(*         ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *)
        ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr)));
  let cvtac, rwtac, gl =
    if EConstr.Vars.closed0 (project gl) r' then 
      let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.build_coq_eq () in
      let sigma, c_ty = Typing.type_of env sigma c in
        ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
      match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
      | AtomicType(e, a) when is_ind_ref sigma e c_eq ->
          let new_rdx = if dir = L2R then a.(2) else a.(1) in
          pirrel_rewrite cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
      | _ -> 
          let cl' = EConstr.mkApp (EConstr.mkNamedLambda pattern_id rdxt cl, [|rdx|]) in
          let sigma, _ = Typing.type_of env sigma cl' in
          let gl = pf_merge_uc_of sigma gl in
          Proofview.V82.of_tactic (convert_concl cl'), rewritetac dir r', gl
    else
      let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in
      let r3, _, r3t  = 
        try EConstr.destCast (project gl) r2 with _ ->
        errorstrm Pp.(str "no cast from " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd sr))
                    ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in
      let cl' = EConstr.mkNamedProd rule_id (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in
      let cl'' = EConstr.mkNamedProd pattern_id rdxt cl' in
      let itacs = [introid pattern_id; introid rule_id] in
      let cltac = Proofview.V82.of_tactic (Tactics.clear [pattern_id; rule_id]) in
      let rwtacs = [rewritetac dir (EConstr.mkVar rule_id); cltac] in
      apply_type cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], tclTHENLIST (itacs @ rwtacs), gl
  in
  let cvtac' _ =
    try cvtac gl with
    | PRtype_error ->
      if occur_existential (project gl) (Tacmach.pf_concl gl)
      then errorstrm Pp.(str "Rewriting impacts evars")
      else errorstrm Pp.(str "Dependent type error in rewrite of "
        ++ pr_constr_env (pf_env gl) (project gl) (Term.mkNamedLambda pattern_id (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl)))
    | CErrors.UserError _ as e -> raise e
    | e -> anomaly ("cvtac's exception: " ^ Printexc.to_string e);
  in
  tclTHEN cvtac' rwtac gl

let prof_rwcltac = mk_profiler "rwrxtac.rwcltac";;
let rwcltac cl rdx dir sr gl =
  prof_rwcltac.profile (rwcltac cl rdx dir sr) gl
;;


let lz_coq_prod =
  let prod = lazy (Coqlib.build_prod ()) in fun () -> Lazy.force prod

let lz_setoid_relation =
  let sdir = ["Classes"; "RelationClasses"] in
  let last_srel = ref (Environ.empty_env, None) in
  fun env -> match !last_srel with
  | env', srel when env' == env -> srel
  | _ ->
    let srel =
       try Some (Universes.constr_of_global @@
                   Coqlib.coq_reference "Class_setoid" sdir "RewriteRelation")
       with _ -> None in
    last_srel := (env, srel); srel

let ssr_is_setoid env =
  match lz_setoid_relation env with
  | None -> fun _ _ _ -> false
  | Some srel ->
  fun sigma r args ->
    Rewrite.is_applied_rewrite_relation env 
      sigma [] (EConstr.mkApp (r, args)) <> None

let prof_rwxrtac_find_rule = mk_profiler "rwrxtac.find_rule";;

let closed0_check cl p gl =
  if closed0 cl then
    errorstrm Pp.(str"No occurrence of redex "++ pr_constr_env (pf_env gl) (project gl) p)

let dir_org = function L2R -> 1 | R2L -> 2

let rwprocess_rule dir rule gl =
  let env = pf_env gl in
  let coq_prod = lz_coq_prod () in
  let is_setoid = ssr_is_setoid env in
  let r_sigma, rules =
    let rec loop d sigma r t0 rs red =
      let t =
        if red = 1 then Tacred.hnf_constr env sigma t0
        else Reductionops.whd_betaiotazeta sigma t0 in
      ppdebug(lazy Pp.(str"rewrule="++pr_constr_pat (EConstr.Unsafe.to_constr t)));
      match EConstr.kind sigma t with
      | Prod (_, xt, at) ->
        let sigma = Evd.create_evar_defs sigma in
        let (sigma, x) = Evarutil.new_evar env sigma xt in
        loop d sigma EConstr.(mkApp (r, [|x|])) (EConstr.Vars.subst1 x at) rs 0
      | App (pr, a) when is_ind_ref sigma pr coq_prod.Coqlib.typ ->
        let sr sigma = match EConstr.kind sigma (Tacred.hnf_constr env sigma r) with
        | App (c, ra) when is_construct_ref sigma c coq_prod.Coqlib.intro ->
          fun i -> ra.(i + 1), sigma
        | _ -> let ra = Array.append a [|r|] in
          function 1 ->
            let sigma, pi1 = Evd.fresh_global env sigma coq_prod.Coqlib.proj1 in
            EConstr.mkApp (EConstr.of_constr pi1, ra), sigma
          | _ ->
            let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in
            EConstr.mkApp (EConstr.of_constr pi2, ra), sigma in
        if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ())) then
         let s, sigma = sr sigma 2 in
         loop (converse_dir d) sigma s a.(1) rs 0
        else
         let s, sigma = sr sigma 2 in
         let sigma, rs2 = loop d sigma s a.(1) rs 0 in
         let s, sigma = sr sigma 1 in
         loop d sigma s a.(0) rs2 0
      | App (r_eq, a) when Hipattern.match_with_equality_type sigma t != None ->
        let (ind, u) = EConstr.destInd sigma r_eq and rhs = Array.last a in
        let np = Inductiveops.inductive_nparamdecls ind in
        let indu = (ind, EConstr.EInstance.kind sigma u) in
        let ind_ct = Inductiveops.type_of_constructors env indu in
        let lhs0 = last_arg sigma (EConstr.of_constr (strip_prod_assum ind_ct.(0))) in
        let rdesc = match EConstr.kind sigma lhs0 with
        | Rel i ->
          let lhs = a.(np - i) in
          let lhs, rhs = if d = L2R then lhs, rhs else rhs, lhs in
(* msgnl (str "RW: " ++ pr_rwdir d ++ str " " ++ pr_constr_pat r ++ str " : "
            ++ pr_constr_pat lhs ++ str " ~> " ++ pr_constr_pat rhs); *)
          d, r, lhs, rhs
(*
          let l_i, r_i = if d = L2R then i, 1 - ndep else 1 - ndep, i in
          let lhs = a.(np - l_i) and rhs = a.(np - r_i) in
          let a' = Array.copy a in let _ = a'.(np - l_i) <- mkVar pattern_id in
          let r' = mkCast (r, DEFAULTcast, mkApp (r_eq, a')) in
          (d, r', lhs, rhs)
*)
        | _ ->
          let lhs = EConstr.Vars.substl (array_list_of_tl (Array.sub a 0 np)) lhs0 in
          let lhs, rhs = if d = R2L then lhs, rhs else rhs, lhs in
          let d' = if Array.length a = 1 then d else converse_dir d in
          d', r, lhs, rhs in
        sigma, rdesc :: rs
      | App (s_eq, a) when is_setoid sigma s_eq a ->
        let np = Array.length a and i = 3 - dir_org d in
        let lhs = a.(np - i) and rhs = a.(np + i - 3) in
        let a' = Array.copy a in let _ = a'.(np - i) <- EConstr.mkVar pattern_id in
        let r' = EConstr.mkCast (r, DEFAULTcast, EConstr.mkApp (s_eq, a')) in
        sigma, (d, r', lhs, rhs) :: rs
      | _ ->
        if red = 0 then loop d sigma r t rs 1
        else errorstrm Pp.(str "not a rewritable relation: " ++ pr_constr_pat (EConstr.Unsafe.to_constr t)
                        ++ spc() ++ str "in rule " ++ pr_constr_pat  (EConstr.Unsafe.to_constr (snd rule)))
        in
    let sigma, r = rule in
    let t = Retyping.get_type_of env sigma r in
    loop dir sigma r t [] 0
  in
    r_sigma, rules

let rwrxtac occ rdx_pat dir rule gl =
  let env = pf_env gl in
  let r_sigma, rules = rwprocess_rule dir rule gl in
  let find_rule rdx =
    let rec rwtac = function
      | [] ->
        errorstrm Pp.(str "pattern " ++ pr_constr_pat (EConstr.Unsafe.to_constr rdx) ++
                   str " does not match " ++ pr_dir_side dir ++
                   str " of " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd rule)))
      | (d, r, lhs, rhs) :: rs ->
        try
          let ise = unify_HO env (Evd.create_evar_defs r_sigma) lhs rdx in
          if not (rw_progress rhs rdx ise) then raise NoMatch else
          d, (ise, Evd.evar_universe_context ise, Reductionops.nf_evar ise r)
        with _ -> rwtac rs in
     rwtac rules in
  let find_rule rdx = prof_rwxrtac_find_rule.profile find_rule rdx in
  let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
  let find_R, conclude = match rdx_pat with
  | Some (_, (In_T _ | In_X_In_T _)) | None ->
      let upats_origin = dir, EConstr.Unsafe.to_constr (snd rule) in
      let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) =
        let sigma, pat =
          let rw_progress rhs t evd = rw_progress rhs (EConstr.of_constr t) evd in
          mk_tpattern env sigma0 (sigma,EConstr.to_constr sigma r) (rw_progress rhs) d (EConstr.to_constr sigma lhs) in
        sigma, pats @ [pat] in
      let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
      let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats in
      (fun e c _ i -> find_R ~k:(fun _ _ _ h -> mkRel h) e c i), 
      fun cl -> let rdx,d,r = end_R () in closed0_check cl rdx gl; (d,r),rdx
  | Some(_, (T e | X_In_T (_,e) | E_As_X_In_T (e,_,_) | E_In_X_In_T (e,_,_))) ->
      let r = ref None in
      (fun env c _ h -> do_once r (fun () -> find_rule (EConstr.of_constr c), c); mkRel h),
      (fun concl -> closed0_check concl e gl;
        let (d,(ev,ctx,c)) , x = assert_done r in (d,(ev,ctx, EConstr.to_constr ev c)) , x) in
  let concl0 = EConstr.Unsafe.to_constr concl0 in
  let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in
  let (d, r), rdx = conclude concl in
  let r = Evd.merge_universe_context (pi1 r) (pi2 r), EConstr.of_constr (pi3 r) in
  rwcltac (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl
;;

let prof_rwxrtac = mk_profiler "rwrxtac";;
let rwrxtac occ rdx_pat dir rule gl =
  prof_rwxrtac.profile (rwrxtac occ rdx_pat dir rule) gl
;;

let ssrinstancesofrule ist dir arg gl =
  let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
  let rule = interp_term ist gl arg in
  let r_sigma, rules = rwprocess_rule dir rule gl in
  let find, conclude =
    let upats_origin = dir, EConstr.Unsafe.to_constr (snd rule) in
    let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) =
      let sigma, pat =
        let rw_progress rhs t evd = rw_progress rhs (EConstr.of_constr t) evd in
        mk_tpattern env sigma0 (sigma,EConstr.to_constr sigma r) (rw_progress rhs) d (EConstr.to_constr sigma lhs) in
      sigma, pats @ [pat] in
    let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
    mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in
  let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr_env env r_sigma p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr_env env r_sigma c)); c in
  Feedback.msg_info Pp.(str"BEGIN INSTANCES");
  try
    while true do
      ignore(find env0 (EConstr.Unsafe.to_constr concl0) 1 ~k:print)
    done; raise NoMatch
  with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); tclIDTAC gl

let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl

let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
  let fail = ref false in
  let interp_rpattern ist gl gc =
    try interp_rpattern ist gl gc
    with _ when snd mult = May -> fail := true; project gl, T mkProp in
  let interp gc gl =
    try interp_term ist gl gc
    with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in
  let rwtac gl = 
    let rx = Option.map (interp_rpattern ist gl) grx in
    let t = interp gt gl in
    (match kind with
    | RWred sim -> simplintac occ rx sim
    | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt
    | RWeq -> rwrxtac occ rx dir t) gl in
  let ctac = cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in
  if !fail then ctac gl else tclTHEN (tclMULT mult rwtac) ctac gl

(** Rewrite argument sequence *)

(* type ssrrwargs = ssrrwarg list *)

(** The "rewrite" tactic *)

let ssrrewritetac ist rwargs =
  tclTHENLIST (List.map (rwargtac ist) rwargs)

(** The "unlock" tactic *)

let unfoldtac occ ko t kt gl =
  let env = pf_env gl in
  let cl, c = pf_fill_occ_term gl occ (fst (strip_unfold_term env t kt)) in
  let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref (project gl) c] gl c) cl in
  let f = if ko = None then CClosure.betaiotazeta else CClosure.betaiota in
  Proofview.V82.of_tactic
    (convert_concl (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl

let unlocktac ist args gl =
  let utac (occ, gt) gl =
    unfoldtac occ occ (interp_term ist gl gt) (fst gt) gl in
  let locked, gl = pf_mkSsrConst "locked" gl in
  let key, gl = pf_mkSsrConst "master_key" gl in
  let ktacs = [
    (fun gl -> unfoldtac None None (project gl,locked) xInParens gl); 
    Ssrelim.casetac key ] in
  tclTHENLIST (List.map utac args @ ktacs) gl