diff options
Diffstat (limited to 'plugins/firstorder/rules.ml')
| -rw-r--r-- | plugins/firstorder/rules.ml | 215 |
1 files changed, 215 insertions, 0 deletions
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml new file mode 100644 index 000000000..fc31ee6fc --- /dev/null +++ b/plugins/firstorder/rules.ml @@ -0,0 +1,215 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +open Util +open Names +open Term +open Tacmach +open Tactics +open Tacticals +open Termops +open Declarations +open Formula +open Sequent +open Libnames + +type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic + +type lseqtac= global_reference -> seqtac + +type 'a with_backtracking = tactic -> 'a + +let wrap n b continue seq gls= + check_for_interrupt (); + let nc=pf_hyps gls in + let env=pf_env gls in + let rec aux i nc ctx= + if i<=0 then seq else + match nc with + []->anomaly "Not the expected number of hyps" + | ((id,_,typ) as nd)::q-> + if occur_var env id (pf_concl gls) || + List.exists (occur_var_in_decl env id) ctx then + (aux (i-1) q (nd::ctx)) + else + add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in + let seq1=aux n nc [] in + let seq2=if b then + add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in + continue seq2 gls + +let id_of_global=function + VarRef id->id + | _->assert false + +let clear_global=function + VarRef id->clear [id] + | _->tclIDTAC + + +(* connection rules *) + +let axiom_tac t seq= + try exact_no_check (constr_of_global (find_left t seq)) + with Not_found->tclFAIL 0 (Pp.str "No axiom link") + +let ll_atom_tac a backtrack id continue seq= + tclIFTHENELSE + (try + tclTHENLIST + [generalize [mkApp(constr_of_global id, + [|constr_of_global (find_left a seq)|])]; + clear_global id; + intro] + with Not_found->tclFAIL 0 (Pp.str "No link")) + (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 gls= + let n=(construct_nhyps ind gls).(0) in + tclIFTHENELSE + (tclTHENLIST + [simplest_elim (constr_of_global id); + clear_global id; + tclDO n intro]) + (wrap n false continue seq) + backtrack gls + +let left_or_tac ind backtrack id continue seq gls= + let v=construct_nhyps ind gls in + let f n= + tclTHENLIST + [clear_global id; + tclDO n intro; + wrap n false continue seq] in + tclIFTHENSVELSE + (simplest_elim (constr_of_global id)) + (Array.map f v) + backtrack gls + +let left_false_tac id= + simplest_elim (constr_of_global id) + +(* left arrow connective rules *) + +(* We use this function for false, and, or, exists *) + +let ll_ind_tac ind largs backtrack id continue seq gl= + let rcs=ind_hyps 0 ind largs gl in + let vargs=Array.of_list largs in + (* construire le terme H->B, le generaliser etc *) + let myterm i= + let rc=rcs.(i) in + let p=List.length rc in + let cstr=mkApp ((mkConstruct (ind,(i+1))),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 (constr_of_global id)),[|capply|]) in + it_mkLambda_or_LetIn head rc in + let lp=Array.length rcs in + let newhyps=list_tabulate myterm lp in + tclIFTHENELSE + (tclTHENLIST + [generalize newhyps; + clear_global id; + tclDO lp intro]) + (wrap lp false continue seq) backtrack gl + +let ll_arrow_tac a b c backtrack id continue seq= + let cc=mkProd(Anonymous,a,(lift 1 b)) in + let d=mkLambda (Anonymous,b, + mkApp ((constr_of_global id), + [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in + tclORELSE + (tclTHENS (cut c) + [tclTHENLIST + [introf; + clear_global id; + wrap 1 false continue seq]; + tclTHENS (cut cc) + [exact_no_check (constr_of_global id); + tclTHENLIST + [generalize [d]; + 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 gls= + let n=(construct_nhyps ind gls).(0) in + tclIFTHENELSE + (simplest_elim (constr_of_global id)) + (tclTHENLIST [clear_global id; + tclDO n intro; + (wrap (n-1) false continue seq)]) + backtrack + gls + +let ll_forall_tac prod backtrack id continue seq= + tclORELSE + (tclTHENS (cut prod) + [tclTHENLIST + [intro; + (fun gls-> + let id0=pf_nth_hyp_id gls 1 in + let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in + tclTHEN (generalize [term]) (clear [id0]) gls); + 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 *) + +(* special for compatibility with old Intuition *) + +let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str + +let defined_connectives=lazy + [all_occurrences,EvalConstRef (destConst (constant "not")); + all_occurrences,EvalConstRef (destConst (constant "iff"))] + +let normalize_evaluables= + onAllHypsAndConcl + (function + None->unfold_in_concl (Lazy.force defined_connectives) + | Some id -> + unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)) |