diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /contrib/first-order/rules.ml |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'contrib/first-order/rules.ml')
-rw-r--r-- | contrib/first-order/rules.ml | 214 |
1 files changed, 214 insertions, 0 deletions
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml new file mode 100644 index 00000000..7fbefa37 --- /dev/null +++ b/contrib/first-order/rules.ml @@ -0,0 +1,214 @@ +(************************************************************************) +(* 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: rules.ml,v 1.24.2.1 2004/07/16 19:30:10 herbelin Exp $ *) + +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_reference (find_left t seq)) + with Not_found->tclFAIL 0 "No axiom link" + +let ll_atom_tac a backtrack id continue seq= + tclIFTHENELSE + (try + tclTHENLIST + [generalize [mkApp(constr_of_reference id, + [|constr_of_reference (find_left a seq)|])]; + clear_global id; + intro] + with Not_found->tclFAIL 0 "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 (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_reference 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_reference id)) + (Array.map f v) + backtrack gls + +let left_false_tac id= + simplest_elim (constr_of_reference 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_reference id)),[|capply|]) in + Sign.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_reference 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_reference 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 "reversible in 1st order mode" + else + backtrack) + +let left_exists_tac ind id continue seq gls= + let n=(construct_nhyps ind gls).(0) in + tclTHENLIST + [simplest_elim (constr_of_reference id); + clear_global id; + tclDO n intro; + (wrap (n-1) false continue seq)] 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_reference 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 + [[],EvalConstRef (destConst (constant "not")); + [],EvalConstRef (destConst (constant "iff"))] + +let normalize_evaluables= + onAllClauses + (function + None->unfold_in_concl (Lazy.force defined_connectives) + | Some (id,_,_)-> + unfold_in_hyp (Lazy.force defined_connectives) + (id,[],(Tacexpr.InHypTypeOnly,ref None))) |