Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258(************************************************************************)(* * 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) *)(************************************************************************)
open CErrorsopen Utilopen Namesopen EConstropen Varsopen Tacticsopen Tacticalsopen Proofview.Notationsopen Termopsopen Formulaopen Sequent
module NamedDecl = Context.Named.Declaration
type tactic = unit Proofview.tactic
type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
type lseqtac= GlobRef.t -> seqtac
type 'a with_backtracking = tactic -> 'a
let wrap ~flags n b continue seq = Proofview.Goal.enter begin fun gls -> Control.check_for_interrupt (); let nc = Proofview.Goal.hyps gls in let env = Proofview.Goal.env gls in let sigma = Proofview.Goal.sigma gls in let concl = Proofview.Goal.concl gls in let rec aux i nc ctx= if i<=0 then seq else match nc with []->anomaly (Pp.str "Not the expected number of hyps.") | nd::q-> let id = NamedDecl.get_id nd in if occur_var env sigma id concl || List.exists (occur_var_in_decl env sigma id) ctx then (aux (i-1) q (nd::ctx)) else add_formula ~flags ~hint:false env sigma (GlobRef.VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in let seq1=aux n nc [] in let seq2 = if b then add_concl ~flags env sigma concl seq1 else seq1 in continue seq2 end
let clear_global=function | GlobRef.VarRef id-> clear [id] | _->tclIDTAC
(* connection rules *)
let find_hyp ~flags seq env sigma typ = let ts = RedFlags.red_transparent flags.reds in let rec find conv = function | [] -> None | decl :: rest -> let id = NamedDecl.get_id decl in let t = NamedDecl.get_type decl in if not (Sequent.mem_hyp id seq) then find conv rest else if conv then match Reductionops.infer_conv ~ts ~pb:CUMUL env sigma t typ with | None -> find conv rest | Some sigma -> Some (sigma, id) else if EConstr.eq_constr sigma t typ then Some (sigma, id) else find conv rest in let hyps = EConstr.named_context env in match find false hyps with | Some ans -> Some ans | None -> find true hyps
let axiom_tac ~flags seq = 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 match find_hyp ~flags seq env sigma concl with | Some (sigma, hyp) -> Proofview.Unsafe.tclEVARS sigma <*> exact_no_check (mkVar hyp) | None -> tclFAIL (Pp.str "No axiom link") end
let ll_atom_tac ~flags backtrack id continue seq = let open EConstr in let tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let (sigma, id) = Evd.fresh_global env sigma id in let typ = Retyping.get_type_of env sigma id in let typ = Reductionops.clos_whd_flags flags.reds env sigma typ in let _, dom, _ = destProd sigma typ in match find_hyp ~flags seq env sigma dom with | Some (sigma, hyp) -> Proofview.Unsafe.tclEVARS sigma <*> Generalize.generalize [mkApp (id, [|mkVar hyp|])] | None -> tclFAIL (Pp.str "No link") end in tclIFTHENELSE (tclTHENLIST [tac; clear_global id; intro]) (wrap ~flags 1 false continue seq) backtrack
(* right connectives rules *)
let and_tac ~flags backtrack continue seq= tclIFTHENELSE simplest_split (wrap ~flags 0 true continue seq) backtrack
let or_tac ~flags backtrack continue seq= tclORELSE (any_constructor false (Some (tclCOMPLETE (wrap ~flags 0 true continue seq)))) backtrack
let arrow_tac ~flags backtrack continue seq= tclIFTHENELSE intro (wrap ~flags 1 true continue seq) (tclORELSE (tclTHEN introf (tclCOMPLETE (wrap ~flags 1 true continue seq))) backtrack)(* left connectives rules *)
let left_and_tac ~flags ind backtrack id continue seq = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let n = (construct_nhyps env ind).(0) in tclIFTHENELSE (tclTHENLIST [(pf_constr_of_global id >>= simplest_elim); clear_global id; tclDO n intro]) (wrap ~flags n false continue seq) backtrack end
let left_or_tac ~flags ind backtrack id continue seq = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let v = construct_nhyps env ind in let f n= tclTHENLIST [clear_global id; tclDO n intro; wrap ~flags n false continue seq] in tclIFTHENSVELSE (pf_constr_of_global id >>= simplest_elim) (Array.map f v) backtrack end
let left_false_tac id= Tacticals.pf_constr_of_global id >>= simplest_elim
(* left arrow connective rules *)
(* We use this function for false, and, or, exists *)
let ll_ind_tac ~flags (ind,u as indu) largs backtrack id continue seq = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let rcs = ind_hyps env sigma 0 indu largs in let vargs=Array.of_list largs in (* construire le terme H->B, le generaliser etc *) let myterm idc i= let rc=rcs.(i) in let p=List.length rc in let u = EInstance.make u in let cstr=mkApp ((mkConstructU ((ind,(i+1)),u)),vargs) in let vars=Array.init p (fun j->mkRel (p-j)) in let capply=mkApp ((lift p cstr),vars) in let head=mkApp ((lift p idc),[|capply|]) in EConstr.it_mkLambda_or_LetIn head rc in let lp=Array.length rcs in let newhyps idc =List.init lp (myterm idc) in tclIFTHENELSE (tclTHENLIST [(pf_constr_of_global id >>= fun idc -> Generalize.generalize (newhyps idc)); clear_global id; tclDO lp intro]) (wrap ~flags lp false continue seq) backtrack end
let ll_arrow_tac ~flags a b c backtrack id continue seq= let open EConstr in let open Vars in let cc=mkProd(Context.make_annot Anonymous ERelevance.relevant,a,(lift 1 b)) in let d idc = mkLambda (Context.make_annot Anonymous ERelevance.relevant,b, mkApp (idc, [|mkLambda (Context.make_annot Anonymous ERelevance.relevant,(lift 1 a),(mkRel 2))|])) in tclORELSE (tclTHENS (cut c) [tclTHENLIST [introf; clear_global id; wrap ~flags 1 false continue seq]; tclTHENS (cut cc) [(pf_constr_of_global id >>= fun c -> exact_no_check c); tclTHENLIST [(pf_constr_of_global id >>= fun idc -> Generalize.generalize [d idc]); clear_global id; introf; introf; tclCOMPLETE (wrap ~flags 2 true continue seq)]]]) backtrack
(* quantifier rules (easy side) *)
let forall_tac ~flags backtrack continue seq= tclORELSE (tclIFTHENELSE intro (wrap ~flags 0 true continue seq) (tclORELSE (tclTHEN introf (tclCOMPLETE (wrap ~flags 0 true continue seq))) backtrack)) (tclFAIL (Pp.str "reversible in 1st order mode"))
let left_exists_tac ~flags ind backtrack id continue seq = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let n = (construct_nhyps env ind).(0) in tclIFTHENELSE (Tacticals.pf_constr_of_global id >>= simplest_elim) (tclTHENLIST [clear_global id; tclDO n intro; (wrap (n-1) ~flags false continue seq)]) backtrack end
let ll_forall_tac ~flags prod backtrack id continue seq= tclORELSE (tclTHENS (cut prod) [tclTHENLIST [intro; (pf_constr_of_global id >>= fun idc -> Proofview.Goal.enter begin fun gls-> let open EConstr in let id0 = List.nth (Tacmach.pf_ids_of_hyps gls) 0 in let term=mkApp(idc,[|mkVar(id0)|]) in tclTHEN (Generalize.generalize [term]) (clear [id0]) end); clear_global id; intro; tclCOMPLETE (wrap ~flags 1 false continue (deepen seq))]; tclCOMPLETE (wrap ~flags 0 true continue (deepen seq))]) backtrack
(* rules for instantiation with unification moved to instances.ml *)