|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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 CErrors
open Util
open Names
open EConstr
open Vars
open Tacmach.New
open Tactics
open Tacticals.New
open Proofview.Notations
open Termops
open Formula
open Sequent
open Globnames
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 n b continue seq =
Proofview.Goal.enter begin fun gls ->
Control.check_for_interrupt ();
let nc = Proofview.Goal.hyps gls in
let env=pf_env gls in
let sigma = project 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 (pf_concl gls) ||
List.exists (occur_var_in_decl env sigma id) ctx then
(aux (i-1) q (nd::ctx))
else
add_formula env sigma Hyp (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_formula env sigma Concl dummy_id (pf_concl gls) seq1 else seq1 in
continue seq2
end
let clear_global=function
VarRef id-> clear [id]
| _->tclIDTAC
(* connection rules *)
let axiom_tac t seq =
Proofview.Goal.enter begin fun gl ->
try
pf_constr_of_global (find_left (project gl) t seq) >>= fun c ->
exact_no_check c
with Not_found -> tclFAIL 0 (Pp.str "No axiom link")
end
let ll_atom_tac a backtrack id continue seq =
let open EConstr in
tclIFTHENELSE
(tclTHENLIST
[(Proofview.tclEVARMAP >>= fun sigma ->
let gr =
try Proofview.tclUNIT (find_left sigma a seq)
with Not_found -> tclFAIL 0 (Pp.str "No link")
in
gr >>= fun gr ->
pf_constr_of_global gr >>= fun left ->
pf_constr_of_global id >>= fun id ->
generalize [(mkApp(id, [|left|]))]);
clear_global id;
intro])
(wrap 1 false continue seq) backtrack
(* right connectives rules *)
let and_tac backtrack continue seq=
tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack
let or_tac backtrack continue seq=
tclORELSE
(any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq))))
backtrack
let arrow_tac backtrack continue seq=
tclIFTHENELSE intro (wrap 1 true continue seq)
(tclORELSE
(tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq)))
backtrack)
(* left connectives rules *)
let left_and_tac ind backtrack id continue seq =
Proofview.Goal.enter begin fun gl ->
let n=(construct_nhyps (pf_env gl) ind).(0) in
tclIFTHENELSE
(tclTHENLIST
[(pf_constr_of_global id >>= simplest_elim);
clear_global id;
tclDO n intro])
(wrap n false continue seq)
backtrack
end
let left_or_tac ind backtrack id continue seq =
Proofview.Goal.enter begin fun gl ->
let v=construct_nhyps (pf_env gl) ind in
let f n=
tclTHENLIST
[clear_global id;
tclDO n intro;
wrap 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.New.pf_constr_of_global id >>= simplest_elim
(* left arrow connective rules *)
(* We use this function for false, and, or, exists *)
let ll_ind_tac (ind,u as indu) largs backtrack id continue seq =
Proofview.Goal.enter begin fun gl ->
let rcs=ind_hyps (pf_env gl) (project gl) 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 (newhyps idc));
clear_global id;
tclDO lp intro])
(wrap lp false continue seq) backtrack
end
let ll_arrow_tac a b c backtrack id continue seq=
let open EConstr in
let open Vars in
let cc=mkProd(Context.make_annot Anonymous Sorts.Relevant,a,(lift 1 b)) in
let d idc = mkLambda (Context.make_annot Anonymous Sorts.Relevant,b,
mkApp (idc, [|mkLambda (Context.make_annot Anonymous Sorts.Relevant,(lift 1 a),(mkRel 2))|])) in
tclORELSE
(tclTHENS (cut c)
[tclTHENLIST
[introf;
clear_global id;
wrap 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 [d idc]);
clear_global id;
introf;
introf;
tclCOMPLETE (wrap 2 true continue seq)]]])
backtrack
(* quantifier rules (easy side) *)
let forall_tac backtrack continue seq=
tclORELSE
(tclIFTHENELSE intro (wrap 0 true continue seq)
(tclORELSE
(tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
backtrack))
(if !qflag then
tclFAIL 0 (Pp.str "reversible in 1st order mode")
else
backtrack)
let left_exists_tac ind backtrack id continue seq =
Proofview.Goal.enter begin fun gl ->
let n=(construct_nhyps (pf_env gl) ind).(0) in
tclIFTHENELSE
(Tacticals.New.pf_constr_of_global id >>= simplest_elim)
(tclTHENLIST [clear_global id;
tclDO n intro;
(wrap (n-1) false continue seq)])
backtrack
end
let ll_forall_tac 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 (pf_ids_of_hyps gls) 0 in
let term=mkApp(idc,[|mkVar(id0)|]) in
tclTHEN (generalize [term]) (clear [id0])
end);
clear_global id;
intro;
tclCOMPLETE (wrap 1 false continue (deepen seq))];
tclCOMPLETE (wrap 0 true continue (deepen seq))])
backtrack
(* rules for instantiation with unification moved to instances.ml *)
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
