Source file ssrelim.ml
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
open Util
open Names
open Printer
open Constr
open Context
open Termops
open Tactypes
open Ssrmatching_plugin
open Ssrmatching
open Ssrast
open Ssrprinters
open Ssrcommon
open Proofview.Notations
module RelDecl = Context.Rel.Declaration
(** The "case" and "elim" tactic *)
let analyze_eliminator elimty env sigma =
let open EConstr in
let rec loop ctx t = match kind_of_type sigma t with
| AtomicType (hd, args) when isRel sigma hd ->
ctx, destRel sigma hd, not (Vars.noccurn sigma 1 t), Array.length args, t
| CastType (t, _) -> loop ctx t
| ProdType (x, ty, t) -> loop (RelDecl.LocalAssum (x, ty) :: ctx) t
| LetInType (x,b,ty,t) -> loop (RelDecl.LocalDef (x, b, ty) :: ctx) (Vars.subst1 b t)
| _ ->
let env' = push_rel_context ctx env in
let t' = Reductionops.whd_all env' sigma t in
if not (eq_constr sigma t t') then loop ctx t' else
errorstrm Pp.(str"The eliminator has the wrong shape."++spc()++
str"A (applied) bound variable was expected as the conclusion of "++
str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in
let ctx, pred_id, elim_is_dep, n_pred_args,concl = loop [] elimty in
let n_elim_args = Context.Rel.nhyps ctx in
let is_rec_elim =
let count_occurn n term =
let count = ref 0 in
let rec occur_rec n c = match EConstr.kind sigma c with
| Rel m -> if m = n then incr count
| Evar (_, args) -> SList.Skip.iter (fun c -> occur_rec n c) args
| _ -> EConstr.iter_with_binders sigma succ occur_rec n c
in
occur_rec n term; !count in
let occurr2 n t = count_occurn n t > 1 in
not (List.for_all_i
(fun i (_,rd) -> pred_id <= i || not (occurr2 (pred_id - i) rd))
1 (assums_of_rel_context ctx))
in
n_elim_args - pred_id, n_elim_args, is_rec_elim, elim_is_dep, n_pred_args,
(ctx,concl)
let subgoals_tys sigma (relctx, concl) =
let rec aux cur_depth acc = function
| hd :: rest ->
let ty = Context.Rel.Declaration.get_type hd in
if EConstr.Vars.noccurn sigma cur_depth concl &&
List.for_all_i (fun i -> function
| Context.Rel.Declaration.LocalAssum(_, t) ->
EConstr.Vars.noccurn sigma i t
| Context.Rel.Declaration.LocalDef (_, b, t) ->
EConstr.Vars.noccurn sigma i t && EConstr.Vars.noccurn sigma i b) 1 rest
then aux (cur_depth - 1) (ty :: acc) rest
else aux (cur_depth - 1) acc rest
| [] -> Array.of_list (List.rev acc)
in
aux (List.length relctx) [] (List.rev relctx)
let get_eq_type env sigma =
Evd.fresh_global env sigma Coqlib.(lib_ref "core.eq.type")
type elim_what =
| EConstr of
Ssrast.ssrhyp list * Ssrmatching.occ *
EConstr.constr
| EGen of
((Ssrast.ssrhyp list option *
Ssrmatching.occ) *
Ssrmatching.cpattern)
let check_elim sigma has_elim = function
| EConstr(_,_,t) when EConstr.isEvar sigma t ->
anomaly "elim called on a constr evar"
| EGen (_, g) when not has_elim && is_wildcard g ->
errorstrm Pp.(str"Indeterminate pattern and no eliminator")
| EGen ((Some clr,occ), g) when is_wildcard g ->
Proofview.tclUNIT (None, clr, occ, None)
| EGen ((None, occ), g) when is_wildcard g ->
Proofview.tclUNIT (None,[],occ,None)
| EGen ((_, occ), p as gen) ->
Proofview.Goal.enter_one begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let concl = Proofview.Goal.concl gl in
let sigma, (_, c, clr) = interp_gen env sigma ~concl true gen in
Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT (Some c, clr, occ, Some p)
end
| EConstr (clr, occ, c) ->
Proofview.tclUNIT (Some c, clr, occ, None)
let match_pat env sigma0 p occ h cl =
debug_ssr (fun () -> Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p));
let (c,ucst), cl =
fill_occ_pattern ~raise_NoMatch:true env sigma0 cl p occ h in
debug_ssr (fun () -> Pp.(str" got: " ++ pr_econstr_env env sigma0 c));
c, cl, ucst
let fire_subst sigma t = Reductionops.nf_evar sigma t
let mkTpat env sigma0 (sigma, t) =
let t, evs, ucst = abs_evars env sigma0 (sigma, fire_subst sigma t) in
let t, _, _, sigma = saturate ~beta:true env sigma t (List.length evs) in
{ pat_sigma = Evd.merge_universe_context sigma ucst; pat_pat = T t }
let redex_of_pattern env p = match redex_of_pattern p with
| None -> CErrors.anomaly (Pp.str "pattern without redex.")
| Some (sigma, e) -> Evarutil.nf_evar sigma e, Evd.evar_universe_context sigma
let unif_redex env sigma0 nsigma p t =
let t, evs, ucst = abs_evars env sigma0 (nsigma, fire_subst nsigma t) in
let t, _, _, sigma = saturate ~beta:true env p.pat_sigma t (List.length evs) in
let sigma = Evd.merge_universe_context sigma ucst in
match p.pat_pat with
| X_In_T (e, p) -> { pat_sigma = sigma; pat_pat = E_As_X_In_T (t, e, p) }
| _ ->
try { p with pat_sigma = unify_HO env sigma t (fst (redex_of_pattern env p)) }
with e when CErrors.noncritical e -> p
let get_nth_arg n args =
List.find_map (fun (i, x, _) -> if Int.equal i n then Some x else None) args
let find_eliminator env sigma ~concl ~is_case ?elim oc c_gen =
match elim with
| Some elim ->
let sigma, elimty = Typing.type_of env sigma elim in
let elimty =
let rename_elimty r =
EConstr.of_constr
(Arguments_renaming.rename_type
(EConstr.to_constr ~abort_on_undefined_evars:false sigma
elimty) r) in
match EConstr.kind sigma elim with
| Constr.Var kn -> rename_elimty (GlobRef.VarRef kn)
| Constr.Const (kn,_) -> rename_elimty (GlobRef.ConstRef kn)
| _ -> elimty
in
let pred_id, n_elim_args, is_rec, elim_is_dep, n_pred_args,ctx_concl =
analyze_eliminator elimty env sigma in
let seed = subgoals_tys sigma ctx_concl in
let elim, elimty, elim_args, sigma =
saturate ~beta:is_case env sigma elim ~ty:elimty n_elim_args in
let pred = get_nth_arg pred_id elim_args in
let elimty = Reductionops.whd_all env sigma elimty in
let cty, sigma =
if Option.is_empty oc then None, sigma
else
let c = Option.get oc in
let sigma, c_ty = Typing.type_of env sigma c in
let pc = match c_gen with
| Some p -> interp_cpattern env sigma p None
| _ -> mkTpat env sigma (sigma, c) in
Some(c, c_ty, pc), sigma in
sigma, seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred
| None ->
let c = Option.get oc in
let sigma, c_ty = Typing.type_of env sigma c in
let ((kn, i),_ as indu), unfolded_c_ty =
Tacred.reduce_to_quantified_ind env sigma c_ty in
let sort = Retyping.get_sort_family_of env sigma concl in
let sigma, elim, elimty =
if not is_case then
let sigma, elim = Evd.fresh_global env sigma (Indrec.lookup_eliminator env (kn,i) sort) in
let elimty = Retyping.get_type_of env sigma elim in
sigma, elim, elimty
else
let indu = (fst indu, EConstr.EInstance.kind sigma (snd indu)) in
let (sigma, ind, indty) = Indrec.build_case_analysis_scheme env sigma indu true sort in
(sigma, EConstr.of_constr ind, EConstr.of_constr indty)
in
let pred_id,n_elim_args,is_rec,elim_is_dep,n_pred_args,ctx_concl =
analyze_eliminator elimty env sigma in
let seed =
if is_case then
let mind,indb = Inductive.lookup_mind_specif env (kn,i) in
let tys = indb.Declarations.mind_nf_lc in
let renamed_tys =
Array.mapi (fun j (ctx, cty) ->
let t = Term.it_mkProd_or_LetIn cty ctx in
debug_ssr (fun () -> Pp.(str "Search" ++ Printer.pr_constr_env env sigma t));
let t = Arguments_renaming.rename_type t
(GlobRef.ConstructRef((kn,i),j+1)) in
debug_ssr (fun () -> Pp.(str"Done Search " ++ Printer.pr_constr_env env sigma t));
t)
tys
in
let drop_params x =
snd @@ EConstr.decompose_prod_n_assum sigma
mind.Declarations.mind_nparams (EConstr.of_constr x) in
Array.map drop_params renamed_tys
else
subgoals_tys sigma ctx_concl
in
let rctx = fst (EConstr.decompose_prod_assum sigma unfolded_c_ty) in
let n_c_args = Context.Rel.length rctx in
let c, c_ty, t_args, sigma = saturate env sigma c ~ty:c_ty n_c_args in
let elim, elimty, elim_args, sigma =
saturate ~beta:is_case env sigma elim ~ty:elimty n_elim_args in
let pred = get_nth_arg pred_id elim_args in
let pc = match n_c_args, c_gen with
| 0, Some p -> interp_cpattern env sigma p None
| _ -> mkTpat env sigma (sigma, c) in
let cty = Some (c, c_ty, pc) in
let elimty = Reductionops.whd_all env sigma elimty in
sigma, seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred
let saturate_until env sigma c c_ty f =
let rec loop n = try
let c, c_ty, _, sigma = saturate env sigma c ~ty:c_ty n in
let sigma' = f sigma c c_ty in
Some (c, c_ty, sigma, sigma')
with
| NotEnoughProducts -> None
| e when CErrors.noncritical e -> loop (n+1) in loop 0
let get_head_pattern env sigma elim_is_dep elim_args n_elim_args inf_deps_r cty = match cty with
| None -> sigma, true
| Some (c, c_ty, _) ->
let rec first = function
| [] ->
errorstrm Pp.(str"Unable to apply the eliminator to the term"++
spc()++pr_econstr_env env sigma c++spc())
| x :: rest ->
match x () with
| None -> first rest
| Some (sigma, b) -> sigma, b
in
let unify_HO_rigid env sigma a b =
let is_applied_evar x = match EConstr.kind sigma x with
| App(x,_) -> EConstr.isEvar sigma x
| _ -> false in
if is_applied_evar a || is_applied_evar b then
raise Evarconv.(UnableToUnify(sigma,
Pretype_errors.ProblemBeyondCapabilities))
else unify_HO env sigma a b in
let try_c_last_arg () =
if elim_is_dep then None else
let arg = get_nth_arg (n_elim_args - 1) elim_args in
let sigma, arg_ty = Typing.type_of env sigma arg in
match saturate_until env sigma c c_ty (fun sigma c c_ty ->
unify_HO env (unify_HO_rigid env sigma c_ty arg_ty) arg c) with
| Some (c, _, _, sigma) -> Some (sigma, false)
| None -> None in
let try_c_last_pattern () =
if inf_deps_r = [] then None else
let inf_arg = List.hd inf_deps_r in
let sigma, inf_arg_ty = Typing.type_of env sigma inf_arg in
match saturate_until env sigma c c_ty (fun sigma _ c_ty ->
unify_HO_rigid env sigma c_ty inf_arg_ty) with
| Some (c, _, _, sigma) -> Some(sigma, true)
| None -> None in
first [try_c_last_arg;try_c_last_pattern]
let check_pattern_instantiated env sigma patterns =
let evars_of_term = Evarutil.undefined_evars_of_term sigma in
let patterns = List.map (fun (_,_,t,_) -> Reductionops.nf_evar sigma t) patterns in
let patterns_ev = List.map evars_of_term patterns in
let ev = List.fold_left Evar.Set.union Evar.Set.empty patterns_ev in
let ty_ev = Evar.Set.fold (fun i e ->
let ex = i in
let i_ty = Evd.evar_concl (Evd.find sigma ex) in
Evar.Set.union e (evars_of_term i_ty))
ev Evar.Set.empty in
let inter = Evar.Set.inter ev ty_ev in
if not (Evar.Set.is_empty inter) then begin
let i = Evar.Set.choose inter in
let pat = List.find (fun t -> Evar.Set.mem i (evars_of_term t)) patterns in
errorstrm Pp.(str"Pattern"++spc()++pr_econstr_pat env sigma pat++spc()++
str"was not completely instantiated and one of its variables"++spc()++
str"occurs in the type of another non-instantiated pattern variable");
end
let is_undef_pat { pat_sigma = sigma; pat_pat = pat } = match pat with
| T t -> EConstr.isEvar sigma t
| _ -> false
let generate_pred env sigma0 ~concl patterns predty eqid is_rec deps elim_args n_elim_args c_is_head_p clr sigma =
let concl0 = concl in
let error sigma t inf_t = errorstrm Pp.(str"The given pattern matches the term"++
spc()++pr_econstr_env env sigma t++spc()++str"while the inferred pattern"++
spc()++pr_econstr_pat env sigma (fire_subst sigma inf_t)++spc()++ str"doesn't") in
let match_or_postpone (cl, sigma, post) (h, p, inf_t, occ) =
let p = unif_redex env sigma0 sigma p inf_t in
if is_undef_pat p then
let () = debug_ssr (fun () -> Pp.(str"postponing " ++ pp_pattern env p)) in
cl, sigma, post @ [h, p, inf_t, occ]
else try
let c, cl, ucst = match_pat env sigma0 p occ h cl in
let sigma = Evd.merge_universe_context sigma ucst in
let sigma = try unify_HO env sigma inf_t c
with exn when CErrors.noncritical exn -> error sigma c inf_t in
cl, sigma, post
with
| NoMatch | NoProgress ->
let e, ucst = redex_of_pattern env p in
let sigma = Evd.merge_universe_context sigma ucst in
let e, evs, _ucst = abs_evars env sigma (p.pat_sigma, e) in
let e, _, _, sigma = saturate ~beta:true env sigma e (List.length evs) in
let sigma = try unify_HO env sigma inf_t e
with exn when CErrors.noncritical exn -> error sigma e inf_t in
cl, sigma, post
in
let rec match_all concl sigma patterns =
let concl, sigma, postponed =
List.fold_left match_or_postpone (concl, sigma, []) patterns in
if postponed = [] then concl, sigma
else if List.length postponed = List.length patterns then
errorstrm Pp.(str "Some patterns are undefined even after all"++spc()++
str"the defined ones matched")
else match_all concl sigma postponed in
let concl, sigma = match_all concl sigma patterns in
let pred_rctx, _ = EConstr.decompose_prod_assum sigma (fire_subst sigma predty) in
let sigma, concl, gen_eq_tac, clr = match eqid with
| Some (IPatId _) when not is_rec ->
let k = List.length deps in
let c = fire_subst sigma (get_nth_arg (n_elim_args - k - 1) elim_args) in
let sigma, t = Typing.type_of env sigma c in
let sigma, eq = get_eq_type env sigma in
let sigma, gen_eq_tac, eq_ty =
let refl = EConstr.mkApp (eq, [|t; c; c|]) in
let new_concl = EConstr.mkArrow refl Sorts.Relevant (EConstr.Vars.lift 1 concl0) in
let new_concl = fire_subst sigma new_concl in
let sigma, erefl = mkRefl env sigma t c in
let erefl = fire_subst sigma erefl in
let erefl_ty = Retyping.get_type_of env sigma erefl in
let eq_ty = Retyping.get_type_of env sigma erefl_ty in
let ucst = Evd.evar_universe_context sigma in
let evds = Evar.Map.bind (Evd.find sigma) @@
Evd.evars_of_term sigma new_concl in
let gen_eq_tac =
let open Proofview.Notations in
Proofview.Goal.enter begin fun s ->
let sigma = Proofview.Goal.sigma s in
let sigma = Evd.merge_universe_context sigma ucst in
let sigma, shelve = Evar.Map.fold (fun e info (sigma, shelve) ->
if not @@ Evd.mem sigma e then
Evd.add sigma e info, e::shelve else
(sigma, shelve))
evds (sigma, []) in
Proofview.Unsafe.tclEVARS sigma <*>
Proofview.shelve_goals @@ shelve <*>
Tactics.apply_type ~typecheck:true new_concl [erefl]
end
in
sigma, gen_eq_tac, eq_ty
in
let rel = k + if c_is_head_p then 1 else 0 in
let sigma, src = mkProt env sigma eq_ty EConstr.(mkApp (eq,[|t; c; mkRel rel|])) in
let concl = EConstr.mkArrow src Sorts.Relevant (EConstr.Vars.lift 1 concl) in
let clr = if deps <> [] then clr else [] in
sigma, concl, gen_eq_tac, clr
| _ -> sigma, concl, Tacticals.tclIDTAC, clr in
let mk_lam t r = EConstr.mkLambda_or_LetIn r t in
let concl = List.fold_left mk_lam concl pred_rctx in
let sigma, concl =
if eqid <> None && is_rec then
let sigma, concls = Typing.type_of env sigma concl in
let sigma, concl = mkProt env sigma concls concl in
let sigma, _ = Typing.type_of env sigma concl in
sigma, concl
else sigma, concl in
sigma, concl, gen_eq_tac, clr
let compute_patterns env sigma0 what c_is_head_p cty deps inf_deps_r occ orig_clr eqid sigma =
let rec loop patterns clr i = function
| [],[] -> patterns, clr, sigma
| ((oclr, occ), t):: deps, inf_t :: inf_deps ->
let p = interp_cpattern env sigma0 t None in
let clr_t =
interp_clr sigma (oclr,(tag_of_cpattern t, fst (redex_of_pattern env p))) in
let clr_t = if deps = [] && eqid <> None then [] else clr_t in
let p = if is_undef_pat p then mkTpat env sigma0 (sigma, inf_t) else p in
loop (patterns @ [i, p, inf_t, occ])
(clr_t @ clr) (i+1) (deps, inf_deps)
| [], c :: inf_deps ->
debug_ssr (fun () -> Pp.(str"adding inf pattern " ++ pr_econstr_pat env sigma c));
loop (patterns @ [i, mkTpat env sigma0 (sigma, c), c, allocc])
clr (i+1) ([], inf_deps)
| _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in
let deps, head_p, inf_deps_r = match what, c_is_head_p, cty with
| EConstr _, _, None -> anomaly "Simple elim with no term"
| _, false, _ -> deps, [], inf_deps_r
| EGen gen, true, None -> deps @ [gen], [], inf_deps_r
| _, true, Some (c, _, pc) ->
let occ = if occ = None then allocc else occ in
let inf_p, inf_deps_r = List.hd inf_deps_r, List.tl inf_deps_r in
deps, [1, pc, inf_p, occ], inf_deps_r in
let patterns, clr, sigma =
loop [] orig_clr (List.length head_p+1) (List.rev deps, inf_deps_r) in
sigma, head_p @ patterns, Util.List.uniquize clr
let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
let open Proofview.Notations in
Proofview.tclEVARMAP >>= begin fun sigma ->
check_elim sigma (Option.has_some elim) what end >>=
fun (oc, orig_clr, occ, c_gen) ->
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let concl = Proofview.Goal.concl gl in
let sigma0 = sigma in
debug_ssr (fun () -> (Pp.str(if is_case then "==CASE==" else "==ELIM==")));
let sigma, seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred =
find_eliminator env sigma ~concl ~is_case ?elim oc c_gen
in
let () =
debug_ssr (fun () -> Pp.(str"elim= "++ pr_econstr_pat env sigma elim));
debug_ssr (fun () -> Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in
let open EConstr in
let inf_deps_r = match kind_of_type sigma elimty with
| AtomicType (_, args) -> List.rev (Array.to_list args)
| _ -> assert false in
let sigma, c_is_head_p = get_head_pattern env sigma elim_is_dep elim_args n_elim_args inf_deps_r cty in
debug_ssr (fun () -> Pp.(str"c_is_head_p= " ++ bool c_is_head_p));
let sigma, predty = Typing.type_of env sigma pred in
let sigma, patterns, clr = compute_patterns env sigma0 what c_is_head_p cty deps inf_deps_r occ orig_clr eqid sigma in
let pp_pat (_,p,_,occ) = Pp.(pr_occ occ ++ pp_pattern env p) in
let pp_inf_pat (_,_,t,_) = pr_econstr_pat env sigma (fire_subst sigma t) in
debug_ssr (fun () -> Pp.(pp_concat (str"patterns=") (List.map pp_pat patterns)));
debug_ssr (fun () -> Pp.(pp_concat (str"inf. patterns=") (List.map pp_inf_pat patterns)));
let sigma, elim_pred, gen_eq_tac, clr =
generate_pred env sigma0 ~concl patterns predty eqid is_rec deps elim_args n_elim_args c_is_head_p clr sigma
in
let sigma, pty = Typing.type_of env sigma elim_pred in
let sigma = List.fold_left (fun sigma (_, arg, argty) -> Typing.check env sigma arg argty) sigma elim_args in
debug_ssr (fun () -> Pp.(str"elim_pred=" ++ pr_econstr_env env sigma elim_pred));
debug_ssr (fun () -> Pp.(str"elim_pred_ty=" ++ pr_econstr_env env sigma pty));
let sigma = unify_HO env sigma pred elim_pred in
let elim = fire_subst sigma elim in
let sigma = resolve_typeclasses env sigma ~where:elim ~fail:false in
let () = check_pattern_instantiated env sigma patterns in
let elim = sigma, elim in
let seed =
Array.map (fun ty ->
let ctx,_ = EConstr.decompose_prod_assum sigma ty in
CList.rev_map Context.Rel.Declaration.get_name ctx) seed in
let elim_tac =
Tacticals.tclTHENLIST [
refine_with ~with_evars:false elim;
cleartac clr] in
Tacticals.tclTHENLIST [gen_eq_tac; elim_intro_tac ?seed:(Some seed) what eqid elim_tac is_rec clr]
end
let elimtac x =
let k ?seed:_ _what _eqid elim_tac _is_rec _clr = elim_tac in
ssrelim ~is_case:false [] (EConstr ([],None,x)) None k
let casetac x k =
let k ?seed _what _eqid elim_tac _is_rec _clr = k ?seed elim_tac in
ssrelim ~is_case:true [] (EConstr ([],None,x)) None k
let rev_id = mk_internal_id "rev concl"
let injecteq_id = mk_internal_id "injection equation"
let revtoptac n0 =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let n = nb_prod sigma concl - n0 in
let dc, cl = EConstr.decompose_prod_n_assum sigma n concl in
let ty = EConstr.it_mkProd_or_LetIn cl (List.rev dc) in
let dc' = dc @ [Context.Rel.Declaration.LocalAssum(make_annot (Name rev_id) Sorts.Relevant, ty)] in
Refine.refine ~typecheck:true begin fun sigma ->
let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in
let sigma, ev = Evarutil.new_evar env sigma ty in
sigma, (EConstr.mkApp (f, [|ev|]))
end
end
let nothing_to_inject =
CWarnings.create ~name:"spurious-ssr-injection" ~category:"ssr"
(fun (sigma, env, ty) ->
Pp.(str "SSReflect: cannot obtain new equations out of" ++ fnl() ++
str" " ++ Printer.pr_econstr_env env sigma ty ++ fnl() ++
str "Did you write an extra [] in the intro pattern?"))
let equality_inj l b id c = Proofview.Goal.enter begin fun gl ->
Proofview.tclORELSE (Equality.inj None ~injection_in_context:false l b None c)
(function
| (Equality.NothingToInject,_) ->
let open Proofview.Notations in
Ssrcommon.tacTYPEOF (EConstr.mkVar id) >>= fun ty ->
nothing_to_inject (Proofview.Goal.sigma gl, Proofview.Goal.env gl, ty);
discharge_hyp (id, (id, ""))
| (e,info) -> Proofview.tclZERO ~info e)
end
let injectidl2rtac id c =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let concl = Proofview.Goal.concl gl in
Tacticals.tclTHEN (equality_inj None true id c) (revtoptac (nb_prod sigma concl))
end
let injectl2rtac sigma c = match EConstr.kind sigma c with
| Var id -> injectidl2rtac id (EConstr.mkVar id, NoBindings)
| _ ->
let id = injecteq_id in
let xhavetac id c = Tactics.pose_proof (Name id) c in
Tacticals.tclTHENLIST [xhavetac id c; injectidl2rtac id (EConstr.mkVar id, NoBindings); Tactics.clear [id]]
let is_injection_case env sigma c =
let sigma, cty = Typing.type_of env sigma c in
let (mind,_) = Tacred.eval_to_quantified_ind env sigma cty in
Coqlib.check_ind_ref "core.eq.type" mind
let perform_injection c =
let open Proofview.Notations in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let sigma, cty = Typing.type_of env sigma c in
let mind, t = Tacred.reduce_to_quantified_ind env sigma cty in
let dc, eqt = EConstr.decompose_prod sigma t in
if dc = [] then injectl2rtac sigma c else
if not (EConstr.Vars.closed0 sigma eqt) then
CErrors.user_err (Pp.str "can't decompose a quantified equality") else
let cl = Proofview.Goal.concl gl in
let n = List.length dc in
let c_eq = mkEtaApp c n 2 in
let cl1 = EConstr.mkLambda EConstr.(make_annot Anonymous Sorts.Relevant, mkArrow eqt Sorts.Relevant cl, mkApp (mkRel 1, [|c_eq|])) in
let id = injecteq_id in
let id_with_ebind = (EConstr.mkVar id, NoBindings) in
let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in
Proofview.Unsafe.tclEVARS sigma <*>
Tacticals.tclTHENLAST (Tactics.apply (EConstr.it_mkLambda cl1 dc)) injtac
end
let ssrscase_or_inj_tac c =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
if is_injection_case env sigma c then perform_injection c
else casetac c (fun ?seed:_ k -> k)
end