package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3
doc/src/ssreflect_plugin/ssrbwd.ml.html
Source file ssrbwd.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
(************************************************************************) (* * The Coq Proof Assistant / The Coq 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 Printer open Pretyping open Glob_term open Tacmach open Ssrmatching_plugin open Ssrmatching open Ssrast open Ssrcommon (** Backward chaining tactics: apply, exact, congr. *) (** The "apply" tactic *) let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) = (* ppdebug(lazy(str"sigma@interp_agen=" ++ pr_evar_map None (project gl))); *) let rc = pf_intern_term ist gl c in let rcs' = rc :: rcs in match goclr with | None -> clr, rcs' | Some ghyps -> let clr' = snd (interp_hyps ist gl ghyps) @ clr in if k <> NoFlag then clr', rcs' else let loc = rc.CAst.loc in match DAst.get rc with | GVar id when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs' | GRef (Names.GlobRef.VarRef id, _) when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs' | _ -> clr', rcs' let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl) (project gl) let interp_nbargs ist gl rc = try let rc6 = mkRApp rc (mkRHoles 6) in let sigma, t = interp_open_constr (pf_env gl) (project gl) ist (rc6, None) in let si = sig_it gl in let gl = re_sig si sigma in 6 + Ssrcommon.nbargs_open_constr (pf_env gl) t with _ -> 5 let interp_view_nbimps ist gl rc = try let sigma, t = interp_open_constr (pf_env gl) (project gl) ist (rc, None) in let si = sig_it gl in let gl = re_sig si sigma in let pl, c = splay_open_constr (pf_env gl) t in if Ssrcommon.isAppInd (pf_env gl) (project gl) c then List.length pl else (-(List.length pl)) with _ -> 0 let interp_agens ist gl gagens = match List.fold_right (interp_agen ist gl) gagens ([], []) with | clr, rlemma :: args -> let n = interp_nbargs ist gl rlemma - List.length args in let rec loop i = if i > n then errorstrm Pp.(str "Cannot apply lemma " ++ pf_pr_glob_constr gl rlemma) else try interp_refine ist gl (mkRApp rlemma (mkRHoles i @ args)) with _ -> loop (i + 1) in clr, loop 0 | _ -> assert false let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c) let apply_rconstr ?ist t gl = (* ppdebug(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *) let n = match ist, DAst.get t with | None, (GVar id | GRef (Names.GlobRef.VarRef id,_)) -> pf_nbargs (pf_env gl) (project gl) (EConstr.mkVar id) | Some ist, _ -> interp_nbargs ist gl t | _ -> anomaly "apply_rconstr without ist and not RVar" in let mkRlemma i = mkRApp t (mkRHoles i) in let cl = pf_concl gl in let rec loop i = if i > n then errorstrm Pp.(str"Cannot apply lemma "++pf_pr_glob_constr gl t) else try pf_match gl (mkRlemma i) (OfType cl) with _ -> loop (i + 1) in Proofview.V82.of_tactic (refine_with (loop 0)) gl let mkRAppView ist gl rv gv = let nb_view_imps = interp_view_nbimps ist gl rv in mkRApp rv (mkRHoles (abs nb_view_imps)) let refine_interp_apply_view dbl ist gl gv = let pair i = List.map (fun x -> i, x) in let rv = pf_intern_term ist gl gv in let v = mkRAppView ist gl rv gv in let interp_with (dbl, hint) = let i = if dbl = Ssrview.AdaptorDb.Equivalence then 2 else 1 in interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in let rec loop = function | [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv) | h :: hs -> (try Proofview.V82.of_tactic (refine_with (snd (interp_with h))) gl with _ -> loop hs) in loop (pair dbl (Ssrview.AdaptorDb.get dbl) @ if dbl = Ssrview.AdaptorDb.Equivalence then pair Ssrview.AdaptorDb.Backward (Ssrview.AdaptorDb.(get Backward)) else []) let apply_top_tac = Proofview.Goal.enter begin fun _ -> Tacticals.New.tclTHENLIST [ introid top_id; Proofview.V82.tactic (apply_rconstr (mkRVar top_id)); cleartac [SsrHyp(None,top_id)] ] end let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:false (fun gl -> let _, clr = interp_hyps ist gl gclr in let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in let ggenl, tclGENTAC = if gviews <> [] && ggenl <> [] then let ggenl= List.map (fun (x,(k,p)) -> x, {kind=k; pattern=p; interpretation= Some ist}) (List.hd ggenl) in [], Tacticals.tclTHEN (Proofview.V82.of_tactic (genstac (ggenl,[]))) else ggenl, Tacticals.tclTHEN Tacticals.tclIDTAC in tclGENTAC (fun gl -> match gviews, ggenl with | v :: tl, [] -> let dbl = if List.length tl = 1 then Ssrview.AdaptorDb.Equivalence else Ssrview.AdaptorDb.Backward in Tacticals.tclTHEN (List.fold_left (fun acc v -> Tacticals.tclTHENLAST acc (vtac v dbl)) (vtac v Ssrview.AdaptorDb.Backward) tl) (old_cleartac clr) gl | [], [agens] -> let clr', (sigma, lemma) = interp_agens ist gl agens in let gl = pf_merge_uc_of sigma gl in Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [cleartac clr; refine_with ~beta:true lemma; cleartac clr']) gl | _, _ -> Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [apply_top_tac; cleartac clr]) gl) gl ) let apply_top_tac = apply_top_tac
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>