From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- contrib/firstorder/formula.ml | 270 ++++++++++++++++++++++++++++++++++ contrib/firstorder/formula.mli | 77 ++++++++++ contrib/firstorder/g_ground.ml4 | 128 +++++++++++++++++ contrib/firstorder/ground.ml | 152 ++++++++++++++++++++ contrib/firstorder/ground.mli | 13 ++ contrib/firstorder/instances.ml | 206 ++++++++++++++++++++++++++ contrib/firstorder/instances.mli | 26 ++++ contrib/firstorder/rules.ml | 216 ++++++++++++++++++++++++++++ contrib/firstorder/rules.mli | 54 +++++++ contrib/firstorder/sequent.ml | 303 +++++++++++++++++++++++++++++++++++++++ contrib/firstorder/sequent.mli | 66 +++++++++ contrib/firstorder/unify.ml | 143 ++++++++++++++++++ contrib/firstorder/unify.mli | 23 +++ 13 files changed, 1677 insertions(+) create mode 100644 contrib/firstorder/formula.ml create mode 100644 contrib/firstorder/formula.mli create mode 100644 contrib/firstorder/g_ground.ml4 create mode 100644 contrib/firstorder/ground.ml create mode 100644 contrib/firstorder/ground.mli create mode 100644 contrib/firstorder/instances.ml create mode 100644 contrib/firstorder/instances.mli create mode 100644 contrib/firstorder/rules.ml create mode 100644 contrib/firstorder/rules.mli create mode 100644 contrib/firstorder/sequent.ml create mode 100644 contrib/firstorder/sequent.mli create mode 100644 contrib/firstorder/unify.ml create mode 100644 contrib/firstorder/unify.mli (limited to 'contrib/firstorder') diff --git a/contrib/firstorder/formula.ml b/contrib/firstorder/formula.ml new file mode 100644 index 00000000..3e49cd9c --- /dev/null +++ b/contrib/firstorder/formula.ml @@ -0,0 +1,270 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* metavariable + +exception Is_atom of constr + +let meta_succ m = m+1 + +let rec nb_prod_after n c= + match kind_of_term c with + | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else + 1+(nb_prod_after 0 b) + | _ -> 0 + +let construct_nhyps ind gls = + let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in + let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in + let hyp = nb_prod_after nparams in + Array.map hyp constr_types + +(* indhyps builds the array of arrays of constructor hyps for (ind largs)*) +let ind_hyps nevar ind largs gls= + let types= Inductiveops.arities_of_constructors (pf_env gls) ind in + let lp=Array.length types in + let myhyps i= + let t1=Term.prod_applist types.(i) largs in + let t2=snd (Sign.decompose_prod_n_assum nevar t1) in + fst (Sign.decompose_prod_assum t2) in + Array.init lp myhyps + +let special_nf gl= + let infos=Closure.create_clos_infos !red_flags (pf_env gl) in + (fun t -> Closure.norm_val infos (Closure.inject t)) + +let special_whd gl= + let infos=Closure.create_clos_infos !red_flags (pf_env gl) in + (fun t -> Closure.whd_val infos (Closure.inject t)) + +type kind_of_formula= + Arrow of constr*constr + | False of inductive*constr list + | And of inductive*constr list*bool + | Or of inductive*constr list*bool + | Exists of inductive*constr list + | Forall of constr*constr + | Atom of constr + +let rec kind_of_formula gl term = + let normalize=special_nf gl in + let cciterm=special_whd gl term in + match match_with_imp_term cciterm with + Some (a,b)-> Arrow(a,(pop b)) + |_-> + match match_with_forall_term cciterm with + Some (_,a,b)-> Forall(a,b) + |_-> + match match_with_nodep_ind cciterm with + Some (i,l,n)-> + let ind=destInd i in + let (mib,mip) = Global.lookup_inductive ind in + let nconstr=Array.length mip.mind_consnames in + if nconstr=0 then + False(ind,l) + else + let has_realargs=(n>0) in + let is_trivial= + let is_constant c = + nb_prod c = mib.mind_nparams in + array_exists is_constant mip.mind_nf_lc in + if Inductiveops.mis_is_recursive (ind,mib,mip) || + (has_realargs && not is_trivial) + then + Atom cciterm + else + if nconstr=1 then + And(ind,l,is_trivial) + else + Or(ind,l,is_trivial) + | _ -> + match match_with_sigma_type cciterm with + Some (i,l)-> Exists((destInd i),l) + |_-> Atom (normalize cciterm) + +type atoms = {positive:constr list;negative:constr list} + +type side = Hyp | Concl | Hint + +let no_atoms = (false,{positive=[];negative=[]}) + +let dummy_id=VarRef (id_of_string "_") (* "_" cannot be parsed *) + +let build_atoms gl metagen side cciterm = + let trivial =ref false + and positive=ref [] + and negative=ref [] in + let normalize=special_nf gl in + let rec build_rec env polarity cciterm= + match kind_of_formula gl cciterm with + False(_,_)->if not polarity then trivial:=true + | Arrow (a,b)-> + build_rec env (not polarity) a; + build_rec env polarity b + | And(i,l,b) | Or(i,l,b)-> + if b then + begin + let unsigned=normalize (substnl env 0 cciterm) in + if polarity then + positive:= unsigned :: !positive + else + negative:= unsigned :: !negative + end; + let v = ind_hyps 0 i l gl in + let g i _ (_,_,t) = + build_rec env polarity (lift i t) in + let f l = + list_fold_left_i g (1-(List.length l)) () l in + if polarity && (* we have a constant constructor *) + array_exists (function []->true|_->false) v + then trivial:=true; + Array.iter f v + | Exists(i,l)-> + let var=mkMeta (metagen true) in + let v =(ind_hyps 1 i l gl).(0) in + let g i _ (_,_,t) = + build_rec (var::env) polarity (lift i t) in + list_fold_left_i g (2-(List.length l)) () v + | Forall(_,b)-> + let var=mkMeta (metagen true) in + build_rec (var::env) polarity b + | Atom t-> + let unsigned=substnl env 0 t in + if not (isMeta unsigned) then (* discarding wildcard atoms *) + if polarity then + positive:= unsigned :: !positive + else + negative:= unsigned :: !negative in + begin + match side with + Concl -> build_rec [] true cciterm + | Hyp -> build_rec [] false cciterm + | Hint -> + let rels,head=decompose_prod cciterm in + let env=List.rev (List.map (fun _->mkMeta (metagen true)) rels) in + build_rec env false head;trivial:=false (* special for hints *) + end; + (!trivial, + {positive= !positive; + negative= !negative}) + +type right_pattern = + Rarrow + | Rand + | Ror + | Rfalse + | Rforall + | Rexists of metavariable*constr*bool + +type left_arrow_pattern= + LLatom + | LLfalse of inductive*constr list + | LLand of inductive*constr list + | LLor of inductive*constr list + | LLforall of constr + | LLexists of inductive*constr list + | LLarrow of constr*constr*constr + +type left_pattern= + Lfalse + | Land of inductive + | Lor of inductive + | Lforall of metavariable*constr*bool + | Lexists of inductive + | LA of constr*left_arrow_pattern + +type t={id:global_reference; + constr:constr; + pat:(left_pattern,right_pattern) sum; + atoms:atoms} + +let build_formula side nam typ gl metagen= + let normalize = special_nf gl in + try + let m=meta_succ(metagen false) in + let trivial,atoms= + if !qflag then + build_atoms gl metagen side typ + else no_atoms in + let pattern= + match side with + Concl -> + let pat= + match kind_of_formula gl typ with + False(_,_) -> Rfalse + | Atom a -> raise (Is_atom a) + | And(_,_,_) -> Rand + | Or(_,_,_) -> Ror + | Exists (i,l) -> + let (_,_,d)=list_last (ind_hyps 0 i l gl).(0) in + Rexists(m,d,trivial) + | Forall (_,a) -> Rforall + | Arrow (a,b) -> Rarrow in + Right pat + | _ -> + let pat= + match kind_of_formula gl typ with + False(i,_) -> Lfalse + | Atom a -> raise (Is_atom a) + | And(i,_,b) -> + if b then + let nftyp=normalize typ in raise (Is_atom nftyp) + else Land i + | Or(i,_,b) -> + if b then + let nftyp=normalize typ in raise (Is_atom nftyp) + else Lor i + | Exists (ind,_) -> Lexists ind + | Forall (d,_) -> + Lforall(m,d,trivial) + | Arrow (a,b) -> + let nfa=normalize a in + LA (nfa, + match kind_of_formula gl a with + False(i,l)-> LLfalse(i,l) + | Atom t-> LLatom + | And(i,l,_)-> LLand(i,l) + | Or(i,l,_)-> LLor(i,l) + | Arrow(a,c)-> LLarrow(a,c,b) + | Exists(i,l)->LLexists(i,l) + | Forall(_,_)->LLforall a) in + Left pat + in + Left {id=nam; + constr=normalize typ; + pat=pattern; + atoms=atoms} + with Is_atom a-> Right a (* already in nf *) + diff --git a/contrib/firstorder/formula.mli b/contrib/firstorder/formula.mli new file mode 100644 index 00000000..8703045c --- /dev/null +++ b/contrib/firstorder/formula.mli @@ -0,0 +1,77 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a -> int) -> ('b -> 'b -> int) -> + 'a -> 'a -> 'b -> 'b -> int + +val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) -> + 'a -> 'a -> 'b -> 'b -> 'c ->'c -> int + +type ('a,'b) sum = Left of 'a | Right of 'b + +type counter = bool -> metavariable + +val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array + +val ind_hyps : int -> inductive -> constr list -> + Proof_type.goal Tacmach.sigma -> Sign.rel_context array + +type atoms = {positive:constr list;negative:constr list} + +type side = Hyp | Concl | Hint + +val dummy_id: global_reference + +val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> + side -> constr -> bool * atoms + +type right_pattern = + Rarrow + | Rand + | Ror + | Rfalse + | Rforall + | Rexists of metavariable*constr*bool + +type left_arrow_pattern= + LLatom + | LLfalse of inductive*constr list + | LLand of inductive*constr list + | LLor of inductive*constr list + | LLforall of constr + | LLexists of inductive*constr list + | LLarrow of constr*constr*constr + +type left_pattern= + Lfalse + | Land of inductive + | Lor of inductive + | Lforall of metavariable*constr*bool + | Lexists of inductive + | LA of constr*left_arrow_pattern + +type t={id: global_reference; + constr: constr; + pat: (left_pattern,right_pattern) sum; + atoms: atoms} + +(*exception Is_atom of constr*) + +val build_formula : side -> global_reference -> types -> + Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum + diff --git a/contrib/firstorder/g_ground.ml4 b/contrib/firstorder/g_ground.ml4 new file mode 100644 index 00000000..f7b0a546 --- /dev/null +++ b/contrib/firstorder/g_ground.ml4 @@ -0,0 +1,128 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Some !ground_depth); + optwrite= + (function + None->ground_depth:=3 + | Some i->ground_depth:=(max i 0))} + in + declare_int_option gdopt + +let congruence_depth=ref 100 + +let _= + let gdopt= + { optsync=true; + optname="Congruence Depth"; + optkey=SecondaryTable("Congruence","Depth"); + optread=(fun ()->Some !congruence_depth); + optwrite= + (function + None->congruence_depth:=0 + | Some i->congruence_depth:=(max i 0))} + in + declare_int_option gdopt + +let default_solver=(Tacinterp.interp <:tactic>) + +let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") + +type external_env= + Ids of global_reference list + | Bases of Auto.hint_db_name list + | Void + +let gen_ground_tac flag taco ext gl= + let backup= !qflag in + try + qflag:=flag; + let solver= + match taco with + Some tac-> tac + | None-> default_solver in + let startseq= + match ext with + Void -> (fun gl -> empty_seq !ground_depth) + | Ids l-> create_with_ref_list l !ground_depth + | Bases l-> create_with_auto_hints l !ground_depth in + let result=ground_tac solver startseq gl in + qflag:=backup;result + with e ->qflag:=backup;raise e + +(* special for compatibility with 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) + (Tacexpr.InHypType id)) *) + +TACTIC EXTEND firstorder + [ "firstorder" tactic_opt(t) "using" ne_reference_list(l) ] -> + [ gen_ground_tac true (Option.map eval_tactic t) (Ids l) ] +| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> + [ gen_ground_tac true (Option.map eval_tactic t) (Bases l) ] +| [ "firstorder" tactic_opt(t) ] -> + [ gen_ground_tac true (Option.map eval_tactic t) Void ] +END + +TACTIC EXTEND gintuition + [ "gintuition" tactic_opt(t) ] -> + [ gen_ground_tac false (Option.map eval_tactic t) Void ] +END + + +let default_declarative_automation gls = + tclORELSE + (tclORELSE (Auto.h_trivial [] None) + (Cctac.congruence_tac !congruence_depth [])) + (gen_ground_tac true + (Some (tclTHEN + default_solver + (Cctac.congruence_tac !congruence_depth []))) + Void) gls + + + +let () = + Decl_proof_instr.register_automation_tac default_declarative_automation + diff --git a/contrib/firstorder/ground.ml b/contrib/firstorder/ground.ml new file mode 100644 index 00000000..f4661869 --- /dev/null +++ b/contrib/firstorder/ground.ml @@ -0,0 +1,152 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + predref:=Names.KNpred.add kn !predref + | _ ->() in + let g _ l=List.iter f l in + let h _ hdb=Auto.Hint_db.iter g hdb in + Util.Stringmap.iter h !Auto.searchtable; + red_flags:= + Closure.RedFlags.red_add_transparent + Closure.betaiotazeta (Names.Idpred.full,!predref) + end +*) + +let update_flags ()= + let predref=ref Names.Cpred.empty in + let f coe= + try + let kn=destConst (Classops.get_coercion_value coe) in + predref:=Names.Cpred.add kn !predref + with Invalid_argument "destConst"-> () in + List.iter f (Classops.coercions ()); + red_flags:= + Closure.RedFlags.red_add_transparent + Closure.betaiotazeta + (Names.Idpred.full,Names.Cpred.complement !predref) + +let ground_tac solver startseq gl= + update_flags (); + let rec toptac skipped seq gl= + if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 + then Pp.msgnl (Printer.pr_goal (sig_it gl)); + tclORELSE (axiom_tac seq.gl seq) + begin + try + let (hd,seq1)=take_formula seq + and re_add s=re_add_formula_list skipped s in + let continue=toptac [] + and backtrack gl=toptac (hd::skipped) seq1 gl in + match hd.pat with + Right rpat-> + begin + match rpat with + Rand-> + and_tac backtrack continue (re_add seq1) + | Rforall-> + let backtrack1= + if !qflag then + tclFAIL 0 (Pp.str "reversible in 1st order mode") + else + backtrack in + forall_tac backtrack1 continue (re_add seq1) + | Rarrow-> + arrow_tac backtrack continue (re_add seq1) + | Ror-> + or_tac backtrack continue (re_add seq1) + | Rfalse->backtrack + | Rexists(i,dom,triv)-> + let (lfp,seq2)=collect_quantified seq in + let backtrack2=toptac (lfp@skipped) seq2 in + if !qflag && seq.depth>0 then + quantified_tac lfp backtrack2 + continue (re_add seq) + else + backtrack2 (* need special backtracking *) + end + | Left lpat-> + begin + match lpat with + Lfalse-> + left_false_tac hd.id + | Land ind-> + left_and_tac ind backtrack + hd.id continue (re_add seq1) + | Lor ind-> + left_or_tac ind backtrack + hd.id continue (re_add seq1) + | Lforall (_,_,_)-> + let (lfp,seq2)=collect_quantified seq in + let backtrack2=toptac (lfp@skipped) seq2 in + if !qflag && seq.depth>0 then + quantified_tac lfp backtrack2 + continue (re_add seq) + else + backtrack2 (* need special backtracking *) + | Lexists ind -> + if !qflag then + left_exists_tac ind backtrack hd.id + continue (re_add seq1) + else backtrack + | LA (typ,lap)-> + let la_tac= + begin + match lap with + LLatom -> backtrack + | LLand (ind,largs) | LLor(ind,largs) + | LLfalse (ind,largs)-> + (ll_ind_tac ind largs backtrack + hd.id continue (re_add seq1)) + | LLforall p -> + if seq.depth>0 && !qflag then + (ll_forall_tac p backtrack + hd.id continue (re_add seq1)) + else backtrack + | LLexists (ind,l) -> + if !qflag then + ll_ind_tac ind l backtrack + hd.id continue (re_add seq1) + else + backtrack + | LLarrow (a,b,c) -> + (ll_arrow_tac a b c backtrack + hd.id continue (re_add seq1)) + end in + ll_atom_tac typ la_tac hd.id continue (re_add seq1) + end + with Heap.EmptyHeap->solver + end gl in + wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl + diff --git a/contrib/firstorder/ground.mli b/contrib/firstorder/ground.mli new file mode 100644 index 00000000..621f99db --- /dev/null +++ b/contrib/firstorder/ground.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic + diff --git a/contrib/firstorder/instances.ml b/contrib/firstorder/instances.ml new file mode 100644 index 00000000..1432207d --- /dev/null +++ b/contrib/firstorder/instances.ml @@ -0,0 +1,206 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (OrderedConstr.compare d1 d2) + | Real((m1,c1),n1),Real((m2,c2),n2)-> + ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2 + | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1 + | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1 + +let compare_gr id1 id2= + if id1==id2 then 0 else + if id1==dummy_id then 1 + else if id2==dummy_id then -1 + else Pervasives.compare id1 id2 + +module OrderedInstance= +struct + type t=instance * Libnames.global_reference + let compare (inst1,id1) (inst2,id2)= + (compare_instance =? compare_gr) inst2 inst1 id2 id1 + (* we want a __decreasing__ total order *) +end + +module IS=Set.Make(OrderedInstance) + +let make_simple_atoms seq= + let ratoms= + match seq.glatom with + Some t->[t] + | None->[] + in {negative=seq.latoms;positive=ratoms} + +let do_sequent setref triv id seq i dom atoms= + let flag=ref true in + let phref=ref triv in + let do_atoms a1 a2 = + let do_pair t1 t2 = + match unif_atoms i dom t1 t2 with + None->() + | Some (Phantom _) ->phref:=true + | Some c ->flag:=false;setref:=IS.add (c,id) !setref in + List.iter (fun t->List.iter (do_pair t) a2.negative) a1.positive; + List.iter (fun t->List.iter (do_pair t) a2.positive) a1.negative in + HP.iter (fun lf->do_atoms atoms lf.atoms) seq.redexes; + do_atoms atoms (make_simple_atoms seq); + !flag && !phref + +let match_one_quantified_hyp setref seq lf= + match lf.pat with + Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))-> + if do_sequent setref triv lf.id seq i dom lf.atoms then + setref:=IS.add ((Phantom dom),lf.id) !setref + | _ ->anomaly "can't happen" + +let give_instances lf seq= + let setref=ref IS.empty in + List.iter (match_one_quantified_hyp setref seq) lf; + IS.elements !setref + +(* collector for the engine *) + +let rec collect_quantified seq= + try + let hd,seq1=take_formula seq in + (match hd.pat with + Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) -> + let (q,seq2)=collect_quantified seq1 in + ((hd::q),seq2) + | _->[],seq) + with Heap.EmptyHeap -> [],seq + +(* open instances processor *) + +let dummy_constr=mkMeta (-1) + +let dummy_bvid=id_of_string "x" + +let mk_open_instance id gl m t= + let env=pf_env gl in + let evmap=Refiner.project gl in + let var_id= + if id==dummy_id then dummy_bvid else + let typ=pf_type_of gl (constr_of_global id) in + (* since we know we will get a product, + reduction is not too expensive *) + let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in + match nam with + Name id -> id + | Anonymous -> dummy_bvid in + let revt=substl (list_tabulate (fun i->mkRel (m-i)) m) t in + let rec aux n avoid= + if n=0 then [] else + let nid=(fresh_id avoid var_id gl) in + (Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in + let nt=it_mkLambda_or_LetIn revt (aux m []) in + let rawt=Detyping.detype false [] [] nt in + let rec raux n t= + if n=0 then t else + match t with + RLambda(loc,name,k,_,t0)-> + let t1=raux (n-1) t0 in + RLambda(loc,name,k,RHole (dummy_loc,Evd.BinderType name),t1) + | _-> anomaly "can't happen" in + let ntt=try + Pretyping.Default.understand evmap env (raux m rawt) + with _ -> + error "Untypable instance, maybe higher-order non-prenex quantification" in + Sign.decompose_lam_n_assum m ntt + +(* tactics *) + +let left_instance_tac (inst,id) continue seq= + match inst with + Phantom dom-> + if lookup (id,None) seq then + tclFAIL 0 (Pp.str "already done") + else + tclTHENS (cut dom) + [tclTHENLIST + [introf; + (fun gls->generalize + [mkApp(constr_of_global id, + [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); + introf; + tclSOLVE [wrap 1 false continue + (deepen (record (id,None) seq))]]; + tclTRY assumption] + | Real((m,t) as c,_)-> + if lookup (id,Some c) seq then + tclFAIL 0 (Pp.str "already done") + else + let special_generalize= + if m>0 then + fun gl-> + let (rc,ot)= mk_open_instance id gl m t in + let gt= + it_mkLambda_or_LetIn + (mkApp(constr_of_global id,[|ot|])) rc in + generalize [gt] gl + else + generalize [mkApp(constr_of_global id,[|t|])] + in + tclTHENLIST + [special_generalize; + introf; + tclSOLVE + [wrap 1 false continue (deepen (record (id,Some c) seq))]] + +let right_instance_tac inst continue seq= + match inst with + Phantom dom -> + tclTHENS (cut dom) + [tclTHENLIST + [introf; + (fun gls-> + split (Rawterm.ImplicitBindings + [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); + tclSOLVE [wrap 0 true continue (deepen seq)]]; + tclTRY assumption] + | Real ((0,t),_) -> + (tclTHEN (split (Rawterm.ImplicitBindings [t])) + (tclSOLVE [wrap 0 true continue (deepen seq)])) + | Real ((m,t),_) -> + tclFAIL 0 (Pp.str "not implemented ... yet") + +let instance_tac inst= + if (snd inst)==dummy_id then + right_instance_tac (fst inst) + else + left_instance_tac inst + +let quantified_tac lf backtrack continue seq gl= + let insts=give_instances lf seq in + tclORELSE + (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts)) + backtrack gl + + diff --git a/contrib/firstorder/instances.mli b/contrib/firstorder/instances.mli new file mode 100644 index 00000000..7667c89f --- /dev/null +++ b/contrib/firstorder/instances.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Formula.t list * Sequent.t + +val give_instances : Formula.t list -> Sequent.t -> + (Unify.instance * global_reference) list + +val quantified_tac : Formula.t list -> seqtac with_backtracking + + + + diff --git a/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml new file mode 100644 index 00000000..b8b56548 --- /dev/null +++ b/contrib/firstorder/rules.ml @@ -0,0 +1,216 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 + 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_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= + onAllClauses + (function + None->unfold_in_concl (Lazy.force defined_connectives) + | Some ((_,id),_)-> + unfold_in_hyp (Lazy.force defined_connectives) + ((Rawterm.all_occurrences_expr,id),Tacexpr.InHypTypeOnly)) diff --git a/contrib/firstorder/rules.mli b/contrib/firstorder/rules.mli new file mode 100644 index 00000000..3798d8d4 --- /dev/null +++ b/contrib/firstorder/rules.mli @@ -0,0 +1,54 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* tactic) -> Sequent.t -> tactic + +type lseqtac= global_reference -> seqtac + +type 'a with_backtracking = tactic -> 'a + +val wrap : int -> bool -> seqtac + +val id_of_global: global_reference -> identifier + +val clear_global: global_reference -> tactic + +val axiom_tac : constr -> Sequent.t -> tactic + +val ll_atom_tac : constr -> lseqtac with_backtracking + +val and_tac : seqtac with_backtracking + +val or_tac : seqtac with_backtracking + +val arrow_tac : seqtac with_backtracking + +val left_and_tac : inductive -> lseqtac with_backtracking + +val left_or_tac : inductive -> lseqtac with_backtracking + +val left_false_tac : global_reference -> tactic + +val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking + +val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking + +val forall_tac : seqtac with_backtracking + +val left_exists_tac : inductive -> lseqtac with_backtracking + +val ll_forall_tac : types -> lseqtac with_backtracking + +val normalize_evaluables : tactic diff --git a/contrib/firstorder/sequent.ml b/contrib/firstorder/sequent.ml new file mode 100644 index 00000000..c832d30f --- /dev/null +++ b/contrib/firstorder/sequent.ml @@ -0,0 +1,303 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* if b then incr cnt;!cnt + +let priority = (* pure heuristics, <=0 for non reversible *) + function + Right rf-> + begin + match rf with + Rarrow -> 100 + | Rand -> 40 + | Ror -> -15 + | Rfalse -> -50 + | Rforall -> 100 + | Rexists (_,_,_) -> -29 + end + | Left lf -> + match lf with + Lfalse -> 999 + | Land _ -> 90 + | Lor _ -> 40 + | Lforall (_,_,_) -> -30 + | Lexists _ -> 60 + | LA(_,lap) -> + match lap with + LLatom -> 0 + | LLfalse (_,_) -> 100 + | LLand (_,_) -> 80 + | LLor (_,_) -> 70 + | LLforall _ -> -20 + | LLexists (_,_) -> 50 + | LLarrow (_,_,_) -> -10 + +let left_reversible lpat=(priority lpat)>0 + +module OrderedFormula= +struct + type t=Formula.t + let compare e1 e2= + (priority e1.pat) - (priority e2.pat) +end + +(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare + the immediate subterms of [c1] of [c2] if needed; Cast's, + application associativity, binders name and Cases annotations are + not taken into account *) + +let rec compare_list f l1 l2= + match l1,l2 with + [],[]-> 0 + | [],_ -> -1 + | _,[] -> 1 + | (h1::q1),(h2::q2) -> (f =? (compare_list f)) h1 h2 q1 q2 + +let compare_array f v1 v2= + let l=Array.length v1 in + let c=l - Array.length v2 in + if c=0 then + let rec comp_aux i= + if i<0 then 0 + else + let ci=f v1.(i) v2.(i) in + if ci=0 then + comp_aux (i-1) + else ci + in comp_aux (l-1) + else c + +let compare_constr_int f t1 t2 = + match kind_of_term t1, kind_of_term t2 with + | Rel n1, Rel n2 -> n1 - n2 + | Meta m1, Meta m2 -> m1 - m2 + | Var id1, Var id2 -> Pervasives.compare id1 id2 + | Sort s1, Sort s2 -> Pervasives.compare s1 s2 + | Cast (c1,_,_), _ -> f c1 t2 + | _, Cast (c2,_,_) -> f t1 c2 + | Prod (_,t1,c1), Prod (_,t2,c2) + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> + (f =? f) t1 t2 c1 c2 + | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> + ((f =? f) ==? f) b1 b2 t1 t2 c1 c2 + | App (_,_), App (_,_) -> + let c1,l1=decompose_app t1 + and c2,l2=decompose_app t2 in + (f =? (compare_list f)) c1 c2 l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> + ((-) =? (compare_array f)) e1 e2 l1 l2 + | Const c1, Const c2 -> Pervasives.compare c1 c2 + | Ind c1, Ind c2 -> Pervasives.compare c1 c2 + | Construct c1, Construct c2 -> Pervasives.compare c1 c2 + | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> + ((f =? f) ==? (compare_array f)) p1 p2 c1 c2 bl1 bl2 + | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> + ((Pervasives.compare =? (compare_array f)) ==? (compare_array f)) + ln1 ln2 tl1 tl2 bl1 bl2 + | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> + ((Pervasives.compare =? (compare_array f)) ==? (compare_array f)) + ln1 ln2 tl1 tl2 bl1 bl2 + | _ -> Pervasives.compare t1 t2 + +let rec compare_constr m n= + compare_constr_int compare_constr m n + +module OrderedConstr= +struct + type t=constr + let compare=compare_constr +end + +type h_item = global_reference * (int*constr) option + +module Hitem= +struct + type t = h_item + let compare (id1,co1) (id2,co2)= + (Pervasives.compare + =? (fun oc1 oc2 -> + match oc1,oc2 with + Some (m1,c1),Some (m2,c2) -> + ((-) =? OrderedConstr.compare) m1 m2 c1 c2 + | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2 +end + +module CM=Map.Make(OrderedConstr) + +module History=Set.Make(Hitem) + +let cm_add typ nam cm= + try + let l=CM.find typ cm in CM.add typ (nam::l) cm + with + Not_found->CM.add typ [nam] cm + +let cm_remove typ nam cm= + try + let l=CM.find typ cm in + let l0=List.filter (fun id->id<>nam) l in + match l0 with + []->CM.remove typ cm + | _ ->CM.add typ l0 cm + with Not_found ->cm + +module HP=Heap.Functional(OrderedFormula) + +type t= + {redexes:HP.t; + context:(global_reference list) CM.t; + latoms:constr list; + gl:types; + glatom:constr option; + cnt:counter; + history:History.t; + depth:int} + +let deepen seq={seq with depth=seq.depth-1} + +let record item seq={seq with history=History.add item seq.history} + +let lookup item seq= + History.mem item seq.history || + match item with + (_,None)->false + | (id,Some ((m,t) as c))-> + let p (id2,o)= + match o with + None -> false + | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in + History.exists p seq.history + +let rec add_formula side nam t seq gl= + match build_formula side nam t gl seq.cnt with + Left f-> + begin + match side with + Concl -> + {seq with + redexes=HP.add f seq.redexes; + gl=f.constr; + glatom=None} + | _ -> + {seq with + redexes=HP.add f seq.redexes; + context=cm_add f.constr nam seq.context} + end + | Right t-> + match side with + Concl -> + {seq with gl=t;glatom=Some t} + | _ -> + {seq with + context=cm_add t nam seq.context; + latoms=t::seq.latoms} + +let re_add_formula_list lf seq= + let do_one f cm= + if f.id == dummy_id then cm + else cm_add f.constr f.id cm in + {seq with + redexes=List.fold_right HP.add lf seq.redexes; + context=List.fold_right do_one lf seq.context} + +let find_left t seq=List.hd (CM.find t seq.context) + +(*let rev_left seq= + try + let lpat=(HP.maximum seq.redexes).pat in + left_reversible lpat + with Heap.EmptyHeap -> false +*) +let no_formula seq= + seq.redexes=HP.empty + +let rec take_formula seq= + let hd=HP.maximum seq.redexes + and hp=HP.remove seq.redexes in + if hd.id == dummy_id then + let nseq={seq with redexes=hp} in + if seq.gl==hd.constr then + hd,nseq + else + take_formula nseq (* discarding deprecated goal *) + else + hd,{seq with + redexes=hp; + context=cm_remove hd.constr hd.id seq.context} + +let empty_seq depth= + {redexes=HP.empty; + context=CM.empty; + latoms=[]; + gl=(mkMeta 1); + glatom=None; + cnt=newcnt (); + history=History.empty; + depth=depth} + +let create_with_ref_list l depth gl= + let f gr seq= + let c=constr_of_global gr in + let typ=(pf_type_of gl c) in + add_formula Hyp gr typ seq gl in + List.fold_right f l (empty_seq depth) + +open Auto + +let create_with_auto_hints l depth gl= + let seqref=ref (empty_seq depth) in + let f p_a_t = + match p_a_t.code with + Res_pf (c,_) | Give_exact c + | Res_pf_THEN_trivial_fail (c,_) -> + (try + let gr=global_of_constr c in + let typ=(pf_type_of gl c) in + seqref:=add_formula Hint gr typ !seqref gl + with Not_found->()) + | _-> () in + let g _ l=List.iter f l in + let h dbname= + let hdb= + try + searchtable_map dbname + with Not_found-> + error ("Firstorder: "^dbname^" : No such Hint database") in + Hint_db.iter g (snd hdb) in + List.iter h l; + !seqref + +let print_cmap map= + let print_entry c l s= + let xc=Constrextern.extern_constr false (Global.env ()) c in + str "| " ++ + Util.prlist Printer.pr_global l ++ + str " : " ++ + Ppconstr.pr_constr_expr xc ++ + cut () ++ + s in + msgnl (v 0 + (str "-----" ++ + cut () ++ + CM.fold print_entry map (mt ()) ++ + str "-----")) + + diff --git a/contrib/firstorder/sequent.mli b/contrib/firstorder/sequent.mli new file mode 100644 index 00000000..47fb74c7 --- /dev/null +++ b/contrib/firstorder/sequent.mli @@ -0,0 +1,66 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* global_reference -> global_reference list CM.t -> + global_reference list CM.t + +val cm_remove : constr -> global_reference -> global_reference list CM.t -> + global_reference list CM.t + +module HP: Heap.S with type elt=Formula.t + +type t = {redexes:HP.t; + context: global_reference list CM.t; + latoms:constr list; + gl:types; + glatom:constr option; + cnt:counter; + history:History.t; + depth:int} + +val deepen: t -> t + +val record: h_item -> t -> t + +val lookup: h_item -> t -> bool + +val add_formula : side -> global_reference -> constr -> t -> + Proof_type.goal sigma -> t + +val re_add_formula_list : Formula.t list -> t -> t + +val find_left : constr -> t -> global_reference + +val take_formula : t -> Formula.t * t + +val empty_seq : int -> t + +val create_with_ref_list : global_reference list -> + int -> Proof_type.goal sigma -> t + +val create_with_auto_hints : Auto.hint_db_name list -> + int -> Proof_type.goal sigma -> t + +val print_cmap: global_reference list CM.t -> unit diff --git a/contrib/firstorder/unify.ml b/contrib/firstorder/unify.ml new file mode 100644 index 00000000..1dd13cbe --- /dev/null +++ b/contrib/firstorder/unify.ml @@ -0,0 +1,143 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (n,subst_meta [i,t] tn)) !sigma) in + let rec head_reduce t= + (* forbids non-sigma-normal meta in head position*) + match kind_of_term t with + Meta i-> + (try + head_reduce (List.assoc i !sigma) + with Not_found->t) + | _->t in + Queue.add (t1,t2) bige; + try while true do + let t1,t2=Queue.take bige in + let nt1=head_reduce (whd_betaiotazeta t1) + and nt2=head_reduce (whd_betaiotazeta t2) in + match (kind_of_term nt1),(kind_of_term nt2) with + Meta i,Meta j-> + if i<>j then + if i + let t=subst_meta !sigma nt2 in + if Intset.is_empty (free_rels t) && + not (occur_term (mkMeta i) t) then + bind i t else raise (UFAIL(nt1,nt2)) + | _,Meta i -> + let t=subst_meta !sigma nt1 in + if Intset.is_empty (free_rels t) && + not (occur_term (mkMeta i) t) then + bind i t else raise (UFAIL(nt1,nt2)) + | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige + | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige + | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> + Queue.add (a,c) bige;Queue.add (pop b,pop d) bige + | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> + Queue.add (pa,pb) bige; + Queue.add (ca,cb) bige; + let l=Array.length va in + if l<>(Array.length vb) then + raise (UFAIL (nt1,nt2)) + else + for i=0 to l-1 do + Queue.add (va.(i),vb.(i)) bige + done + | App(ha,va),App(hb,vb)-> + Queue.add (ha,hb) bige; + let l=Array.length va in + if l<>(Array.length vb) then + raise (UFAIL (nt1,nt2)) + else + for i=0 to l-1 do + Queue.add (va.(i),vb.(i)) bige + done + | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2)) + done; + assert false + (* this place is unreachable but needed for the sake of typing *) + with Queue.Empty-> !sigma + +let value i t= + let add x y= + if x<0 then y else if y<0 then x else x+y in + let tref=mkMeta i in + let rec vaux term= + if term=tref then 0 else + let f v t=add v (vaux t) in + let vr=fold_constr f (-1) term in + if vr<0 then -1 else vr+1 in + vaux t + +type instance= + Real of (int*constr)*int + | Phantom of constr + +let mk_rel_inst t= + let new_rel=ref 1 in + let rel_env=ref [] in + let rec renum_rec d t= + match kind_of_term t with + Meta n-> + (try + mkRel (d+(List.assoc n !rel_env)) + with Not_found-> + let m= !new_rel in + incr new_rel; + rel_env:=(n,m) :: !rel_env; + mkRel (m+d)) + | _ -> map_constr_with_binders succ renum_rec d t + in + let nt=renum_rec 0 t in (!new_rel - 1,nt) + +let unif_atoms i dom t1 t2= + try + let t=List.assoc i (unif t1 t2) in + if isMeta t then Some (Phantom dom) + else Some (Real(mk_rel_inst t,value i t1)) + with + UFAIL(_,_) ->None + | Not_found ->Some (Phantom dom) + +let renum_metas_from k n t= (* requires n = max (free_rels t) *) + let l=list_tabulate (fun i->mkMeta (k+i)) n in + substl l t + +let more_general (m1,t1) (m2,t2)= + let mt1=renum_metas_from 0 m1 t1 + and mt2=renum_metas_from m1 m2 t2 in + try + let sigma=unif mt1 mt2 in + let p (n,t)= nfalse diff --git a/contrib/firstorder/unify.mli b/contrib/firstorder/unify.mli new file mode 100644 index 00000000..9fbe3dda --- /dev/null +++ b/contrib/firstorder/unify.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constr -> (int*constr) list + +type instance= + Real of (int*constr)*int (* nb trous*terme*valeur heuristique *) + | Phantom of constr (* domaine de quantification *) + +val unif_atoms : metavariable -> constr -> constr -> constr -> instance option + +val more_general : (int*constr) -> (int*constr) -> bool -- cgit v1.2.3