diff options
| -rw-r--r-- | .depend | 28 | ||||
| -rw-r--r-- | contrib/cc/CC.v | 9 | ||||
| -rw-r--r-- | contrib/first-order/engine.ml4 | 92 | ||||
| -rw-r--r-- | contrib/first-order/formula.ml | 148 | ||||
| -rw-r--r-- | contrib/first-order/formula.mli | 10 | ||||
| -rw-r--r-- | contrib/first-order/rules.ml | 6 | ||||
| -rw-r--r-- | contrib/first-order/sequent.ml | 2 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 16 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 3 |
9 files changed, 152 insertions, 162 deletions
@@ -2767,21 +2767,21 @@ contrib/field/field.cmx: toplevel/cerrors.cmx interp/constrintern.cmx \ interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx contrib/first-order/engine.cmo: tactics/auto.cmi toplevel/cerrors.cmi \ - parsing/egrammar.cmi parsing/extend.cmi contrib/first-order/formula.cmi \ - interp/genarg.cmi library/libnames.cmi parsing/pcoq.cmi lib/pp.cmi \ - parsing/pptactic.cmi proofs/proof_trees.cmi proofs/refiner.cmi \ - contrib/first-order/rules.cmi contrib/first-order/sequent.cmi \ - proofs/tacexpr.cmo tactics/tacinterp.cmi proofs/tacmach.cmi \ - proofs/tactic_debug.cmi tactics/tacticals.cmi tactics/tactics.cmi \ - kernel/term.cmi contrib/first-order/unify.cmi lib/util.cmi + parsing/egrammar.cmi contrib/first-order/formula.cmi interp/genarg.cmi \ + library/libnames.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \ + proofs/proof_trees.cmi proofs/refiner.cmi contrib/first-order/rules.cmi \ + contrib/first-order/sequent.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \ + proofs/tacmach.cmi proofs/tactic_debug.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi contrib/first-order/unify.cmi \ + lib/util.cmi contrib/first-order/engine.cmx: tactics/auto.cmx toplevel/cerrors.cmx \ - parsing/egrammar.cmx parsing/extend.cmx contrib/first-order/formula.cmx \ - interp/genarg.cmx library/libnames.cmx parsing/pcoq.cmx lib/pp.cmx \ - parsing/pptactic.cmx proofs/proof_trees.cmx proofs/refiner.cmx \ - contrib/first-order/rules.cmx contrib/first-order/sequent.cmx \ - proofs/tacexpr.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \ - proofs/tactic_debug.cmx tactics/tacticals.cmx tactics/tactics.cmx \ - kernel/term.cmx contrib/first-order/unify.cmx lib/util.cmx + parsing/egrammar.cmx contrib/first-order/formula.cmx interp/genarg.cmx \ + library/libnames.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \ + proofs/proof_trees.cmx proofs/refiner.cmx contrib/first-order/rules.cmx \ + contrib/first-order/sequent.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \ + proofs/tacmach.cmx proofs/tactic_debug.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx contrib/first-order/unify.cmx \ + lib/util.cmx contrib/first-order/formula.cmo: interp/coqlib.cmi kernel/declarations.cmi \ library/global.cmi tactics/hipattern.cmi pretyping/inductiveops.cmi \ library/libnames.cmi kernel/names.cmi pretyping/reductionops.cmi \ diff --git a/contrib/cc/CC.v b/contrib/cc/CC.v index 7bd349787..da7292084 100644 --- a/contrib/cc/CC.v +++ b/contrib/cc/CC.v @@ -28,9 +28,10 @@ Intros A B H E;Rewrite E;Assumption. Save. Tactic Definition CCsolve := - Match Context With + Repeat (Match Context With [ H: ?1 |- ?2] -> - (Assert (?2==?1);[CC| - Match Reverse Context With - [ H: ?1;Heq: (?2==?1)|- ?2] ->(Rewrite Heq;Exact H)]). + (Assert Heq____:(?2==?1);[CC|(Rewrite Heq____;Exact H)]) + |[ H: ?1; G: ?2 -> ?3 |- ?] -> + (Assert Heq____:(?2==?1) ;[CC| + (Rewrite Heq____ in G;Generalize (G H);Clear G;Intro G)])). diff --git a/contrib/first-order/engine.ml4 b/contrib/first-order/engine.ml4 index 612ac309b..45c95a469 100644 --- a/contrib/first-order/engine.ml4 +++ b/contrib/first-order/engine.ml4 @@ -47,29 +47,32 @@ let ground_tac solver startseq gl= if not (is_empty_left seq) && rev_left seq then left_tac seq [] else - right_tac seq pat l []) gl - and right_tac seq pat atoms ctx gl= + right_tac seq []) gl + and right_tac seq ctx gl= let re_add s=re_add_left_list ctx s in - match pat with - Ror-> - tclORELSE - (or_tac toptac (re_add seq)) - (left_tac seq ctx) gl - | Rexists(i,dom)-> - let cont_tac=left_tac seq ctx in - if seq.depth<=0 || not !qflag then - cont_tac gl - else - (match Unify.give_right_instances i dom atoms seq with - Some l -> tclORELSE - (exists_tac l toptac (re_add seq)) cont_tac gl - | None -> - tclORELSE cont_tac - (dummy_exists_tac dom toptac (re_add seq)) gl) - | _-> anomaly "unreachable place" + match seq.gl with + Complex (pat,_,atoms)-> + (match pat with + Ror-> + tclORELSE + (or_tac toptac (re_add seq)) + (left_tac seq ctx) gl + | Rexists(i,dom)-> + let cont_tac=left_tac seq ctx in + if seq.depth<=0 || not !qflag then + cont_tac gl + else + (match Unify.give_right_instances i dom atoms seq with + Some l -> tclORELSE + (exists_tac l toptac (re_add seq)) cont_tac gl + | None -> + tclORELSE cont_tac + (dummy_exists_tac dom toptac (re_add seq)) gl) + | _-> anomaly "unreachable place") + | Atomic _ -> left_tac seq ctx gl and left_tac seq ctx gl= if is_empty_left seq then - solver gl (* put solver here *) + solver gl else let (hd,seq1)=take_left seq in let re_add s=re_add_left_list ctx s in @@ -99,11 +102,7 @@ let ground_tac solver startseq gl= (ll_atom_tac typ hd.id toptac (re_add seq1)) (match lap with LLatom-> - (match seq1.gl with - Atomic t-> - (left_tac seq1 (hd::ctx)) - | Complex (pat,_,atoms)-> - (right_tac seq1 pat atoms (hd::ctx))) + right_tac seq1 (hd::ctx) | LLfalse-> ll_false_tac hd.id toptac (re_add seq1) | LLand (ind,largs) | LLor(ind,largs) -> @@ -115,9 +114,9 @@ let ground_tac solver startseq gl= else ll_forall_tac p hd.id toptac (re_add seq1)) (left_tac seq1 (hd::ctx)) - | LLexists (ind,a,p,_) -> + | LLexists (ind,l) -> if !qflag then - ll_ind_tac ind [a;p] hd.id toptac (re_add seq1) + ll_ind_tac ind l hd.id toptac (re_add seq1) else left_tac seq1 (hd::ctx) | LLarrow (a,b,c) -> @@ -155,39 +154,28 @@ open Genarg open Pcoq open Pp -type depth=int option - -let pr_depth _ _=function - None->mt () - | Some i -> str " depth " ++ int i - -ARGUMENT EXTEND depth TYPED AS depth PRINTED BY pr_depth -[ "depth" integer(i)]-> [ Some i] -| [ ] -> [None] -END - -type with_reflist = global_reference list - -let pr_ref_list _ _=function - [] -> mt () - | l -> prlist pr_reference l - TACTIC EXTEND Ground - [ "Ground" tactic(t) "with" ne_reference_list(l) ] -> - [ gen_ground_tac true (Some (snd t)) None l ] -| [ "Ground" tactic(t) "depth" integer(i) "with" ne_reference_list(l) ] -> - [ gen_ground_tac true (Some (snd t)) (Some i) l ] + [ "Ground" tactic(t) "depth" integer(i) "with" ne_reference_list(l) ] -> + [ gen_ground_tac true (Some (snd t)) (Some i) l ] | [ "Ground" tactic(t) "depth" integer(i) ] -> - [ gen_ground_tac true (Some (snd t)) (Some i) [] ] + [ gen_ground_tac true (Some (snd t)) (Some i) [] ] +| [ "Ground" tactic(t) "with" ne_reference_list(l) ] -> + [ gen_ground_tac true (Some (snd t)) None l ] | [ "Ground" tactic(t) ] -> - [ gen_ground_tac true (Some (snd t)) None [] ] + [ gen_ground_tac true (Some (snd t)) None [] ] +| [ "Ground" "depth" integer(i) "with" ne_reference_list(l) ] -> + [ gen_ground_tac true None (Some i) l ] +| [ "Ground" "depth" integer(i) ] -> + [ gen_ground_tac true None (Some i) [] ] +| [ "Ground" "with" ne_reference_list(l) ] -> + [ gen_ground_tac true None None l ] | [ "Ground" ] -> - [ gen_ground_tac true None None [] ] + [ gen_ground_tac true None None [] ] END TACTIC EXTEND GTauto [ "GTauto" ] -> - [ gen_ground_tac false (Some fail_solver) (Some 0) [] ] + [ gen_ground_tac false (Some fail_solver) None [] ] END TACTIC EXTEND GIntuition diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml index 810603e45..e00f26f3d 100644 --- a/contrib/first-order/formula.ml +++ b/contrib/first-order/formula.ml @@ -28,13 +28,13 @@ let (==?) fg h i1 i2 j1 j2 k1 k2= let c=fg i1 i2 j1 j2 in if c=0 then h k1 k2 else c -type ('a,'b)sum=Left of 'a|Right of 'b +type ('a,'b) sum = Left of 'a | Right of 'b type kind_of_formula= Arrow of constr*constr |And of inductive*constr list |Or of inductive*constr list - |Exists of inductive*constr*constr*constr + |Exists of inductive*constr list |Forall of constr*constr |Atom of constr |Evaluable of evaluable_global_reference*constr @@ -42,34 +42,13 @@ type kind_of_formula= type counter = bool -> metavariable -let constant path str ()=Coqlib.gen_constant "User" ["Init";path] str +let constant path str () = Coqlib.gen_constant "User" ["Init";path] str -let op2bool=function Some _->true |None->false +let op2bool = function Some _->true | None->false -let id_ex=constant "Logic" "ex" -let id_sig=constant "Specif" "sig" -let id_sigT=constant "Specif" "sigT" -let id_sigS=constant "Specif" "sigS" let id_not=constant "Logic" "not" let id_iff=constant "Logic" "iff" -let is_ex t = - t=(id_ex ()) || - t=(id_sig ()) || - t=(id_sigT ()) || - t=(id_sigS ()) - -let match_with_exist_term t= - match kind_of_term t with - App(t,v)-> - if t=id_ex () && (Array.length v)=2 then - let p=v.(1) in - match kind_of_term p with - Lambda(na,a,b)->Some(t,a,b,p) - | _ ->Some(t,v.(0),mkApp(p,[|mkRel 1|]),p) - else None - | _->None - let match_with_evaluable t= match kind_of_term t with App (hd,b)-> @@ -91,51 +70,49 @@ let nhyps mip = Array.map hyp constr_types let construct_nhyps ind= nhyps (snd (Global.lookup_inductive ind)) - -exception Dependent_Inductive -(* builds the array of arrays of constructor hyps for (ind Vargs)*) -let ind_hyps ind largs= +(* builds the array of arrays of constructor hyps for (ind largs)*) + +let ind_hyps nevar ind largs= let (mib,mip) = Global.lookup_inductive ind in let n = mip.mind_nparams in - if n<>(List.length largs) then - raise Dependent_Inductive - else - let p=nhyps mip in - let lp=Array.length p in - let types= mip.mind_nf_lc in - let myhyps i= - let t1=Term.prod_applist types.(i) largs in - fst (Sign.decompose_prod_n_assum p.(i) t1) in - Array.init lp myhyps - -let kind_of_formula cciterm = - 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_exist_term cciterm with - Some (i,a,b,p)-> Exists((destInd i),a,b,p) - |_-> - match match_with_nodep_ind cciterm with - Some (i,l)-> - let ind=destInd i in - let (mib,mip) = Global.lookup_inductive ind in - if Inductiveops.mis_is_recursive (ind,mib,mip) then - Atom cciterm - else - (match Array.length mip.mind_consnames with - 0->False - | 1->And(ind,l) - | _->Or(ind,l)) - | None -> - match match_with_evaluable cciterm with - Some (cst,t)->Evaluable ((EvalConstRef cst),t) - | None ->Atom cciterm - - +(* assert (n=(List.length largs));*) + let lp=Array.length mip.mind_consnames in + let types= mip.mind_nf_lc 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 kind_of_formula term = + let cciterm=whd_betaiotazeta 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)-> + let ind=destInd i in + let (mib,mip) = Global.lookup_inductive ind in + if Inductiveops.mis_is_recursive (ind,mib,mip) then + Atom cciterm + else + (match Array.length mip.mind_consnames with + 0->False + | 1->And(ind,l) + | _->Or(ind,l)) + | _ -> + match match_with_sigma_type cciterm with + Some (i,l)-> Exists((destInd i),l) + |_-> + match match_with_evaluable cciterm with + Some (cst,t)->Evaluable ((EvalConstRef cst),t) + | None ->Atom cciterm + let build_atoms gl metagen= let rec build_rec env polarity cciterm = match kind_of_formula cciterm with @@ -144,18 +121,21 @@ let build_atoms gl metagen= (build_rec env (not polarity) a)@ (build_rec env polarity b) | And(i,l) | Or(i,l)-> - (try - let v = ind_hyps i l in - let g i accu (_,_,t) = - (build_rec env polarity (lift i t))@accu in - let f l accu = - list_fold_left_i g (1-(List.length l)) accu l in - Array.fold_right f v [] - with Dependent_Inductive -> - [polarity,(substnl env 0 cciterm)]) - | Forall(_,b)|Exists(_,_,b,_)-> + let v = ind_hyps 0 i l in + let g i accu (_,_,t) = + (build_rec env polarity (lift i t))@accu in + let f l accu = + list_fold_left_i g (1-(List.length l)) accu l in + Array.fold_right f v [] + | Exists(i,l)-> + let var=mkMeta (metagen true) in + let v =(ind_hyps 1 i l).(0) in + let g i accu (_,_,t) = + (build_rec (var::env) polarity (lift i t))@accu 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 + build_rec (var::env) polarity b | Atom t-> [polarity,(substnl env 0 cciterm)] | Evaluable(ec,t)-> @@ -181,7 +161,7 @@ type left_arrow_pattern= | LLand of inductive*constr list | LLor of inductive*constr list | LLforall of constr - | LLexists of inductive*constr*constr*constr + | LLexists of inductive*constr list | LLarrow of constr*constr*constr | LLevaluable of evaluable_global_reference @@ -212,7 +192,7 @@ let build_left_entry nam typ internal gl metagen= | Atom a -> raise (Is_atom a) | And(i,_) -> Land i | Or(i,_) -> Lor i - | Exists (_,_,_,_) -> Lexists + | Exists (_,_) -> Lexists | Forall (d,_) -> let m=meta_succ(metagen false) in Lforall(m,d) | Evaluable (egc,_) ->Levaluable egc | Arrow (a,b) ->LA (a, @@ -222,7 +202,7 @@ let build_left_entry nam typ internal gl metagen= | And(i,l)-> LLand(i,l) | Or(i,l)-> LLor(i,l) | Arrow(a,c)-> LLarrow(a,c,b) - | Exists(i,a,_,p)->LLexists(i,a,p,b) + | Exists(i,l)->LLexists(i,l) | Forall(_,_)->LLforall a | Evaluable (egc,_)-> LLevaluable egc) in let l= @@ -244,8 +224,10 @@ let build_right_entry typ gl metagen= | Atom a -> raise (Is_atom a) | And(_,_) -> Rand | Or(_,_) -> Ror - | Exists (_,d,_,_) -> - let m=meta_succ(metagen false) in Rexists(m,d) + | Exists (i,l) -> + let m=meta_succ(metagen false) in + let (_,_,d)=list_last (ind_hyps 0 i l).(0) in + Rexists(m,d) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow | Evaluable (egc,_)->Revaluable egc in diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli index 89bd6d25f..3bcf1af0e 100644 --- a/contrib/first-order/formula.mli +++ b/contrib/first-order/formula.mli @@ -26,7 +26,7 @@ type kind_of_formula= Arrow of constr*constr |And of inductive*constr list |Or of inductive*constr list - |Exists of inductive*constr*constr*constr + |Exists of inductive*constr list |Forall of constr*constr |Atom of constr |Evaluable of Names.evaluable_global_reference * Term.constr @@ -36,9 +36,7 @@ type counter = bool -> metavariable val construct_nhyps : inductive -> int array -exception Dependent_Inductive - -val ind_hyps : inductive -> constr list -> Sign.rel_context array +val ind_hyps : int -> inductive -> constr list -> Sign.rel_context array val kind_of_formula : constr -> kind_of_formula @@ -63,7 +61,7 @@ type left_arrow_pattern= | LLand of inductive*constr list | LLor of inductive*constr list | LLforall of constr - | LLexists of inductive*constr*constr*constr + | LLexists of inductive*constr list | LLarrow of constr*constr*constr | LLevaluable of Names.evaluable_global_reference @@ -82,6 +80,8 @@ type left_formula={id:global_reference; atoms:(bool*constr) list; internal:bool} +exception Is_atom of constr + val build_left_entry : global_reference -> types -> bool -> Proof_type.goal Tacmach.sigma -> counter -> (left_formula,types) sum diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml index ebd820bcc..2ae0b5df4 100644 --- a/contrib/first-order/rules.ml +++ b/contrib/first-order/rules.ml @@ -205,7 +205,7 @@ let left_false_tac id= let ll_ind_tac ind largs id tacrec seq gl= (try - let rcs=ind_hyps ind largs in + let rcs=ind_hyps 0 ind largs in let vargs=Array.of_list largs in (* construire le terme H->B, le generaliser etc *) let myterm i= @@ -217,13 +217,13 @@ let ll_ind_tac ind largs id tacrec seq gl= 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.map myterm (interval 0 (lp-1)) in + let newhyps=list_tabulate myterm lp in tclTHENLIST [generalize newhyps; clear_global id; tclDO lp intro; wrap lp false tacrec seq] - with Dependent_Inductive | Invalid_argument _ ->tclFAIL 0 "") gl + with Invalid_argument _ ->tclFAIL 0 "") gl let ll_forall_tac prod id tacrec seq= tclTHENS (cut prod) diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index 1684716d1..690feb874 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -34,7 +34,7 @@ let priority = function (* pure heuristics, <=0 for non reversible *) | LLand (_,_) -> 80 | LLor (_,_) -> 70 | LLforall _ -> -20 - | LLexists (_,_,_,_) -> 50 + | LLexists (_,_) -> 50 | LLarrow (_,_,_) -> -10 | LLevaluable _ -> 100 diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index a9a8e432a..6c4a01f26 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -223,6 +223,22 @@ let match_with_nodep_ind t = let is_nodep_ind t=op2bool (match_with_nodep_ind t) +let match_with_sigma_type t= + let (hdapp,args) = decompose_app t in + match (kind_of_term hdapp) with + | Ind ind -> + let (mib,mip) = Global.lookup_inductive ind in + if (mip.mind_nrealargs=0) && + (Array.length mip.mind_consnames=1) && + has_nodep_prod_after (mip.mind_nparams+1) mip.mind_nf_lc.(0) then + (*allowing only 1 existential*) + Some (hdapp,args) + else + None + | _ -> None + +let is_sigma_type t=op2bool (match_with_sigma_type t) + (***** Destructing patterns bound to some theory *) let rec first_match matcher = function diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index cfe3f4027..3dd6a420f 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -91,6 +91,9 @@ val has_nodep_prod : testing_function val match_with_nodep_ind : (constr * constr list) matching_function val is_nodep_ind : testing_function +val match_with_sigma_type : (constr * constr list) matching_function +val is_sigma_type : testing_function + (***** Destructing patterns bound to some theory *) open Coqlib |