aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/rules.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/rules.ml')
-rw-r--r--plugins/firstorder/rules.ml215
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))