package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/src/ssreflect_plugin/ssrelim.ml.html
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 605 606
(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) 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 *) (* TASSI: given the type of an elimination principle, it finds the higher order * argument (index), it computes it's arity and the arity of the eliminator and * checks if the eliminator is recursive or not *) 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) (* A case without explicit dependent terms but with both a view and an *) (* occurrence switch and/or an equation is treated as dependent, with the *) (* viewed term as the dependent term (the occurrence switch would be *) (* meaningless otherwise). When both a view and explicit dependents are *) (* present, it is forbidden to put a (meaningless) occurrence switch on *) (* the viewed term. *) (* This is both elim and case (defaulting to the former). If ~elim is omitted * the standard eliminator is chosen. The code is made of 4 parts: * 1. find the eliminator if not given as ~elim and analyze it * 2. build the patterns to be matched against the conclusion, looking at * (occ, c), deps and the pattern inferred from the type of the eliminator * 3. build the new predicate matching the patterns, and the tactic to * generalize the equality in case eqid is not None * 4. build the tactic handle instructions and clears as required in ipats and * by eqid *) let get_eq_type env sigma = Evd.fresh_global env sigma Rocqlib.(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) = (* takes a term, refreshes it and makes a T pattern *) 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.ustate sigma let unif_redex env sigma0 nsigma p t = (* t is a hint for the redex of p *) 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_exn (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_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) (EConstr.ESorts.family sigma sort)) in let elimty = Retyping.get_type_of env sigma elim in sigma, elim, elimty else let sigma, case = Indrec.build_case_analysis_scheme env sigma indu true sort in let (ind, indty) = Indrec.eval_case_analysis case in (sigma, ind, 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_decls 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_decls 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 (* The user wrote elim: _ *) | 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 (* Unify two terms if their heads are not applied unif variables, eg * not (?P x). The idea is to rule out cases where the problem is too * vague to drive the current heuristics. *) 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 () = (* we try to see if c unifies with the last arg of elim *) 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 () = (* we try to see if c unifies with the last inferred 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_undefined 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_decls 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 EConstr.ERelevance.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.ustate sigma in let evds = Evar.Map.bind (Evd.find_undefined 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 EConstr.ERelevance.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 (* if we are the index for the equation we do not clear *) 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 -> (* some sanity checks *) 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=="))); (* finds the eliminator applies it to evars and c saturated as needed *) (* obtaining "elim ??? (c ???)". pred is the higher order evar *) (* cty is None when the user writes _ (hence we can't make a pattern *) (* `seed` represents the array of types from which we derive the name seeds for the block intro patterns *) 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 (* Here we try to understand if the main pattern/term the user gave is * the first pattern to be matched (i.e. if elimty ends in P t1 .. tn, * wether tn is the t the user wrote in 'elim: t' *) 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 (* Patterns for the inductive types indexes to be bound in pred are computed * looking at the ones provided by the user and the inferred ones looking at * the type of the elimination principle *) 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))); (* Predicate generation, and (if necessary) tactic to generalize the * equation asked by the user *) 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 (* check that the patterns do not contain non instantiated dependent metas *) let () = check_pattern_instantiated env sigma patterns in (* the elim tactic, with the eliminator and the predicated we computed *) let elim = sigma, elim in let seed = Array.map (fun ty -> let ctx,_ = EConstr.decompose_prod_decls 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_decls 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) EConstr.ERelevance.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:CWarnings.CoreCategories.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 Rocqlib.check_ref "core.eq.type" (GlobRef.IndRef 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 ERelevance.relevant, mkArrow eqt ERelevance.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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>