From dcef667a444aa0f189225855c1433d26b65fb8b7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 28 Apr 2009 13:59:26 +0000 Subject: [PATCH] huge commit in automation: - tactics: - all tactics used by auto (apply, applys and thus rewrite) do handle correctly the subst present in the status - indexing: - demodualte_all (and thus solve_rewriting) reimplemented, faster and more correct - auto: - applyS used to apply theorems, remaining goals have a depth penalty --- .../acic_procedural/proceduralConversion.ml | 5 +- .../binaries/transcript/.depend.opt | 5 + .../components/cic_unification/cicRefine.ml | 22 +- .../components/cic_unification/cicRefine.mli | 6 + .../grafite_engine/grafiteEngine.ml | 4 +- .../components/grafite_engine/grafiteSync.ml | 30 +- .../grafite_parser/grafiteParser.ml | 1 - .../components/syntax_extensions/.depend | 3 + helm/software/components/tactics/auto.ml | 1000 ++++++++++------- helm/software/components/tactics/auto.mli | 5 - helm/software/components/tactics/autoCache.ml | 3 + .../software/components/tactics/autoCache.mli | 1 + .../components/tactics/declarative.ml | 7 +- .../components/tactics/equalityTactics.ml | 70 +- .../tactics/paramodulation/equality.ml | 4 +- .../tactics/paramodulation/indexing.ml | 191 ++-- .../tactics/paramodulation/indexing.mli | 6 +- .../tactics/paramodulation/saturation.ml | 5 +- .../components/tactics/primitiveTactics.ml | 87 +- .../components/tactics/primitiveTactics.mli | 10 +- .../components/tactics/proofEngineHelpers.ml | 33 +- .../components/tactics/proofEngineHelpers.mli | 1 + .../components/tactics/reductionTactics.ml | 23 +- helm/software/components/tactics/tacticals.ml | 8 +- helm/software/components/tactics/tactics.ml | 1 - helm/software/components/tactics/tactics.mli | 5 +- .../components/tactics/variousTactics.ml | 2 +- .../matita/contribs/POPLmark/Fsub/defn.ma | 3 +- .../POPLmark/Fsub/part1a_inversion.ma | 3 +- .../matita/contribs/POPLmark/Fsub/util.ma | 5 +- .../matita/library/Q/fraction/ftimes.ma | 9 +- helm/software/matita/library/R/r.ma | 61 +- helm/software/matita/library/R/root.ma | 22 +- .../software/matita/library/algebra/groups.ma | 2 +- .../matita/library/decidable_kit/decidable.ma | 4 +- helm/software/matita/library/demo/cantor.ma | 2 +- .../matita/library/demo/formal_topology.ma | 2 +- .../matita/library/demo/power_derivative.ma | 1 + .../matita/library/logic/coimplication.ma | 2 +- .../matita/library/logic/connectives2.ma | 2 +- .../matita/library/nat/div_and_mod.ma | 2 +- .../matita/library/nat/factorization.ma | 26 +- helm/software/matita/library/nat/gcd.ma | 16 +- .../matita/library/nat/generic_iter_p.ma | 10 +- .../software/matita/library/nat/map_iter_p.ma | 8 +- helm/software/matita/library/nat/minus.ma | 16 +- helm/software/matita/library/nat/times.ma | 7 +- 47 files changed, 1009 insertions(+), 732 deletions(-) diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index 97e32b94a..67b293393 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -244,8 +244,9 @@ let elim_inferred_type context goal arg using cpattern = let metasenv, ugraph = [], Un.default_ugraph in let ety = H.get_type "elim_inferred_type" context using in let _splits, args_no = PEH.split_with_whd (context, ety) in - let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim - ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no + let _metasenv, _subst, predicate, _arg, actual_args = + PT.mk_predicate_for_elim + ~context ~metasenv ~subst:[] ~ugraph ~goal ~arg ~using ~cpattern ~args_no in let ty = C.Appl (predicate :: actual_args) in let upto = List.length actual_args in diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index efadc681e..f17459162 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmx grafiteParser.cmi: types.cmx grafite.cmi: types.cmx +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmx gallina8Parser.cmi diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 40eaa1ba6..b535b9ebe 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -337,8 +337,8 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | _ -> raise (AssertFailure (lazy "Wrong number of arguments"))) | _ -> raise (AssertFailure (lazy "Prod or MutInd expected")) -and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t - ugraph +and type_of_aux' ?(clean_dummy_dependent_types=true) + ?(localization_tbl = Cic.CicHash.create 1) metasenv subst context t ugraph = let rec type_of_aux subst metasenv context t ugraph = let module C = Cic in @@ -1828,7 +1828,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci (* eat prods ends here! *) let t',ty,subst',metasenv',ugraph1 = - type_of_aux [] metasenv context t ugraph + type_of_aux subst metasenv context t ugraph in let substituted_t = CicMetaSubst.apply_subst subst' t' in let substituted_ty = CicMetaSubst.apply_subst subst' ty in @@ -1872,7 +1872,21 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci else substituted_metasenv in - (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) + (cleaned_t,cleaned_ty,cleaned_metasenv,subst',ugraph1) +;; + +let type_of metasenv subst context t ug = + type_of_aux' metasenv subst context t ug +;; + +let type_of_aux' + ?clean_dummy_dependent_types ?localization_tbl metasenv context t ug += + let t,ty,m,s,ug = + type_of_aux' ?clean_dummy_dependent_types ?localization_tbl + metasenv [] context t ug + in + t,ty,m,ug ;; let undebrujin uri typesno tys t = diff --git a/helm/software/components/cic_unification/cicRefine.mli b/helm/software/components/cic_unification/cicRefine.mli index d17b1ac85..666099dce 100644 --- a/helm/software/components/cic_unification/cicRefine.mli +++ b/helm/software/components/cic_unification/cicRefine.mli @@ -35,6 +35,12 @@ val type_of_aux': Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph -> Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph + (* this is the correct one and should be used by tactics to fold subst *) +val type_of: + Cic.metasenv -> Cic.substitution -> + Cic.context -> Cic.term -> CicUniv.universe_graph -> + Cic.term * Cic.term * Cic.metasenv * Cic.substitution *CicUniv.universe_graph + (* typecheck metasenv uri obj graph *) (* refines [obj] and returns the refined form of [obj], *) (* the new metasenv and universe graph. *) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 5caafb67b..97af8a06f 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -336,14 +336,14 @@ let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) = let after = ProofEngineTypes.goals_of_proof proof in let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in let proof, opened_goals = - let uri, metasenv_after_tactic, _subst, t, ty, attrs = proof in + let uri, metasenv_after_tactic, subst, t, ty, attrs = proof in let reordered_metasenv, opened_goals = reorder_metasenv starting_metasenv metasenv_after_refinement metasenv_after_tactic opened goal always_opens_a_goal in - let proof' = uri, reordered_metasenv, _subst, t, ty, attrs in + let proof' = uri, reordered_metasenv, [], t, ty, attrs in proof', opened_goals in let incomplete_proof = diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index 759186c12..49545e5f4 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -78,10 +78,30 @@ let add_obj ~pack_coercion_obj uri obj status = let term = CicUtil.term_of_uri uri in let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in let tkeys = Universe.keys [] ty in - let index_cmd = - List.map - (fun key -> GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri)) - tkeys + let universe = automation_cache.AutomationCache.univ in + let universe, index_cmd = + List.fold_left + (fun (universe,acc) key -> + let cands = Universe.get_candidates universe key in + let tys = + List.map + (fun t -> + let ty, _ = + CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph + in + ty) + cands + in + if List.for_all + (fun cty -> + not (fst(CicReduction.are_convertible [] ty cty + CicUniv.oblivion_ugraph))) tys + then + Universe.index universe key term, + GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri)::acc + else + universe, acc) + (universe,[]) tkeys in let is_equational = is_equational_fact ty in let select_cmd = @@ -90,8 +110,6 @@ let add_obj ~pack_coercion_obj uri obj status = else [] in - let universe = automation_cache.AutomationCache.univ in - let universe = Universe.index_term_and_unfolded_term universe [] term ty in let automation_cache = if is_equational then AutomationCache.add_term_to_active automation_cache [] [] [] term None diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 324231b50..216b88b05 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -436,7 +436,6 @@ EXTEND | IDENT "timeout" | IDENT "library" | IDENT "type" - | IDENT "steps" | IDENT "all" ] ]; diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index f3c6a8bd1..25e67131f 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,2 +1,5 @@ +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index ce4b9357e..06844a209 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -366,8 +366,19 @@ let init_cache_and_tables ?dbd ~use_library ~use_context automation_cache restricted_univ (proof, goal) = - let _, metasenv, _, _, _, _ = proof in + let _, metasenv, subst, _, _, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in + let is_prop m s c t = + let ty,_ = + CicTypeChecker.type_of_aux' m ~subst:s c t CicUniv.oblivion_ugraph + in + let sort,_ = + CicTypeChecker.type_of_aux' m ~subst:s c ty CicUniv.oblivion_ugraph + in + match CicReduction.whd ~subst c sort with + | Cic.Sort Cic.Prop | Cic.Sort (Cic.CProp _) -> true + | _ -> false + in if restricted_univ = [] then let ct = if use_context then find_context_theorems context metasenv else [] @@ -379,22 +390,28 @@ let init_cache_and_tables in let cache = AutoCache.cache_empty in let cache = cache_add_list cache context (ct@lt) in - let tables = - let env = metasenv, context, CicUniv.oblivion_ugraph in - List.fold_left - (fun (a,p,b) (t,ty) -> - let mes = CicUtil.metas_of_term ty in - Saturation.add_to_active b a p env ty t - (List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv)) - automation_cache.AutomationCache.tables ct + let automation_cache, _ = + List.fold_left + (fun (c,maxmeta) (t,ty) -> + let head, metasenv, args, maxmeta = + TermUtil.saturate_term maxmeta metasenv context ty 0 + in + if List.exists (is_prop metasenv subst context) args then + c,maxmeta + else + let st = if args = [] then t else Cic.Appl (t::args) in + AutomationCache.add_term_to_active + c metasenv [] context st (Some head), maxmeta) + (automation_cache,CicMkImplicit.new_meta metasenv subst) ct in -(* AutomationCache.pp_cache { automation_cache with AutomationCache.tables = - * tables }; *) - automation_cache.AutomationCache.univ, tables, cache +(* AutomationCache.pp_cache automation_cache; *) + automation_cache.AutomationCache.univ, + automation_cache.AutomationCache.tables, + cache else let metasenv, t_ty, s_t_ty, _ = List.fold_left - (fun (metasenv,acc, sacc, maxmeta) t -> + (fun (metasenv as orig,acc, sacc, maxmeta) t -> let ty, _ = CicTypeChecker.type_of_aux' metasenv ~subst:[] context t CicUniv.oblivion_ugraph @@ -402,9 +419,12 @@ let init_cache_and_tables let head, metasenv, args, maxmeta = TermUtil.saturate_term maxmeta metasenv context ty 0 in - let st = if args = [] then t else Cic.Appl (t::args) in - metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta) - (metasenv, [],[], CicMkImplicit.new_meta metasenv []) restricted_univ + if List.exists (is_prop metasenv subst context) args then + orig, (t,ty)::acc, sacc, maxmeta + else + let st = if args = [] then t else Cic.Appl (t::args) in + metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta) + (metasenv, [],[], CicMkImplicit.new_meta metasenv subst) restricted_univ in let automation_cache = AutomationCache.empty () in let automation_cache = @@ -593,7 +613,7 @@ let close_more tables context status auto universe cache = (active,passive,bag), cache ;; -let find_context_equalities tables context proof (universe:Universe.universe) cache +let find_context_equalities dbd tables context proof (universe:Universe.universe) cache = let module C = Cic in let module S = CicSubstitution in @@ -717,92 +737,380 @@ let flags_of_params params ?(for_applyS=false) () = AutoTypes.skip_context = skip_context; } + +let eq_of_goal = function + | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri -> + uri + | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) +;; + +(* performs steps of rewrite with the universe, obtaining if possible + * a trivial goal *) +let solve_rewrite ~automation_cache ~params:(univ,params) (proof,goal)= + let steps = int_of_string (string params "steps" "4") in + let use_context = bool params "use_context" true in + let universe, tables, cache = + init_cache_and_tables ~use_library:false ~use_context + automation_cache univ (proof,goal) + in + let actives, passives, bag = tables in + let pa,metasenv,subst,pb,pc,pd = proof in + let _,context,ty = CicUtil.lookup_meta goal metasenv in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + let context = CicMetaSubst.apply_subst_context subst context in + let ty = CicMetaSubst.apply_subst subst ty in + let eq_uri = eq_of_goal ty in + let initgoal = [], metasenv, ty in + let table = + let equalities = (Saturation.list_of_passive passives) in + List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd actives) equalities + in + let env = metasenv,context,CicUniv.oblivion_ugraph in + debug_print (lazy ("demod to solve: " ^ CicPp.ppterm ty)); + match Indexing.solve_demodulating bag env table initgoal steps with + | Some (bag, gproof, metasenv, sub_subst, proof) -> + let subst_candidates,extra_infos = + List.split + (HExtlib.filter_map + (fun (i,c,_) -> + if i <> goal && c = context then Some (i,(c,ty)) else None) + metasenv) + in + let proofterm,proto_subst = + let proof = Equality.add_subst sub_subst proof in + Equality.build_goal_proof + bag eq_uri gproof proof ty subst_candidates context metasenv + in + let proofterm = Subst.apply_subst sub_subst proofterm in + let extrasubst = + HExtlib.filter_map + (fun (i,((c,ty),t)) -> + match t with + | Cic.Meta (j,_) when i=j -> None + | _ -> Some (i,(c,t,ty))) + (List.combine subst_candidates + (List.combine extra_infos proto_subst)) + in + let subst = subst @ extrasubst in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + let proofterm, _, metasenv,subst, _ = + CicRefine.type_of metasenv subst context proofterm + CicUniv.oblivion_ugraph + in + let status = (pa,metasenv,subst,pb,pc,pd), goal in + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:proofterm) status + | None -> + raise + (ProofEngineTypes.Fail (lazy + ("Unable to solve with " ^ string_of_int steps ^ " demodulations"))) +;; + +(* Demodulate thorem *) +let open_type ty bo = + let rec open_type_aux context ty k args = + match ty with + | Cic.Prod (n,s,t) -> + let n' = + FreshNamesGenerator.mk_fresh_name [] context n ~typ:s ~subst:[] in + let entry = match n' with + | Cic.Name _ -> Some (n',(Cic.Decl s)) + | Cic.Anonymous -> None + in + open_type_aux (entry::context) t (k+1) ((Cic.Rel k)::args) + | Cic.LetIn (n,s,sty,t) -> + let entry = Some (n,(Cic.Def (s,sty))) + in + open_type_aux (entry::context) t (k+1) args + | _ -> context, ty, args + in + let context, ty, args = open_type_aux [] ty 1 [] in + match args with + | [] -> context, ty, bo + | _ -> context, ty, Cic.Appl (bo::args) +;; + +let rec close_type bo ty context = + match context with + | [] -> assert_proof_is_valid bo [] [] ty; (bo,ty) + | Some (n,(Cic.Decl s))::tl -> + close_type (Cic.Lambda (n,s,bo)) (Cic.Prod (n,s,ty)) tl + | Some (n,(Cic.Def (s,sty)))::tl -> + close_type (Cic.LetIn (n,s,sty,bo)) (Cic.LetIn (n,s,sty,ty)) tl + | _ -> assert false +;; + +let is_subsumed univ context ty = + let candidates = Universe.get_candidates univ ty in + List.fold_left + (fun res cand -> + match res with + | Some found -> Some found + | None -> + try + let mk_irl = + CicMkImplicit.identity_relocation_list_for_metavariable in + let metasenv = [(0,context,ty)] in + let fake_proof = + None,metasenv,[] , (lazy (Cic.Meta(0,mk_irl context))),ty,[] + in + let (_,metasenv,subst,_,_,_), open_goals = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:cand) + (fake_proof,0) + in + let prop_goals, other = + split_goals_in_prop metasenv subst open_goals + in + if prop_goals = [] then Some cand else None + with + | ProofEngineTypes.Fail s -> None + | CicUnification.Uncertain s -> None + ) None candidates +;; + +let demodulate_theorem ~automation_cache uri = + let eq_uri = + match LibraryObjects.eq_URI () with + | Some (uri) -> uri + | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in + let obj,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in + let context,ty,bo = + match obj with + | Cic.Constant(n, _, ty ,_, _) -> open_type ty (Cic.Const(uri,[])) + | _ -> raise (ProofEngineTypes.Fail (lazy "not a theorem")) + in + if CicUtil.is_closed ty then + raise (ProofEngineTypes.Fail (lazy ("closed term: dangerous reduction"))); + let initgoal = [], [], ty in + (* compute the signature *) + let signature = + let ty_set = MetadataConstraints.constants_of ty in + let hyp_set = MetadataQuery.signature_of_hypothesis context [] in + let set = MetadataConstraints.UriManagerSet.union ty_set hyp_set in + MetadataQuery.close_with_types set [] context + in + (* retrieve equations from the universe universe *) + (* XXX automation_cache *) + let universe = automation_cache.AutomationCache.univ in + let equations = + retrieve_equations true signature universe AutoCache.cache_empty context [] + in + debug_print + (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations)))); + let eqs_and_types = + HExtlib.filter_map + (fun t -> + let ty,_ = + CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph + in + (* retrieve_equations could also return flexible terms *) + if is_an_equality ty then Some(t,ty) + else + try + let ty' = unfold context ty in + if is_an_equality ty' then Some(t,ty') else None + with ProofEngineTypes.Fail _ -> None) + equations + in + let bag = Equality.mk_equality_bag () in + + let bag, units, _, newmeta = + partition_unit_equalities context [] (CicMkImplicit.new_meta [] []) bag eqs_and_types + in + let table = + List.fold_left + (fun tbl eq -> Indexing.index tbl eq) + Indexing.empty units + in + let changed,(newproof,newmetasenv, newty) = + Indexing.demod bag + ([],context,CicUniv.oblivion_ugraph) table initgoal in + if changed then + begin + let oldproof = Equality.Exact bo in + let proofterm,_ = + Equality.build_goal_proof (~contextualize:false) (~forward:true) bag + eq_uri newproof oldproof ty [] context newmetasenv + in + if newmetasenv <> [] then + raise (ProofEngineTypes.Fail (lazy ("metasenv not empty"))) + else + begin + assert_proof_is_valid proofterm newmetasenv context newty; + match is_subsumed universe context newty with + | Some t -> raise + (ProofEngineTypes.Fail (lazy ("subsumed by " ^ CicPp.ppterm t))) + | None -> close_type proofterm newty context + end + end + else (* if newty = ty then *) + raise (ProofEngineTypes.Fail (lazy "no progress")) + (*else ProofEngineTypes.apply_tactic + (ReductionTactics.simpl_tac + ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*) +;; + + +(* NEW DEMODULATE *) +let demodulate ~dbd ~automation_cache ~params:(univ, params) (proof,goal)= + let universe, tables, cache = + init_cache_and_tables + ~dbd ~use_library:false ~use_context:true + automation_cache univ (proof,goal) + in + let eq_uri = + match LibraryObjects.eq_URI () with + | Some (uri) -> uri + | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in + let active, passive, bag = tables in + let curi,metasenv,subst,pbo,pty, attrs = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in + let initgoal = [], metasenv, ty in + let equalities = (Saturation.list_of_passive passive) in + (* we demodulate using both actives passives *) + let env = metasenv,context,CicUniv.empty_ugraph in + debug_print (lazy ("PASSIVES:" ^ string_of_int(List.length equalities))); + List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e))) + equalities; + let table = + List.fold_left + (fun tbl eq -> Indexing.index tbl eq) + (snd active) equalities + in + let changed,(newproof,newmetasenv, newty) = + (* Indexing.demodulation_goal bag *) + Indexing.demod bag + (metasenv,context,CicUniv.oblivion_ugraph) table initgoal + in + if changed then + begin + let maxm = CicMkImplicit.new_meta metasenv subst in + let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in + let subst_candidates = List.map (fun (i,_,_) -> i) metasenv in + let subst_candidates = List.filter (fun x-> x <> goal) subst_candidates in + let proofterm, proto_subst = + Equality.build_goal_proof (~contextualize:false) bag + eq_uri newproof opengoal ty subst_candidates context metasenv + in + (* XXX understan what to do with proto subst *) + let metasenv = (maxm,context,newty)::metasenv in + let proofterm, _, metasenv, subst, _ = + CicRefine.type_of metasenv subst context proofterm + CicUniv.oblivion_ugraph + in + let extended_status = (curi,metasenv,subst,pbo,pty, attrs),goal in + let proof,gl = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:proofterm) extended_status + in + proof,maxm::gl + end + else + raise (ProofEngineTypes.Fail (lazy "no progress")) +;; + +let demodulate_tac ~dbd ~params:(_,flags as params) ~automation_cache = + ProofEngineTypes.mk_tactic + (fun status -> + let all = bool flags "all" false in + if all then + solve_rewrite ~params ~automation_cache status + else + demodulate ~dbd ~params ~automation_cache status) +;; (***************** applyS *******************) let apply_smart_aux - dbd flags automation_cache univ proof goal newmeta' metasenv' - context term' ty termty goal_arity + dbd automation_cache params proof goal newmeta' metasenv' subst + context term' ty termty goal_arity = -(* let ppterm = ppterm context in *) - let (consthead,newmetasenv,arguments,_) = + let consthead,newmetasenv,arguments,_ = TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in let term'' = - match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) + match arguments with + | [] -> term' + | _ -> Cic.Appl (term'::arguments) in - let proof',oldmetasenv = - let (puri,metasenv,_subst,pbo,pty, attrs) = proof in - (puri,newmetasenv,_subst,pbo,pty, attrs),metasenv + let consthead = + let rec aux t = function + | [] -> + let t = CicReduction.normalize ~delta:false context t in + (match t, ty with + | Cic.Appl (hd1::_), Cic.Appl (hd2::_) when hd1 <> hd2 -> + let t = ProofEngineReduction.unfold context t in + (match t with + | Cic.Appl (hd1'::_) when hd1' = hd2 -> t + | _ -> raise (ProofEngineTypes.Fail (lazy "incompatible head"))) + | _ -> t) + | arg :: tl -> + match CicReduction.whd context t with + | Cic.Prod (_,_,tgt) -> + aux (CicSubstitution.subst arg tgt) tl + | _ -> assert false + in + aux termty arguments in let goal_for_paramod = match LibraryObjects.eq_URI () with | Some uri -> - Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty] + Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Implicit (Some `Type); consthead; ty] | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined")) in - let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in - let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in - let proof'' = - let uri,_,_subst,p,ty, attrs = proof' in - uri,metasenv_for_paramod,_subst,p,ty, attrs - in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - let proof''',goals = - ProofEngineTypes.apply_tactic - (EqualityTactics.rewrite_tac ~direction:`RightToLeft - ~pattern:(ProofEngineTypes.conclusion_pattern None) - (Cic.Meta(newmeta,irl)) []) - (proof'',goal) - in - let goal = match goals with [g] -> g | _ -> assert false in - let proof'''', _ = - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac term'') - (proof''',goal) - in - let universe, tables, cache = - init_cache_and_tables ~dbd ~use_library:flags.use_library - ~use_context:true automation_cache univ (proof'''',newmeta) - in - let active, passive, bag = tables in - match - Saturation.given_clause bag (proof'''',newmeta) active passive - 20 10 flags.timeout - with - | None, _,_,_ -> - raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) - | Some (_,proof''''',_), active,passive,bag -> - proof''''', - ProofEngineHelpers.compare_metasenvs ~oldmetasenv - ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive -(* - debug_print - (lazy - ("SUBSUMPTION SU: " ^ string_of_int newmeta ^ " " ^ ppterm goal_for_paramod)); - let res, maxmeta = - Saturation.all_subsumed bag maxm (proof'''',newmeta) active passive - in - if res = [] then - raise (ProofEngineTypes.Fail (lazy("BUM"))) - else let (_,proof''''',_) = List.hd res in - proof''''',ProofEngineHelpers.compare_metasenvs ~oldmetasenv - ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive + try + let goal_for_paramod, _, newmetasenv, subst, _ = + CicRefine.type_of newmetasenv subst context goal_for_paramod + CicUniv.oblivion_ugraph + in + let newmeta = CicMkImplicit.new_meta newmetasenv subst in + let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in + let proof'' = + let uri,_,_,p,ty, attrs = proof in + uri,metasenv_for_paramod,subst,p,ty, attrs + in + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in +(* + prerr_endline ("------ prima di rewrite su ------ " ^ string_of_int goal); + prerr_endline ("menv:\n"^CicMetaSubst.ppmetasenv [] metasenv_for_paramod); + prerr_endline ("subst:\n"^CicMetaSubst.ppsubst + ~metasenv:(metasenv_for_paramod) + subst); *) -;; -let rec count_prods context ty = - match CicReduction.whd context ty with - Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t - | _ -> 0 + let (proof''',goals) = + ProofEngineTypes.apply_tactic + (EqualityTactics.rewrite_tac ~direction:`RightToLeft + ~pattern:(ProofEngineTypes.conclusion_pattern None) + (Cic.Meta(newmeta,irl)) []) (proof'',goal) + in + let goal = match goals with [g] -> g | _ -> assert false in + let proof'''', _ = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac term'') + (proof''',goal) + in + let (_,m,_,_,_,_ as p),_ = + solve_rewrite ~params ~automation_cache (proof'''',newmeta) + in + let open_goals = + ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv' ~newmetasenv:m + in + p, open_goals + with + CicRefine.RefineFailure msg -> + raise (ProofEngineTypes.Fail msg) +;; let apply_smart - ~dbd ~term ~subst ~automation_cache ~params:(univ,params) (proof, goal) + ~dbd ~term ~automation_cache ~params (proof, goal) = let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in - let (_,metasenv,_subst,_,_, _) = proof in + let (_,metasenv,subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let flags = flags_of_params params ~for_applyS:true () in let newmeta = CicMkImplicit.new_meta metasenv subst in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with @@ -838,26 +1146,37 @@ let apply_smart in let metasenv' = metasenv@newmetasenvfragment in let termty,_ = - CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph + CicTypeChecker.type_of_aux' + metasenv' ~subst context term' CicUniv.oblivion_ugraph in let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in - let goal_arity = count_prods context ty in - let proof, gl, active, passive = - apply_smart_aux dbd flags automation_cache univ proof goal - newmeta' metasenv' context term' ty termty goal_arity + let goal_arity = + let rec count_prods context ty = + match CicReduction.whd ~subst context ty with + | Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t + | _ -> 0 + in + count_prods context ty in - proof, gl, active, passive + apply_smart_aux dbd automation_cache params proof goal + newmeta' metasenv' subst context term' ty termty goal_arity ;; -(****************** AUTO ********************) - - - -(* -let prop = function (_,depth,P) -> depth < 9 | _ -> false;; -*) - -let calculate_timeout flags = +let applyS_tac ~dbd ~term ~params ~automation_cache = + ProofEngineTypes.mk_tactic + (fun status -> + try + apply_smart ~dbd ~term ~params ~automation_cache status + with + | CicUnification.UnificationFailure msg + | CicTypeChecker.TypeCheckerFailure msg -> + raise (ProofEngineTypes.Fail msg)) +;; + + +(****************** AUTO ********************) + +let calculate_timeout flags = if flags.timeout = 0. then (debug_print (lazy "AUTO WITH NO TIMEOUT"); {flags with timeout = infinity}) @@ -868,20 +1187,10 @@ let is_equational_case goalty flags = let ensure_equational t = if is_an_equational_goal t then true else false - (* - let msg="Not an equational goal.\nYou cant use the paramodulation flag"in - raise (ProofEngineTypes.Fail (lazy msg)) - *) in (flags.use_paramod && is_an_equational_goal goalty) || (flags.use_only_paramod && ensure_equational goalty) ;; -(* -let cache_add_success sort cache k v = - if sort = P then cache_add_success cache k v else cache_remove_underinspection - cache k -;; -*) type menv = Cic.metasenv type subst = Cic.substitution @@ -951,7 +1260,8 @@ let calculate_closed_goal_ty (goalno,_,_) s = let cc,_,goalty = List.assoc goalno s in (* XXX applicare la subst al contesto? *) Some (cc, CicMetaSubst.apply_subst s goalty) - with Not_found -> None + with Not_found -> + None ;; let pp_status ctx status = @@ -1207,8 +1517,11 @@ let add_to_cache_and_del_from_orlist_if_green_cut let close_failures (fl : fail list) (cache : cache) = List.fold_left (fun cache ((gno,depth,_),gty) -> - debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno)); - cache_add_failure cache gty depth) + if CicUtil.is_meta_closed gty then + ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno)); + cache_add_failure cache gty depth) + else + cache) cache fl ;; let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty = @@ -1224,6 +1537,7 @@ let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty = let mk_fake_proof metasenv subst (goalno,_,_) goalty context = None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, [] ;; + let equational_case tables cache depth fake_proof goalno goalty subst context flags @@ -1238,7 +1552,6 @@ let equational_case let goal_steps, saturation_steps, timeout = max_int,max_int,flags.timeout in - match Saturation.given_clause bag status active passive goal_steps saturation_steps timeout @@ -1261,9 +1574,20 @@ let equational_case end else begin - debug_print - (lazy - ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty)); + let params = ([],["use_context","false"]) in + let automation_cache = { + AutomationCache.tables = tables ; + AutomationCache.univ = Universe.empty; } + in + try + let ((_,metasenv,subst,_,_,_),open_goals) = + solve_rewrite ~params ~automation_cache + (fake_proof, goalno) + in + let proof = lazy (Cic.Meta (-1,[])) in + [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags + with ProofEngineTypes.Fail _ -> [], tables, cache, flags +(* let res = Saturation.all_subsumed bag status active passive in let res' = List.map @@ -1281,20 +1605,33 @@ let equational_case res in res', (active,passive,bag), cache, flags +*) end ;; -let try_candidate +let sort_new_elems = + List.sort (fun (_,_,_,l1) (_,_,_,l2) -> + let p1 = List.length (prop_only l1) in + let p2 = List.length (prop_only l2) in + if p1 = p2 then List.length l1 - List.length l2 else p1-p2) +;; + + +let try_candidate dbd goalty tables subst fake_proof goalno depth context cand = let ppterm = ppterm context in try let actives, passives, bag = tables in - let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta = - (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:(Equality.maxmeta bag) ~term:cand) + let (_,metasenv,subst,_,_,_), open_goals = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:cand) (fake_proof,goalno) in - let tables = actives, passives, Equality.push_maxmeta bag maxmeta in + let tables = actives, passives, + Equality.push_maxmeta bag + (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst)) + in debug_print (lazy (" OK: " ^ ppterm cand)); let metasenv = CicRefine.pack_coercion_metasenv metasenv in let open_goals = order_new_goals metasenv subst open_goals ppterm in @@ -1306,32 +1643,123 @@ let try_candidate | CicUnification.Uncertain s -> None,tables ;; -let sort_new_elems = - List.sort (fun (_,_,_,l1) (_,_,_,l2) -> - List.length (prop_only l1) - List.length (prop_only l2)) +let applicative_case dbd + tables depth subst fake_proof goalno goalty metasenv context universe + cache flags += + let goalty_aux = + match goalty with + | Cic.Appl (hd::tl) -> + Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl)) + | _ -> goalty + in + let candidates = + get_candidates flags.skip_trie_filtering universe cache goalty_aux + in + let tables, elems = + List.fold_left + (fun (tables,elems) cand -> + match + try_candidate dbd goalty + tables subst fake_proof goalno depth context cand + with + | None, tables -> tables, elems + | Some x, tables -> tables, x::elems) + (tables,[]) candidates + in + let elems = sort_new_elems elems in + elems, tables, cache ;; -let applicative_case +let try_smart_candidate dbd + goalty tables subst fake_proof goalno depth context cand += + let ppterm = ppterm context in + try + let params = ([],[]) in + let automation_cache = { + AutomationCache.tables = tables ; + AutomationCache.univ = Universe.empty; } + in + debug_print (lazy ("candidato per " ^ string_of_int goalno + ^ ": " ^ CicPp.ppterm cand)); +(* + let (_,metasenv,subst,_,_,_) = fake_proof in + prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv); + prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst); +*) + let ((_,metasenv,subst,_,_,_),open_goals) = + apply_smart ~dbd ~term:cand ~params ~automation_cache + (fake_proof, goalno) + in + let metasenv = CicRefine.pack_coercion_metasenv metasenv in + let open_goals = order_new_goals metasenv subst open_goals ppterm in + let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in + incr candidate_no; + Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables + with + | ProofEngineTypes.Fail s -> None,tables + | CicUnification.Uncertain s -> None,tables +;; + +let smart_applicative_case dbd tables depth subst fake_proof goalno goalty metasenv context universe cache flags = - let candidates = get_candidates flags.skip_trie_filtering universe cache goalty in + let signature = MetadataQuery.signature_of metasenv goalno in + let goalty_aux = + match goalty with + | Cic.Appl (hd::tl) -> + Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl)) + | _ -> goalty + in + let smart_candidates = + get_candidates flags.skip_trie_filtering universe cache goalty_aux + in + let candidates = + get_candidates flags.skip_trie_filtering universe cache goalty + in + let smart_candidates = + List.filter + (fun x -> not(List.mem x candidates)) smart_candidates + in + let candidates = List.filter (only signature context metasenv) candidates in + let smart_candidates = + List.filter (only signature context metasenv) smart_candidates + in +(* + let penalty cand depth = + if only signature context metasenv cand then depth else ((prerr_endline ( + "penalizzo " ^ CicPp.ppterm cand));depth -1) + in +*) let tables, elems = List.fold_left (fun (tables,elems) cand -> match - try_candidate goalty + try_candidate dbd goalty tables subst fake_proof goalno depth context cand with | None, tables -> tables, elems | Some x, tables -> tables, x::elems) (tables,[]) candidates in - let elems = sort_new_elems elems in + let tables, smart_elems = + List.fold_left + (fun (tables,elems) cand -> + match + try_smart_candidate dbd goalty + tables subst fake_proof goalno 1 context cand + with + | None, tables -> tables, elems + | Some x, tables -> tables, x::elems) + (tables,[]) smart_candidates + in + let elems = sort_new_elems (elems @ smart_elems) in elems, tables, cache ;; -let equational_and_applicative_case +let equational_and_applicative_case dbd universe flags m s g gty tables cache context = let goalno, depth, sort = g in @@ -1345,15 +1773,20 @@ let equational_and_applicative_case if flags.use_only_paramod then [],tables, cache else - applicative_case + applicative_case dbd tables depth s fake_proof goalno gty m context universe cache flags in elems@more_elems, tables, cache, flags else let elems, tables, cache = - applicative_case tables depth s fake_proof goalno - gty m context universe cache flags + match LibraryObjects.eq_URI () with + | Some _ -> + smart_applicative_case dbd tables depth s fake_proof goalno + gty m context universe cache flags + | None -> + applicative_case dbd tables depth s fake_proof goalno + gty m context universe cache flags in elems, tables, cache, flags ;; @@ -1442,21 +1875,23 @@ let condition_for_prune_hint prune (m, s, size, don, todo, fl) = in List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s ;; -let filter_prune_hint l = +let filter_prune_hint c l = let prune = !prune_hint in prune_hint := []; (* possible race... *) - if prune = [] then l - else List.filter (condition_for_prune_hint prune) l + if prune = [] then c,l + else + cache_reset_underinspection c, + List.filter (condition_for_prune_hint prune) l ;; -let auto_main tables context flags universe cache elems = +let auto_main dbd tables context flags universe cache elems = auto_context := context; let rec aux tables flags cache (elems : status) = -(* pp_status context elems; *) + pp_status context elems; (* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration auto_status := elems; check_pause (); *) - let elems = filter_prune_hint elems in + let cache, elems = filter_prune_hint cache elems in match elems with | (m, s, size, don, todo, fl)::orlist when !hint <> None -> debug_print (lazy "skip"); @@ -1559,7 +1994,7 @@ let auto_main tables context flags universe cache elems = CicPp.ppterm gty)); (* elems are possible computations for proving gty *) let elems, tables, cache, flags = - equational_and_applicative_case + equational_and_applicative_case dbd universe flags m s g gty tables cache context in if elems = [] then @@ -1607,7 +2042,7 @@ let auto_main tables context flags universe cache elems = let - auto_all_solutions tables universe cache context metasenv gl flags + auto_all_solutions dbd tables universe cache context metasenv gl flags = let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = @@ -1616,7 +2051,7 @@ let in let elems = [metasenv,[],1,[],goals,[]] in let rec aux tables solutions cache elems flags = - match auto_main tables context flags universe cache elems with + match auto_main dbd tables context flags universe cache elems with | Gaveup (tables,cache) -> solutions,cache, tables | Proved (metasenv,subst,others,tables,cache) -> @@ -1643,12 +2078,12 @@ let (******************* AUTO ***************) -let auto flags metasenv tables universe cache context metasenv gl = +let auto dbd flags metasenv tables universe cache context metasenv gl = let initial_time = Unix.gettimeofday() in let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in let elems = [metasenv,[],1,[],goals,[]] in - match auto_main tables context flags universe cache elems with + match auto_main dbd tables context flags universe cache elems with | Proved (metasenv,subst,_, tables,cache) -> debug_print(lazy ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); @@ -1659,19 +2094,6 @@ let auto flags metasenv tables universe cache context metasenv gl = None,cache ;; -let applyS_tac ~dbd ~term ~params ~automation_cache = - ProofEngineTypes.mk_tactic - (fun status -> - try - let proof, gl,_,_ = - apply_smart ~dbd ~term ~subst:[] ~params ~automation_cache status - in - proof, gl - with - | CicUnification.UnificationFailure msg - | CicTypeChecker.TypeCheckerFailure msg -> - raise (ProofEngineTypes.Fail msg)) - let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) = let flags = flags_of_params params () in let use_library = flags.use_library in @@ -1680,21 +2102,21 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa ~dbd ~use_library ~use_context:(not flags.skip_context) automation_cache univ (proof, goal) in - let _,metasenv,_subst,_,_, _ = proof in + let _,metasenv,subst,_,_, _ = proof in let _,context,goalty = CicUtil.lookup_meta goal metasenv in let tables,cache = if flags.close_more then close_more tables context (proof, goal) - auto_all_solutions universe cache + (auto_all_solutions dbd) universe cache else tables,cache in let initial_time = Unix.gettimeofday() in - let (_,oldmetasenv,_subst,_,_, _) = proof in + let (_,oldmetasenv,_,_,_, _) = proof in hint := None; let elem = - metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[] + metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[] in - match auto_main tables context flags universe cache [elem] with + match auto_main dbd tables context flags universe cache [elem] with | Proved (metasenv,subst,_, tables,cache) -> debug_print (lazy ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); @@ -1717,270 +2139,6 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa let auto_tac ~dbd ~params ~automation_cache = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~automation_cache);; -let eq_of_goal = function - | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri -> - uri - | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) -;; - -(* performs steps of rewrite with the universe, obtaining if possible - * a trivial goal *) -let solve_rewrite_tac ~automation_cache ~params:(univ,params) (proof,goal)= - let steps = int_of_string (string params "steps" "1") in - let use_context = bool params "use_context" true in - let universe, tables, cache = - init_cache_and_tables ~use_library:false ~use_context - automation_cache univ (proof,goal) - in - let actives, passives, bag = tables in - let pa,metasenv,_subst,pb,pc,pd = proof in - let _,context,ty = CicUtil.lookup_meta goal metasenv in - let eq_uri = eq_of_goal ty in - let initgoal = [], metasenv, ty in - let table = - let equalities = (Saturation.list_of_passive passives) in - List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd actives) equalities - in - let env = metasenv,context,CicUniv.oblivion_ugraph in - match Indexing.solve_demodulating bag env table initgoal steps with - | Some (proof, metasenv, newty) -> - let refl = - match newty with - | Cic.Appl[Cic.MutInd _;eq_ty;left;_] -> - Equality.Exact (Equality.refl_proof eq_uri eq_ty left) - | _ -> assert false - in - let proofterm,_ = - Equality.build_goal_proof - bag eq_uri proof refl newty [] context metasenv - in - let proofterm, _, metasenv, _ = - CicRefine.type_of_aux' metasenv context proofterm - CicUniv.oblivion_ugraph - in - let status = (pa,metasenv,_subst,pb,pc,pd), goal in - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:proofterm) status - | None -> - raise - (ProofEngineTypes.Fail (lazy - ("Unable to solve with " ^ string_of_int steps ^ " demodulations"))) -;; -let solve_rewrite_tac ~params ~automation_cache () = - ProofEngineTypes.mk_tactic (solve_rewrite_tac ~automation_cache ~params) -;; - -(* Demodulate thorem *) -let open_type ty bo = - let rec open_type_aux context ty k args = - match ty with - | Cic.Prod (n,s,t) -> - let n' = - FreshNamesGenerator.mk_fresh_name [] context n ~typ:s ~subst:[] in - let entry = match n' with - | Cic.Name _ -> Some (n',(Cic.Decl s)) - | Cic.Anonymous -> None - in - open_type_aux (entry::context) t (k+1) ((Cic.Rel k)::args) - | Cic.LetIn (n,s,sty,t) -> - let entry = Some (n,(Cic.Def (s,sty))) - in - open_type_aux (entry::context) t (k+1) args - | _ -> context, ty, args - in - let context, ty, args = open_type_aux [] ty 1 [] in - match args with - | [] -> context, ty, bo - | _ -> context, ty, Cic.Appl (bo::args) -;; - -let rec close_type bo ty context = - match context with - | [] -> assert_proof_is_valid bo [] [] ty; (bo,ty) - | Some (n,(Cic.Decl s))::tl -> - close_type (Cic.Lambda (n,s,bo)) (Cic.Prod (n,s,ty)) tl - | Some (n,(Cic.Def (s,sty)))::tl -> - close_type (Cic.LetIn (n,s,sty,bo)) (Cic.LetIn (n,s,sty,ty)) tl - | _ -> assert false -;; - -let is_subsumed univ context ty = - let candidates = Universe.get_candidates univ ty in - List.fold_left - (fun res cand -> - match res with - | Some found -> Some found - | None -> - try - let mk_irl = CicMkImplicit.identity_relocation_list_for_metavariable in - let metasenv = [(0,context,ty)] in - let fake_proof = None,metasenv,[] , (lazy (Cic.Meta(0,mk_irl context))),ty,[] in - let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta = - (PrimitiveTactics.apply_with_subst ~subst:[] ~maxmeta:0 ~term:cand) (fake_proof,0) - in - let prop_goals, other = split_goals_in_prop metasenv subst open_goals in - if prop_goals = [] then Some cand else None - with - | ProofEngineTypes.Fail s -> None - | CicUnification.Uncertain s -> None - ) None candidates -;; - -let demodulate_theorem ~automation_cache uri = - let eq_uri = - match LibraryObjects.eq_URI () with - | Some (uri) -> uri - | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in - let obj,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - in - let context,ty,bo = - match obj with - | Cic.Constant(n, _, ty ,_, _) -> open_type ty (Cic.Const(uri,[])) - | _ -> raise (ProofEngineTypes.Fail (lazy "not a theorem")) - in - if CicUtil.is_closed ty then - raise (ProofEngineTypes.Fail (lazy ("closed term: dangerous reduction"))); - let initgoal = [], [], ty in - (* compute the signature *) - let signature = - let ty_set = MetadataConstraints.constants_of ty in - let hyp_set = MetadataQuery.signature_of_hypothesis context [] in - let set = MetadataConstraints.UriManagerSet.union ty_set hyp_set in - MetadataQuery.close_with_types set [] context - in - (* retrieve equations from the universe universe *) - (* XXX automation_cache *) - let universe = automation_cache.AutomationCache.univ in - let equations = - retrieve_equations true signature universe AutoCache.cache_empty context [] - in - debug_print - (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations)))); - let eqs_and_types = - HExtlib.filter_map - (fun t -> - let ty,_ = - CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph - in - (* retrieve_equations could also return flexible terms *) - if is_an_equality ty then Some(t,ty) - else - try - let ty' = unfold context ty in - if is_an_equality ty' then Some(t,ty') else None - with ProofEngineTypes.Fail _ -> None) - equations - in - let bag = Equality.mk_equality_bag () in - - let bag, units, _, newmeta = - partition_unit_equalities context [] (CicMkImplicit.new_meta [] []) bag eqs_and_types - in - let table = - List.fold_left - (fun tbl eq -> Indexing.index tbl eq) - Indexing.empty units - in - let changed,(newproof,newmetasenv, newty) = - Indexing.demod bag - ([],context,CicUniv.oblivion_ugraph) table initgoal in - if changed then - begin - let oldproof = Equality.Exact bo in - let proofterm,_ = - Equality.build_goal_proof (~contextualize:false) (~forward:true) bag - eq_uri newproof oldproof ty [] context newmetasenv - in - if newmetasenv <> [] then - raise (ProofEngineTypes.Fail (lazy ("metasenv not empty"))) - else - begin - assert_proof_is_valid proofterm newmetasenv context newty; - match is_subsumed universe context newty with - | Some t -> raise - (ProofEngineTypes.Fail (lazy ("subsumed by " ^ CicPp.ppterm t))) - | None -> close_type proofterm newty context - end - end - else (* if newty = ty then *) - raise (ProofEngineTypes.Fail (lazy "no progress")) - (*else ProofEngineTypes.apply_tactic - (ReductionTactics.simpl_tac - ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*) -;; - - -(* NEW DEMODULATE *) -let demodulate_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)= - let universe, tables, cache = - init_cache_and_tables - ~dbd ~use_library:false ~use_context:true - automation_cache univ (proof,goal) - in - let eq_uri = - match LibraryObjects.eq_URI () with - | Some (uri) -> uri - | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in - let active, passive, bag = tables in - let curi,metasenv,_subst,pbo,pty, attrs = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - let initgoal = [], metasenv, ty in - let equalities = (Saturation.list_of_passive passive) in - (* we demodulate using both actives passives *) - let env = metasenv,context,CicUniv.empty_ugraph in - debug_print (lazy ("PASSIVES:" ^ string_of_int(List.length equalities))); - List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e))) - equalities; - let table = - List.fold_left - (fun tbl eq -> Indexing.index tbl eq) - (snd active) equalities - in - let changed,(newproof,newmetasenv, newty) = - (* Indexing.demodulation_goal bag *) - Indexing.demod bag - (metasenv,context,CicUniv.oblivion_ugraph) table initgoal - in - if changed then - begin - let maxm = CicMkImplicit.new_meta metasenv [] in - let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in - let proofterm,_ = - Equality.build_goal_proof (~contextualize:false) bag - eq_uri newproof opengoal ty [] context metasenv - in - let metasenv = (maxm,context,newty)::metasenv in - let proofterm, _, metasenv, _ = - CicRefine.type_of_aux' metasenv context proofterm - CicUniv.oblivion_ugraph - in - let extended_status = - (curi,metasenv,_subst,pbo,pty, attrs),goal in - let (status,newgoals) = - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:proofterm) - extended_status in - (status,maxm::newgoals) - end - else (* if newty = ty then *) - raise (ProofEngineTypes.Fail (lazy "no progress")) - (*else ProofEngineTypes.apply_tactic - (ReductionTactics.simpl_tac - ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*) -;; - -let demodulate_tac ~dbd ~params ~automation_cache = - ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~automation_cache);; - -let demodulate_tac ~dbd ~params:(_,flags as params) ~automation_cache = - let all = bool flags "all" false in - if all then - solve_rewrite_tac ~params ~automation_cache () - else - demodulate_tac ~dbd ~params ~automation_cache -;; - let pp_proofterm = Equality.pp_proofterm;; let revision = "$Revision$";; diff --git a/helm/software/components/tactics/auto.mli b/helm/software/components/tactics/auto.mli index d5297e7b8..c8a9224cb 100644 --- a/helm/software/components/tactics/auto.mli +++ b/helm/software/components/tactics/auto.mli @@ -49,11 +49,6 @@ val demodulate_theorem : UriManager.uri -> Cic.term * Cic.term -val solve_rewrite_tac: - params:auto_params -> - automation_cache:AutomationCache.cache -> - unit -> ProofEngineTypes.tactic - type auto_status = Cic.context * (* or list: goalno, goaltype, grey, depth, candidates: (goalno, c) *) diff --git a/helm/software/components/tactics/autoCache.ml b/helm/software/components/tactics/autoCache.ml index 7458e5777..882a18393 100644 --- a/helm/software/components/tactics/autoCache.ml +++ b/helm/software/components/tactics/autoCache.ml @@ -153,3 +153,6 @@ let cache_size (_,oldcache) = let cache_clean (univ,oldcache) = univ,List.filter (function (_,Succeded _) -> true | _ -> false) oldcache ;; +let cache_reset_underinspection (u,c) = + u,List.filter (function (_,UnderInspection) -> false | _ -> true) c +;; diff --git a/helm/software/components/tactics/autoCache.mli b/helm/software/components/tactics/autoCache.mli index 61c658811..c4c99c382 100644 --- a/helm/software/components/tactics/autoCache.mli +++ b/helm/software/components/tactics/autoCache.mli @@ -38,6 +38,7 @@ val cache_add_failure: cache -> cache_key -> int -> cache val cache_add_success: cache -> cache_key -> Cic.term -> cache val cache_add_underinspection: cache -> cache_key -> int -> cache val cache_remove_underinspection: cache -> cache_key -> cache +val cache_reset_underinspection: cache -> cache val cache_empty: cache val cache_print: Cic.context -> cache -> string val cache_size: cache -> int diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index 0cc52ac1a..428e858c5 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -196,8 +196,9 @@ let rewritingstep ~dbd ~automation_cache lhs rhs just last_step = Tactics.auto ~dbd ~params:(univ, params') ~automation_cache] | `Term just -> Tactics.apply just | `SolveWith term -> - Tactics.solve_rewrite ~automation_cache - ~params:([term],["steps","1"; "use_context","false"]) () + Tactics.demodulate ~automation_cache ~dbd + ~params:([term], + ["all","1";"steps","1"; "use_context","false"]) | `Proof -> Tacticals.id_tac in @@ -275,7 +276,7 @@ let we_proceed_by_cases_on t pat = ;; let we_proceed_by_induction_on t pat = - let pattern = None, [], Some pat in +(* let pattern = None, [], Some pat in *) Tactics.elim_intros ~depth:0 (*~pattern*) t ;; diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index 6eae44531..1a0fe31d0 100644 --- a/helm/software/components/tactics/equalityTactics.ml +++ b/helm/software/components/tactics/equalityTactics.ml @@ -40,28 +40,27 @@ module LO = LibraryObjects module DTI = DoubleTypeInference module HEL = HExtlib -let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = - let _rewrite_tac status = +let rec rewrite ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status= assert (wanted = None); (* this should be checked syntactically *) let proof,goal = status in - let curi, metasenv, _subst, pbo, pty, attrs = proof in + let curi, metasenv, subst, pbo, pty, attrs = proof in let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in match hyps_pat with he::(_::_ as tl) -> - PET.apply_tactic + PET.apply_tactic (T.then_ - (rewrite_tac ~direction - ~pattern:(None,[he],None) equality) - (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) - (S.lift 1 equality)) + (PET.mk_tactic (rewrite ~direction + ~pattern:(None,[he],None) equality)) + (PET.mk_tactic (rewrite ~direction + ~pattern:(None,tl,concl_pat) (S.lift 1 equality))) ) status | [_] as hyps_pat when concl_pat <> None -> - PET.apply_tactic + PET.apply_tactic (T.then_ - (rewrite_tac ~direction - ~pattern:(None,hyps_pat,None) equality) - (rewrite_tac ~direction ~pattern:(None,[],concl_pat) - (S.lift 1 equality)) + (PET.mk_tactic (rewrite ~direction + ~pattern:(None,hyps_pat,None) equality)) + (PET.mk_tactic (rewrite ~direction + ~pattern:(None,[],concl_pat) (S.lift 1 equality))) ) status | _ -> let arg,dir2,tac,concl_pat,gty = @@ -88,14 +87,16 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = | _::_ -> assert false in let gsort,_ = - CicTypeChecker.type_of_aux' metasenv context gty CicUniv.oblivion_ugraph in + CicTypeChecker.type_of_aux' + metasenv ~subst context gty CicUniv.oblivion_ugraph + in let if_right_to_left do_not_change a b = match direction with | `RightToLeft -> if do_not_change then a else b | `LeftToRight -> if do_not_change then b else a in let ty_eq,ugraph = - CicTypeChecker.type_of_aux' metasenv context equality + CicTypeChecker.type_of_aux' metasenv ~subst context equality CicUniv.oblivion_ugraph in let (ty_eq,metasenv',arguments,fresh_meta) = TermUtil.saturate_term @@ -131,7 +132,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = (* now we always do as if direction was `LeftToRight *) let fresh_name = FreshNamesGenerator.mk_fresh_name - ~subst:[] metasenv' context C.Anonymous ~typ:ty in + ~subst metasenv' context C.Anonymous ~typ:ty in let lifted_t1 = S.lift 1 t1x in let lifted_gty = S.lift 1 gty in let lifted_conjecture = @@ -147,7 +148,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = in let subst,metasenv',ugraph,_,selected_terms_with_context = ProofEngineHelpers.select - ~metasenv:metasenv' ~ugraph ~conjecture:lifted_conjecture + ~metasenv:metasenv' ~subst ~ugraph ~conjecture:lifted_conjecture ~pattern:lifted_pattern in let metasenv' = CicMetaSubst.apply_subst_metasenv subst metasenv' in let what,with_what = @@ -175,6 +176,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = let metasenv',arg,newtyp = match arg with None -> + let fresh_meta = CicMkImplicit.new_meta metasenv' subst in let gty' = S.subst t2 abstr_gty in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in @@ -189,8 +191,8 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = in try let (proof',goals) = - PET.apply_tactic - (tac ~term:exact_proof newtyp) ((curi,metasenv',_subst,pbo,pty, attrs),goal) + PET.apply_tactic (tac ~term:exact_proof newtyp) + ((curi,metasenv',subst,pbo,pty, attrs),goal) in let goals = goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv @@ -201,15 +203,15 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = TC.TypeCheckerFailure m -> let msg = lazy ("rewrite: "^ Lazy.force m) in raise (PET.Fail msg) - in - PET.mk_tactic _rewrite_tac +;; let rewrite_tac ~direction ~pattern equality names = let _, hyps_pat, _ = pattern in let froms = List.map fst hyps_pat in - let start = rewrite_tac ~direction ~pattern equality in + let start = PET.mk_tactic (rewrite ~direction ~pattern equality) in let continuation = PESR.rename ~froms ~tos:names in if names = [] then start else T.then_ ~start ~continuation +;; let rewrite_simpl_tac ~direction ~pattern equality names = T.then_ @@ -218,12 +220,11 @@ let rewrite_simpl_tac ~direction ~pattern equality names = (ReductionTactics.simpl_tac ~pattern:(ProofEngineTypes.conclusion_pattern None)) - let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status = let _wanted, hyps_pat, concl_pat = pattern in let (proof, goal) = status in - let uri,metasenv,_subst,pbo,pty, attrs = proof in + let uri,metasenv,subst,pbo,pty, attrs = proof in let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in assert (hyps_pat = []); (*CSC: not implemented yet *) let eq_URI = @@ -233,17 +234,17 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = in let context_len = List.length context in let subst,metasenv,u,_,selected_terms_with_context = - ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph + ProofEngineHelpers.select ~subst ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in let with_what, metasenv, u = with_what context metasenv u in let with_what = CicMetaSubst.apply_subst subst with_what in let pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in let pty = CicMetaSubst.apply_subst subst pty in - let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in + let status = (uri,metasenv,subst,pbo,pty, attrs),goal in let ty_of_with_what,u = CicTypeChecker.type_of_aux' - metasenv context with_what CicUniv.oblivion_ugraph in + metasenv ~subst context with_what CicUniv.oblivion_ugraph in let whats = match selected_terms_with_context with [] -> raise (ProofEngineTypes.Fail (lazy "Replace: no term selected")) @@ -269,9 +270,9 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = raise (ProofEngineTypes.Fail (lazy "Replace: one of the selected terms is not closed")) in let ty_of_t_in_context,u = (* TASSI: FIXME *) - CicTypeChecker.type_of_aux' metasenv context t_in_context + CicTypeChecker.type_of_aux' metasenv ~subst context t_in_context CicUniv.oblivion_ugraph in - let b,u = CicReduction.are_convertible ~metasenv context + let b,u = CicReduction.are_convertible ~metasenv ~subst context ty_of_with_what ty_of_t_in_context u in if b then let concl_pat_for_t = ProofEngineHelpers.pattern_of ~term:ty [t] in @@ -301,13 +302,14 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = ~continuations:[ T.then_ ~start:( - rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1) []) + rewrite_tac + ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1) []) ~continuation:( T.then_ ~start:( ProofEngineTypes.mk_tactic (function ((proof,goal) as status) -> - let _,metasenv,_subst,_,_, _ = proof in + let _,metasenv,_,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let hyps = try @@ -336,14 +338,14 @@ let reflexivity_tac = let symmetry_tac = let symmetry_tac (proof, goal) = - let (_,metasenv,_subst,_,_, _) = proof in + let (_,metasenv,_,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when LibraryObjects.is_eq_URI uri -> ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac - ~term: (C.Const (LibraryObjects.sym_eq_URI uri, []))) + ~term:(C.Const (LibraryObjects.sym_eq_URI uri, []))) (proof,goal) | _ -> raise (ProofEngineTypes.Fail (lazy "Symmetry failed")) @@ -354,7 +356,7 @@ let symmetry_tac = let transitivity_tac ~term = let transitivity_tac ~term status = let (proof, goal) = status in - let (_,metasenv,_subst,_,_, _) = proof in + let (_,metasenv,_,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index bf0e71bbd..5888019e4 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -898,9 +898,7 @@ let relocate newmeta menv to_be_relocated = let fix_metas_goal (id_to_eq,newmeta) goal = let (proof, menv, ty) = goal in - let to_be_relocated = - HExtlib.list_uniq (List.sort Pervasives.compare (Utils.metas_of_term ty)) - in + let to_be_relocated = List.map (fun i ,_,_ -> i) menv in let subst, menv, newmeta = relocate newmeta menv to_be_relocated in let ty = Subst.apply_subst subst ty in let proof = diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index cdddc6595..b5d683dc9 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -556,7 +556,7 @@ let subsumption_all x y z = ;; let unification_all x y z = - prerr_endline "unification_all"; subsumption_aux_all true x y z + subsumption_aux_all true x y z ;; let rec demodulation_aux bag ?from ?(typecheck=false) @@ -1232,9 +1232,6 @@ let rec demodulation_goal bag env table goal = | None -> do_right () ;; -type next = L | R -type solved = Yes of Equality.goal | No of Equality.goal list - (* returns all the 1 step demodulations *) module C = Cic;; module S = CicSubstitution;; @@ -1250,7 +1247,8 @@ let rec demodulation_all_aux let termty, ugraph = C.Implicit None, ugraph in let res = find_all_matches - metasenv context ugraph lift_amount term termty candidates + ~unif_fun:Founif.matching + metasenv context ugraph lift_amount term termty candidates in match term with | C.Appl l -> @@ -1267,87 +1265,124 @@ let rec demodulation_all_aux (res, [], List.map (S.lift 1) l) l in res - | C.Prod (nn, s, t) - | C.Lambda (nn, s, t) -> - let context = (Some (nn, C.Decl s))::context in - let mk s t = - match term with - | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t) - in - res @ - List.map - (fun (rel, subst, m, ug, c) -> - mk (S.lift 1 s) rel, subst, m, ug, c) - (demodulation_all_aux - metasenv context ugraph table (lift_amount+1) t) - (* we could demodulate also in s, but then t may be badly - * typed... *) | t -> res ;; -let solve_demodulating bag env table initgoal steps = +let demod_all steps bag env table goal = let _, context, ugraph = env in - let solved goal res side = - let newg = build_newgoal bag context goal side Equality.Demodulation res in - match newg with - | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right]) - when LibraryObjects.is_eq_URI uri -> - (try - let _ = - Founif.unification [] m context left right CicUniv.empty_ugraph - in - Yes newg - with CicUnification.UnificationFailure _ -> No [newg]) - | _ -> No [newg] + let is_visited l (_,_,t) = + List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l in - let solved goal res_list side = - let newg = List.map (fun x -> solved goal x side) res_list in - try - List.find (function Yes _ -> true | _ -> false) newg - with Not_found -> - No (List.flatten (List.map (function No s -> s | _-> assert false) newg)) + let rec aux steps visited bag = function + | _ when steps = 0 -> visited, bag, [] + | [] -> visited, bag, [] + | goal :: rest when is_visited visited goal -> aux steps visited bag rest + | goal :: rest -> + let visited = goal :: visited in + let _,menv,t = goal in + let res = demodulation_all_aux menv context ugraph table 0 t in + let steps = if res = [] then steps-1 else steps in + let new_goals = + List.map (build_newg bag context goal Equality.Demodulation) res + in + (* we need this cause an equation E like + F ?x => F ?y + can add a meta for y in a goal without instantiating it + P (F true) ----> P (F ?y) + and this may cause duplicated in metasenvs + demodulating again with E + *) + let bag, new_goals = + List.fold_right + (fun g (bag,acc) -> + let bag, g = Equality.fix_metas_goal bag g in + bag, g::acc) + new_goals (bag,[]) + in + let visited, bag, res = aux steps visited bag (new_goals @ rest) in + visited, bag, goal :: res in - let rec first f acc l = - match l with - | [] -> acc,None - | x::tl -> - match f acc x with - | acc,None -> first f acc tl - | acc,Some x as ok -> ok + aux steps [] bag [goal] +;; + + +let solve_demodulating bag env table initgoal steps = + let proof,menv,eq,ty,left,right = open_goal initgoal in + let uri = + match eq with + | Cic.MutInd (u,_,_) -> u + | _ -> assert false in - let rec aux steps next visited goal = - if steps = 0 then visited, None else - let goalproof,menv,_,_,left,right = open_goal goal in - if (List.mem (left,right,next) visited || List.mem (right,left,next) visited) - then visited, None else - let do_step t = - demodulation_all_aux menv context ugraph table 0 t + let _, context, ugraph = env in + let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in + let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in + let is_solved left right ml mr = + let m = ml @ (List.filter + (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr) in - let visited = (left,right,next) :: visited in - match next with - | L -> - (match do_step left with - | _::_ as res -> - (match solved goal res Utils.Right with - | No newgoals -> - (match first (aux (steps - 1) L) visited newgoals with - | _,Some g as success -> success - | visited,None -> aux steps R visited goal) - | Yes newgoal -> visited, Some newgoal) - | [] -> aux steps R visited goal) - | R -> - (match do_step right with - | _::_ as res -> - (match solved goal res Utils.Left with - | No newgoals -> - (match first (aux (steps - 1) L) visited newgoals with - | visited, Some g as success -> success - | visited, None as failure -> failure) - | Yes newgoal -> visited, Some newgoal) - | [] -> visited, None) + try + let s,_,_ = + Founif.unification [] m context left right CicUniv.empty_ugraph in + Some (bag, m,s,Equality.Exact (Equality.refl_proof uri ty left)) + with CicUnification.UnificationFailure _ -> + let solutions = + unification_all env table (Equality.mk_tmp_equality + (0,(Cic.Implicit None,left,right,Utils.Incomparable),m)) + in + if solutions = [] then None + else + let s, e, swapped = List.hd solutions in + let _,p,(ty,l,r,_),me,id = Equality.open_equality e in + let bag, p = + if swapped then Equality.symmetric bag ty l id uri me else bag, p + in + Some (bag, m,s, p) in - let _, res = aux steps L [] initgoal in - res + let newgoal = + HExtlib.list_findopt + (fun (pr,mr,r) _ -> + try + let pl,ml,l,bag,m,s,p = + match + HExtlib.list_findopt (fun (pl,ml,l) _ -> + match is_solved l r ml mr with + | None -> None + | Some (bag,m,s,p) -> Some (pl,ml,l,bag,m,s,p) + ) l_demod + with Some x -> x | _ -> raise Not_found + in + let pl = + List.map + (fun (rule,pos,id,subst,pred) -> + let pred = + match pred with + | Cic.Lambda (name,src,tgt) -> + Cic.Lambda (name,src, + Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right]) + | _ -> assert false + in + rule,pos,id,subst,pred) + pl + in + let pr = + List.map + (fun (rule,pos,id,subst,pred) -> + let pred = + match pred with + | Cic.Lambda (name,src,tgt) -> + Cic.Lambda (name,src, + Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt]) + | _ -> assert false + in + rule,pos,id,subst,pred) + pr + in + Some (bag,pr@pl@proof,m,s,p) + with Not_found -> None) + r_demod + in + newgoal ;; -let get_stats () = "" ;; + + diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli index 8895b89a0..8370d9da3 100644 --- a/helm/software/components/tactics/paramodulation/indexing.mli +++ b/helm/software/components/tactics/paramodulation/indexing.mli @@ -111,8 +111,6 @@ val solve_demodulating: Index.t -> Equality.goal -> int -> - Equality.goal option + (Equality.equality_bag * Equality.goal_proof * Cic.metasenv * + Subst.substitution * Equality.proof) option - - (** profiling *) -val get_stats: unit -> string diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index ceb8ab5af..8f4e54851 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -803,7 +803,8 @@ let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) = bag, p in bag, Some (goalproof, p, id, subst, cicmenv) - | None -> bag, None) + | None -> + bag, None) | _ -> bag, None ;; @@ -900,7 +901,7 @@ let infer_goal_set bag env active goals = | [] -> bag, (active_goals, []) | hd::tl -> let changed, selected = simplify_goal bag env hd active in - let (_,_,t1) = selected in + let (_,m1,t1) = selected in let already_in = List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) active_goals diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 0040d7ebf..420934944 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -249,17 +249,17 @@ let new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty termt in subst,newmetasenv',t -let rec count_prods context ty = - match CicReduction.whd context ty with - Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t +let rec count_prods subst context ty = + match CicReduction.whd ~subst context ty with + Cic.Prod (n,s,t) -> 1 + count_prods subst (Some (n,Cic.Decl s)::context) t | _ -> 0 -let apply_with_subst ~term ~subst ~maxmeta (proof, goal) = +let apply_with_subst ~term ~maxmeta (proof, goal) = (* Assumption: The term "term" must be closed in the current context *) let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in - let (_,metasenv,_subst,_,_, _) = proof in + let (_,metasenv,subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = @@ -296,11 +296,12 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) = in let metasenv' = metasenv@newmetasenvfragment in let termty,_ = - CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph + CicTypeChecker.type_of_aux' + metasenv' ~subst context term' CicUniv.oblivion_ugraph in let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in - let goal_arity = count_prods context ty in + let goal_arity = count_prods subst context ty in let subst,newmetasenv',t = let rec add_one_argument n = try @@ -330,6 +331,10 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) = newmetasenv'' in let subst = ((metano,(context,bo',ty))::subst) in + let newproof = + let u,m,_,p,t,l = newproof in + u,m,subst,p,t,l + in subst, (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas), max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst) @@ -338,9 +343,12 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) = (* ALB *) let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status = try -(* apply_tac_verbose ~term status *) - apply_with_subst ~term ~subst ~maxmeta status - (* TODO cacciare anche altre eccezioni? *) + let status = + if subst <> [] then + let (u,m,_,p,t,l), g = status in (u,m,subst,p,t,l), g + else status + in + apply_with_subst ~term ~maxmeta status with | CicUnification.UnificationFailure msg | CicTypeChecker.TypeCheckerFailure msg -> raise (PET.Fail msg) @@ -482,7 +490,8 @@ let rec args_init n f = if n <= 0 then [] else f n :: args_init (pred n) f let mk_predicate_for_elim - ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no = + ~context ~metasenv ~subst ~ugraph ~goal ~arg ~using ~cpattern ~args_no += let instantiated_eliminator = let f n = if n = 1 then arg else C.Implicit None in C.Appl (using :: args_init args_no f) @@ -496,22 +505,22 @@ let mk_predicate_for_elim | _ -> assert false in (* let _, upto = PEH.split_with_whd (List.nth splits pred_pos) in *) - let rec mk_pred metasenv context' pred arg' cpattern' = function - | [] -> metasenv, pred, arg' + let rec mk_pred metasenv subst context' pred arg' cpattern' = function + | [] -> metasenv, subst, pred, arg' | arg :: tail -> (* FG: we find the predicate for the eliminator as in the rewrite tactic ****) - let argty, _ugraph = TC.type_of_aux' metasenv context arg ugraph in - let argty = CicReduction.whd context argty in + let argty, _ = TC.type_of_aux' metasenv ~subst context arg ugraph in + let argty = CicReduction.whd ~subst context argty in let fresh_name = FreshNamesGenerator.mk_fresh_name - ~subst:[] metasenv context' C.Anonymous ~typ:argty in + ~subst metasenv context' C.Anonymous ~typ:argty in let hyp = Some (fresh_name, C.Decl argty) in let lazy_term c m u = let distance = List.length c - List.length context in S.lift distance arg, m, u in let pattern = Some lazy_term, [], Some cpattern' in let subst, metasenv, _ugraph, _conjecture, selected_terms = - ProofEngineHelpers.select ~metasenv ~ugraph + ProofEngineHelpers.select ~subst ~metasenv ~ugraph ~conjecture:(0, context, pred) ~pattern in let metasenv = MS.apply_subst_metasenv subst metasenv in let map (_context_of_t, t) l = t :: l in @@ -522,13 +531,13 @@ let mk_predicate_for_elim let pred = MS.apply_subst subst pred in let pred = C.Lambda (fresh_name, argty, pred) in let cpattern' = C.Lambda (C.Anonymous, C.Implicit None, cpattern') in - mk_pred metasenv (hyp :: context') pred arg' cpattern' tail + mk_pred metasenv subst (hyp :: context') pred arg' cpattern' tail in - let metasenv, pred, arg = - mk_pred metasenv context goal arg cpattern (List.rev actual_args) + let metasenv, subst, pred, arg = + mk_pred metasenv subst context goal arg cpattern (List.rev actual_args) in HLog.debug ("PREDICATE: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args)); - metasenv, pred, arg, actual_args + metasenv, subst, pred, arg, actual_args let beta_after_elim_tac upto predicate = let beta_after_elim_tac status = @@ -612,10 +621,10 @@ let generalize_tac let (proof, goal) = status in let module C = Cic in let module T = Tacticals in - let uri,metasenv,_subst,pbo,pty, attrs = proof in + let uri,metasenv,subst,pbo,pty, attrs = proof in let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in let subst,metasenv,u,selected_hyps,terms_with_context = - ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph + ProofEngineHelpers.select ~metasenv ~subst ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern in let context = CicMetaSubst.apply_subst_context subst context in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in @@ -642,7 +651,7 @@ let generalize_tac context_of_t, t context_of_t metasenv u | (context_of_t, t)::_, None -> context_of_t, (t, metasenv, u) in - let t,subst,metasenv' = + let t,e_subst,metasenv' = try CicMetaSubst.delift_rels [] metasenv (List.length context_of_t - List.length context) t @@ -652,7 +661,7 @@ let generalize_tac in (*CSC: I am not sure about the following two assertions; maybe I need to propagate the new subst and metasenv *) - assert (subst = []); + assert (e_subst = []); assert (metasenv' = metasenv); let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in u,typ,t,metasenv @@ -686,7 +695,7 @@ let generalize_tac else u1 ) u terms_with_context) ; - let status = (uri,metasenv',_subst,pbo,pty, attrs),goal in + let status = (uri,metasenv',subst,pbo,pty, attrs),goal in let proof,goals = PET.apply_tactic (T.thens @@ -706,7 +715,7 @@ let generalize_tac T.id_tac]) status in - let _,metasenv'',_subst,_,_, _ = proof in + let _,metasenv'',_,_,_, _ = proof in (* CSC: the following is just a bad approximation since a meta can be closed and then re-opened! *) (proof, @@ -762,7 +771,7 @@ let pattern_after_generalize_pattern_tac (tp, hpatterns, cpattern) = let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = let elim_tac pattern (proof, goal) = let ugraph = CicUniv.oblivion_ugraph in - let curi, metasenv, _subst, proofbo, proofty, attrs = proof in + let curi, metasenv, subst, proofbo, proofty, attrs = proof in let conjecture = CicUtil.lookup_meta goal metasenv in let metano, context, ty = conjecture in let pattern = pattern_after_generalize_pattern_tac pattern in @@ -770,8 +779,8 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = match pattern with | None, [], Some cpattern -> cpattern | _ -> raise (PET.Fail (lazy "not implemented")) in - let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in - let termty = CicReduction.whd context termty in + let termty,_ugraph = TC.type_of_aux' metasenv ~subst context term ugraph in + let termty = CicReduction.whd ~subst context termty in let termty, metasenv', arguments, _fresh_meta = TermUtil.saturate_term (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in @@ -793,7 +802,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = name | _ -> assert false in - let ty_ty,_ugraph = TC.type_of_aux' metasenv' context ty ugraph in + let ty_ty,_ugraph = TC.type_of_aux' metasenv' ~subst context ty ugraph in let ext = match ty_ty with C.Sort C.Prop -> "_ind" @@ -810,7 +819,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = | Some t -> t in let ety, _ugraph = - TC.type_of_aux' metasenv' context eliminator_ref ugraph in + TC.type_of_aux' metasenv' ~subst context eliminator_ref ugraph in (* FG: ADDED PART ***********************************************************) (* FG: we can not assume eliminator is the default eliminator ***************) let splits, args_no = PEH.split_with_whd (context, ety) in @@ -819,13 +828,13 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = | _, C.Appl (C.Rel i :: _) when i > 1 && i <= args_no -> i | _ -> raise NotAnEliminator in - let metasenv', pred, term, actual_args = match pattern with + let metasenv', subst, pred, term, actual_args = match pattern with | None, [], Some (C.Implicit (Some `Hole)) -> - metasenv', C.Implicit None, term, [] + metasenv', subst, C.Implicit None, term, [] | _ -> mk_predicate_for_elim ~args_no ~context ~ugraph ~cpattern - ~metasenv:metasenv' ~arg:term ~using:eliminator_ref ~goal:ty + ~metasenv:metasenv' ~subst ~arg:term ~using:eliminator_ref ~goal:ty in (* FG: END OF ADDED PART ****************************************************) let term_to_refine = @@ -835,20 +844,20 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = in C.Appl (eliminator_ref :: args_init args_no f) in - let refined_term,_refined_termty,metasenv'',_ugraph = - CicRefine.type_of_aux' metasenv' context term_to_refine ugraph + let refined_term,_refined_termty,metasenv'',subst,_ugraph = + CicRefine.type_of metasenv' subst context term_to_refine ugraph in let new_goals = ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:metasenv'' in - let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in + let proof' = curi,metasenv'',subst,proofbo,proofty, attrs in let proof'', new_goals' = PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal) in (* The apply_tactic can have closed some of the new_goals *) let patched_new_goals = - let (_,metasenv''',_subst,_,_, _) = proof'' in + let (_,metasenv''',_,_,_, _) = proof'' in List.filter (function i -> List.exists (function (j,_,_) -> j=i) metasenv''') new_goals @ new_goals' diff --git a/helm/software/components/tactics/primitiveTactics.mli b/helm/software/components/tactics/primitiveTactics.mli index 24d5cbc88..f2178fb38 100644 --- a/helm/software/components/tactics/primitiveTactics.mli +++ b/helm/software/components/tactics/primitiveTactics.mli @@ -51,17 +51,13 @@ val generalize_tac: ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic -(* ALB, needed by the new paramodulation... *) -val apply_with_subst: - term:Cic.term -> ?subst:Cic.substitution -> ?maxmeta:int -> ProofEngineTypes.proof * int -> - Cic.substitution * (ProofEngineTypes.proof * int list) * int - (* not a real tactic *) val apply_tac_verbose : term:Cic.term -> ProofEngineTypes.proof * int -> (Cic.term -> Cic.term) * (ProofEngineTypes.proof * int list) +(* the proof status has a subst now, and apply_tac honors it *) val apply_tac: term: Cic.term -> ProofEngineTypes.tactic val applyP_tac: (* apply for procedural reconstruction *) @@ -101,7 +97,7 @@ val cases_intros_tac: (* FG *) val mk_predicate_for_elim: - context:Cic.context -> metasenv:Cic.metasenv -> + context:Cic.context -> metasenv:Cic.metasenv -> subst:Cic.substitution -> ugraph:CicUniv.universe_graph -> goal:Cic.term -> arg:Cic.term -> using:Cic.term -> cpattern:Cic.term -> args_no:int -> - Cic.metasenv * Cic.term * Cic.term * Cic.term list + Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.term list diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml index fc508f0c1..d95d37d8c 100644 --- a/helm/software/components/tactics/proofEngineHelpers.ml +++ b/helm/software/components/tactics/proofEngineHelpers.ml @@ -27,8 +27,8 @@ exception Bad_pattern of string Lazy.t -let new_meta_of_proof ~proof:(_, metasenv, _, _, _, _) = - CicMkImplicit.new_meta metasenv [] +let new_meta_of_proof ~proof:(_, metasenv, subst, _, _, _) = + CicMkImplicit.new_meta metasenv subst let subst_meta_in_proof proof meta term newmetasenv = let uri,metasenv,initial_subst,bo,ty, attrs = proof in @@ -229,7 +229,9 @@ let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t = in find subst metasenv ugraph context wanted t -let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = +let select_in_term + ~metasenv ~subst ~context ~ugraph ~term ~pattern:(wanted,where) += let add_ctx context name entry = (Some (name, entry)) :: context in let map2 error_msg f l1 l2 = try @@ -313,13 +315,13 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = | Some where -> aux context where term in match wanted with - None -> [],metasenv,ugraph,roots + None -> subst,metasenv,ugraph,roots | Some wanted -> - let rec find_in_roots = + let rec find_in_roots subst = function - [] -> [],metasenv,ugraph,[] + [] -> subst,metasenv,ugraph,[] | (context',where)::tl -> - let subst,metasenv,ugraph,tl' = find_in_roots tl in + let subst,metasenv,ugraph,tl' = find_in_roots subst tl in let subst,metasenv,ugraph,found = let wanted, metasenv, ugraph = wanted context' metasenv ugraph in find_subterms ~subst ~metasenv ~ugraph ~wanted ~context:context' @@ -327,7 +329,8 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = in subst,metasenv,ugraph,found @ tl' in - find_in_roots roots + find_in_roots subst roots +;; (** create a pattern from a term and a list of subterms. * the pattern is granted to have a ? for every subterm that has no selected @@ -483,7 +486,7 @@ exception Fail of string Lazy.t * * @raise Bad_pattern * *) - let select ~metasenv ~ugraph ~conjecture:(_,context,ty) + let select ~metasenv ~subst ~ugraph ~conjecture:(_,context,ty) ~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern) = let what, hyp_patterns, goal_pattern = pattern in @@ -507,8 +510,9 @@ exception Fail of string Lazy.t aux [] context in let subst,metasenv,ugraph,ty_terms = - select_in_term ~metasenv ~context ~ugraph ~term:ty - ~pattern:(what,goal_pattern) in + select_in_term ~metasenv ~subst ~context ~ugraph ~term:ty + ~pattern:(what,goal_pattern) + in let subst,metasenv,ugraph,context_terms = let subst,metasenv,ugraph,res,_ = (List.fold_right @@ -521,7 +525,7 @@ exception Fail of string Lazy.t subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context) | Some pat -> let subst,metasenv,ugraph,terms = - select_in_term ~metasenv ~context ~ugraph ~term + select_in_term ~subst ~metasenv ~context ~ugraph ~term ~pattern:(what, Some pat) in subst,metasenv,ugraph,((Some (`Decl terms))::res), @@ -534,11 +538,11 @@ exception Fail of string Lazy.t (entry::context) | Some pat -> let subst,metasenv,ugraph,terms_bo = - select_in_term ~metasenv ~context ~ugraph ~term:bo + select_in_term ~subst ~metasenv ~context ~ugraph ~term:bo ~pattern:(what, Some pat) in let subst,metasenv,ugraph,terms_ty = let subst,metasenv,ugraph,res = - select_in_term ~metasenv ~context ~ugraph ~term:ty + select_in_term ~subst ~metasenv ~context ~ugraph ~term:ty ~pattern:(what, Some pat) in subst,metasenv,ugraph,res @@ -550,6 +554,7 @@ exception Fail of string Lazy.t subst,metasenv,ugraph,res in subst,metasenv,ugraph,context_terms, ty_terms +;; (** locate_in_term equality what where context * [what] must match a subterm of [where] according to [equality] diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli index 714860501..c57efff5d 100644 --- a/helm/software/components/tactics/proofEngineHelpers.mli +++ b/helm/software/components/tactics/proofEngineHelpers.mli @@ -74,6 +74,7 @@ val pattern_of: * *) val select: metasenv:Cic.metasenv -> + subst:Cic.substitution -> ugraph:CicUniv.universe_graph -> conjecture:Cic.conjecture -> pattern:ProofEngineTypes.lazy_pattern -> diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml index c943e7a19..2684222d4 100644 --- a/helm/software/components/tactics/reductionTactics.ml +++ b/helm/software/components/tactics/reductionTactics.ml @@ -30,7 +30,7 @@ open ProofEngineTypes (* Note: this code is almost identical to change_tac and * it could be unified by making the change function a callback *) let reduction_tac ~reduction ~pattern (proof,goal) = - let curi,metasenv,_subst,pbo,pty, attrs = proof in + let curi,metasenv,subst,pbo,pty, attrs = proof in let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in let change subst where terms metasenv ugraph = if terms = [] then where, metasenv, ugraph @@ -51,7 +51,7 @@ let reduction_tac ~reduction ~pattern (proof,goal) = CicMetaSubst.apply_subst subst where', metasenv, ugraph in let (subst,metasenv,ugraph,selected_context,selected_ty) = - ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph + ProofEngineHelpers.select ~subst ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern in let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in @@ -80,7 +80,7 @@ let reduction_tac ~reduction ~pattern (proof,goal) = | _ as t -> t ) metasenv in - (curi,metasenv',_subst,pbo,pty, attrs), [metano] + (curi,metasenv',subst,pbo,pty, attrs), [metano] ;; let simpl_tac ~pattern = @@ -135,7 +135,7 @@ exception NotConvertible term(s) to be replaced. *) let change_tac ?(with_cast=false) ~pattern with_what = let change_tac ~pattern ~with_what (proof, goal) = - let curi,metasenv,_subst,pbo,pty, attrs = proof in + let curi,metasenv,subst,pbo,pty, attrs = proof in let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in let change subst where terms metasenv ugraph = if terms = [] then where, metasenv, ugraph @@ -147,10 +147,12 @@ let change_tac ?(with_cast=false) ~pattern with_what = with_what context_of_t metasenv ugraph in let _,u = - CicTypeChecker.type_of_aux' metasenv context_of_t with_what ugraph + CicTypeChecker.type_of_aux' + metasenv ~subst context_of_t with_what ugraph in let b,_ = - CicReduction.are_convertible ~metasenv context_of_t t with_what u + CicReduction.are_convertible + ~metasenv ~subst context_of_t t with_what u in if b then ((t, with_what) :: pairs), metasenv, ugraph @@ -167,8 +169,9 @@ let change_tac ?(with_cast=false) ~pattern with_what = CicMetaSubst.apply_subst subst where', metasenv, ugraph in let (subst,metasenv,ugraph,selected_context,selected_ty) = - ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture - ~pattern in + ProofEngineHelpers.select + ~metasenv ~subst ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern + in let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in let context', metasenv, ugraph = List.fold_right2 @@ -196,7 +199,7 @@ let change_tac ?(with_cast=false) ~pattern with_what = | _ as t -> t) metasenv in - let proof,goal = (curi,metasenv',_subst,pbo,pty, attrs), metano in + let proof,goal = (curi,metasenv',subst,pbo,pty, attrs), metano in if with_cast then let metano' = ProofEngineHelpers.new_meta_of_proof ~proof in let (newproof,_) = @@ -211,6 +214,7 @@ let change_tac ?(with_cast=false) ~pattern with_what = proof,[goal] in mk_tactic (change_tac ~pattern ~with_what) +;; let fold_tac ~reduction ~term ~pattern = let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status = @@ -225,4 +229,5 @@ let fold_tac ~reduction ~term ~pattern = (change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status in mk_tactic (fold_tac ~reduction ~term ~pattern) +;; diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml index 4a4f150b7..34ecb2d99 100644 --- a/helm/software/components/tactics/tacticals.ml +++ b/helm/software/components/tactics/tacticals.ml @@ -42,7 +42,7 @@ module PET = ProofEngineTypes let id_tac = let id_tac (proof,goal) = - let _, metasenv, _subst, _, _, _ = proof in + let _, metasenv, _, _, _, _ = proof in let _, _, _ = CicUtil.lookup_meta goal metasenv in (proof,[goal]) in @@ -50,7 +50,7 @@ let id_tac = let fail_tac = let fail_tac (proof,goal) = - let _, metasenv, _subst, _ , _, _ = proof in + let _, metasenv, _, _ , _, _ = proof in let _, _, _ = CicUtil.lookup_meta goal metasenv in raise (PET.Fail (lazy "fail tactical")) in @@ -290,8 +290,8 @@ let solve_tactics ~tactics = let progress_tactic ~tactic = let msg = lazy "Failed to progress" in - let progress_tactic (((_,metasenv,_subst,_,_,_),g) as istatus) = - let ((_,metasenv',_subst,_,_,_),opened) as ostatus = + let progress_tactic (((_,metasenv,_,_,_,_),g) as istatus) = + let ((_,metasenv',_,_,_,_),opened) as ostatus = PET.apply_tactic tactic istatus in match opened with diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml index 8b21c7753..1fb1f8de5 100644 --- a/helm/software/components/tactics/tactics.ml +++ b/helm/software/components/tactics/tactics.ml @@ -65,7 +65,6 @@ let rewrite_simpl = EqualityTactics.rewrite_simpl_tac let right = IntroductionTactics.right_tac let ring = Ring.ring_tac let simpl = ReductionTactics.simpl_tac -let solve_rewrite = Auto.solve_rewrite_tac let split = IntroductionTactics.split_tac let symmetry = EqualityTactics.symmetry_tac let transitivity = EqualityTactics.transitivity_tac diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index fa9d4ed8b..ca340f7d1 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Apr 16 11:28:06 CEST 2009 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Apr 23 10:59:57 CEST 2009 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyP : term:Cic.term -> ProofEngineTypes.tactic @@ -98,9 +98,6 @@ val rewrite_simpl : val right : ProofEngineTypes.tactic val ring : ProofEngineTypes.tactic val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic -val solve_rewrite : - params:Auto.auto_params -> - automation_cache:AutomationCache.cache -> unit -> ProofEngineTypes.tactic val split : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic val transitivity : term:Cic.term -> ProofEngineTypes.tactic diff --git a/helm/software/components/tactics/variousTactics.ml b/helm/software/components/tactics/variousTactics.ml index 4652899f0..fd383cf99 100644 --- a/helm/software/components/tactics/variousTactics.ml +++ b/helm/software/components/tactics/variousTactics.ml @@ -38,7 +38,7 @@ let assumption_tac = let module R = CicReduction in let module S = CicSubstitution in let module PT = PrimitiveTactics in - let _,metasenv,_subst,_,_, _ = proof in + let _,metasenv,_,_,_, _ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in let rec find n = function hd::tl -> diff --git a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma index 184166ed9..d9e4e4695 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma @@ -248,8 +248,7 @@ qed. (*** lemmata on well-formedness ***) -lemma fv_WFT : \forall T,x,G.(WFType G T) \to (in_list ? x (fv_type T)) \to - (in_list ? x (fv_env G)). +lemma fv_WFT : \forall T,x,G.(WFType G T) → x ∈ fv_type T → x ∈ fv_env G. intros 4.elim H [simplify in H2;elim (in_list_cons_case ? ? ? ? H2) [rewrite > H3;assumption|elim (not_in_list_nil ? ? H3)] diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma index 5a472e640..c1e909097 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma @@ -22,7 +22,8 @@ intros 3.elim H |apply (SA_Arrow ? ? ? ? ? (H2 H5) (H4 H5)) |apply (SA_All ? ? ? ? ? (H2 H5));intros;apply (H4 ? H6) [intro;apply H6;apply (fv_WFT ? ? ? (WFT_Forall ? ? ? H1 H3)); - simplify;autobatch + simplify; + autobatch; |autobatch]] qed. diff --git a/helm/software/matita/contribs/POPLmark/Fsub/util.ma b/helm/software/matita/contribs/POPLmark/Fsub/util.ma index 3521e87dd..ca2a0e730 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/util.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/util.ma @@ -43,12 +43,13 @@ apply (leb_elim m n) ] qed. +(* notation > "hvbox(x ∈ l)" non associative with precedence 30 for @{ 'inlist $x $l }. notation < "hvbox(x \nbsp ∈ \nbsp l)" non associative with precedence 30 for @{ 'inlist $x $l }. -interpretation "item in list" 'inlist x l = - (cic:/matita/list/in/in_list.ind#xpointer(1/1) _ x l). +*) +interpretation "item in list" 'mem x l = (in_list _ x l). lemma max_case : \forall m,n.(max m n) = match (leb m n) with [ true \Rightarrow n diff --git a/helm/software/matita/library/Q/fraction/ftimes.ma b/helm/software/matita/library/Q/fraction/ftimes.ma index bcc7358b2..aff8a04a6 100644 --- a/helm/software/matita/library/Q/fraction/ftimes.ma +++ b/helm/software/matita/library/Q/fraction/ftimes.ma @@ -122,12 +122,15 @@ elim n ] |generalize in match n4. elim n2 - [cases n6;simplify;autobatch + [cases n6;simplify; + [ exists; [2: autobatch;] + | exists; [2:autobatch;] + ] |cases n7;simplify - [autobatch + [exists;[2:autobatch] |elim (H2 n9). rewrite > H3. simplify. - autobatch + exists;[2:autobatch] ]]]]] qed. \ No newline at end of file diff --git a/helm/software/matita/library/R/r.ma b/helm/software/matita/library/R/r.ma index 46a4e416b..d47a1dc58 100644 --- a/helm/software/matita/library/R/r.ma +++ b/helm/software/matita/library/R/r.ma @@ -58,8 +58,10 @@ axiom assoc_Rtimes : ∀x,y,z:R.(x*y)*z = x*(y*z). axiom Rtimes_x_R1 : ∀x.x * R1 = x. axiom distr_Rtimes_Rplus_l : ∀x,y,z:R.x*(y+z) = x*y + x*z. +pump 200. + lemma distr_Rtimes_Rplus_r : ∀x,y,z:R.(x+y)*z = x*z + y*z. -intros;autobatch paramodulation; +intros; demodulate all. (*autobatch paramodulation;*) qed. (* commutative field *) @@ -201,15 +203,18 @@ intros;autobatch paramodulation; qed. *) lemma Rtimes_x_R0 : ∀x.x * R0 = R0. -intro; +intro; demodulate all. +(* rewrite < Rplus_x_R0 in ⊢ (? ? % ?); rewrite < (Rplus_Ropp (x*R0)) in ⊢ (? ? (? ? %) %); rewrite < assoc_Rplus; apply eq_f2;autobatch paramodulation; +*) qed. lemma eq_Rtimes_Ropp_R1_Ropp : ∀x.x*(-R1) = -x. -intro. +intro. demodulate all. (* +auto paramodulation. rewrite < Rplus_x_R0 in ⊢ (? ? % ?); rewrite < Rplus_x_R0 in ⊢ (? ? ? %); rewrite < (Rplus_Ropp x) in ⊢ (? ? % ?); @@ -219,6 +224,7 @@ rewrite < sym_Rplus in ⊢ (? ? (? ? %) ?); apply eq_f2 [reflexivity] rewrite < Rtimes_x_R1 in ⊢ (? ? (? % ?) ?); rewrite < distr_Rtimes_Rplus_l;autobatch paramodulation; +*) qed. lemma Ropp_inv : ∀x.x = Ropp (Ropp x). @@ -235,24 +241,24 @@ apply eq_Rtimes_l_to_r |apply Rinv_Rtimes_l;assumption] qed. -lemma Ropp_R0 : R0 = - R0. -rewrite < eq_Rtimes_Ropp_R1_Ropp;autobatch paramodulation; +lemma Ropp_R0 : R0 = - R0. demodulate all. (* +rewrite < eq_Rtimes_Ropp_R1_Ropp;autobatch paramodulation; *) qed. lemma distr_Ropp_Rplus : ∀x,y:R.-(x + y) = -x -y. -intros;rewrite < eq_Rtimes_Ropp_R1_Ropp; +intros; demodulate all; (*rewrite < eq_Rtimes_Ropp_R1_Ropp; rewrite > sym_Rtimes;rewrite > distr_Rtimes_Rplus_l; -autobatch paramodulation; +autobatch paramodulation;*) qed. lemma Ropp_Rtimes_l : ∀x,y:R.-(x*y) = -x*y. -intros;rewrite < eq_Rtimes_Ropp_R1_Ropp; -rewrite > sym_Rtimes;rewrite < assoc_Rtimes;autobatch paramodulation; +intros; demodulate all; (*rewrite < eq_Rtimes_Ropp_R1_Ropp; +rewrite > sym_Rtimes;rewrite < assoc_Rtimes;autobatch paramodulation;*) qed. lemma Ropp_Rtimes_r : ∀x,y:R.-(x*y) = x*-y. -intros;rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (???%); -autobatch; +intros; demodulate all; (*rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (???%); +autobatch;*) qed. (* less than *) @@ -284,11 +290,11 @@ qed. lemma pos_z_to_le_Rtimes_Rtimes_to_lt : ∀x,y,z.R0 < z → z*x ≤ z*y → x ≤ y. intros;cases H1 [left;autobatch -|right;rewrite < Rtimes_x_R1;rewrite < Rtimes_x_R1 in ⊢ (???%); +|right; rewrite < Rtimes_x_R1;rewrite < Rtimes_x_R1 in ⊢ (???%); rewrite < sym_Rtimes;rewrite < sym_Rtimes in ⊢ (???%); rewrite < (Rinv_Rtimes_l z) - [rewrite < sym_Rtimes in ⊢ (??(?%?)?);rewrite < sym_Rtimes in ⊢ (???(?%?)); - autobatch paramodulation + [demodulate all; (*rewrite < sym_Rtimes in ⊢ (??(?%?)?);rewrite < sym_Rtimes in ⊢ (???(?%?)); + autobatch paramodulation*) |intro;rewrite > H3 in H;apply (irrefl_Rlt R0);assumption]] qed. @@ -297,7 +303,8 @@ intros;rewrite > Ropp_inv in ⊢ (?%?); rewrite > Ropp_inv in ⊢ (??%); apply Rlt_to_Rlt_Ropp_Ropp;apply (pos_z_to_lt_Rtimes_Rtimes_to_lt ?? (-z)) [rewrite > Ropp_R0;autobatch -|rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (?(??%)?); +|applyS H1; (* + rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (?(??%)?); rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (??(??%)); do 2 rewrite < assoc_Rtimes; rewrite > eq_Rtimes_Ropp_R1_Ropp; @@ -309,7 +316,7 @@ apply Rlt_to_Rlt_Ropp_Ropp;apply (pos_z_to_lt_Rtimes_Rtimes_to_lt ?? (-z)) rewrite > eq_Rtimes_Ropp_R1_Ropp; rewrite < Ropp_inv; rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%); - assumption] + assumption*)] qed. lemma lt_R0_Rinv : ∀x.R0 < x → R0 < Rinv x. @@ -335,27 +342,37 @@ qed. lemma lt_Rinv : ∀x,y.R0 < x → x < y → Rinv y < Rinv x. intros; lapply (Rlt_times_l ? ? (Rinv x * Rinv y) H1) -[rewrite > sym_Rtimes in Hletin;rewrite < assoc_Rtimes in Hletin; +[ lapply (Rinv_Rtimes_l x);[2: intro; destruct H2; autobatch;] + lapply (Rinv_Rtimes_l y);[2: intro; destruct H2; autobatch;] + cut ((x \sup -1/y*x sym_Rtimes in Hletin;rewrite < assoc_Rtimes in Hletin; rewrite > assoc_Rtimes in Hletin:(??%); rewrite > sym_Rtimes in Hletin:(??(??%)); rewrite > Rinv_Rtimes_l in Hletin [rewrite > Rinv_Rtimes_l in Hletin - [rewrite > Rtimes_x_R1 in Hletin;rewrite > sym_Rtimes in Hletin; - rewrite > Rtimes_x_R1 in Hletin;assumption + [applyS Hletin;(*rewrite > Rtimes_x_R1 in Hletin;rewrite > sym_Rtimes in Hletin; + rewrite > Rtimes_x_R1 in Hletin;assumption*) |intro;rewrite > H2 in H1;apply (asym_Rlt ? ? H H1)] - |intro;rewrite > H2 in H;apply (irrefl_Rlt ? H)] + |intro;rewrite > H2 in H;apply (irrefl_Rlt ? H)]*) |apply pos_times_pos_pos;apply lt_R0_Rinv;autobatch] qed. lemma Rlt_plus_l_to_r : ∀a,b,c.a + b < c → a < c - b. -intros;rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b); +intros; lapply (Rlt_plus_l ?? (-b) H); applyS Hletin; +(* +rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b); rewrite < assoc_Rplus; rewrite < sym_Rplus;rewrite < sym_Rplus in ⊢ (??%); apply Rlt_plus_l;assumption; +*) qed. lemma Rlt_plus_r_to_l : ∀a,b,c.a < b + c → a - c < b. -intros;rewrite > Ropp_inv;rewrite > Ropp_inv in ⊢ (??%); +intros; +rewrite > Ropp_inv;rewrite > Ropp_inv in ⊢ (??%); apply Rlt_to_Rlt_Ropp_Ropp;rewrite > distr_Ropp_Rplus; apply Rlt_plus_l_to_r;rewrite < distr_Ropp_Rplus;apply Rlt_to_Rlt_Ropp_Ropp; assumption; diff --git a/helm/software/matita/library/R/root.ma b/helm/software/matita/library/R/root.ma index 574483be7..1205fc92b 100644 --- a/helm/software/matita/library/R/root.ma +++ b/helm/software/matita/library/R/root.ma @@ -109,7 +109,7 @@ letin bound ≝ (λy:R.R0 < y ∧ Rexp_nat y n < x); rewrite < sym_Rplus;apply Rle_minus_r_to_l; apply (pos_z_to_le_Rtimes_Rtimes_to_lt ? ? (n*Rexp_nat a (n-1))) [apply pos_times_pos_pos - [lapply (nat_lt_to_R_lt ?? H1);autobatch + [apply (nat_lt_to_R_lt ?? H1); |elim daemon] |rewrite > Rtimes_x_R0;do 2 rewrite > distr_Rtimes_Rplus_l; rewrite > sym_Rtimes in ⊢ (? ? (? (? ? (? ? (? %))) ?)); @@ -127,14 +127,21 @@ letin bound ≝ (λy:R.R0 < y ∧ Rexp_nat y n < x); rewrite < distr_Rtimes_Rplus_l; apply (trans_Rle ? (Rexp_nat a n - Rexp_nat y n)) [apply Rle_plus_l;left;autobatch - |rewrite > assoc_Rtimes;rewrite > sym_Rtimes in ⊢ (??(??%)); + | cut (∀x,y.(S x ≤ y) = (x < y));[2: intros; reflexivity] + applyS Rexp_nat_tech; + [ unfold lt; change in H1 with (O < n); + autobatch; (*applyS H1;*) + | assumption; + | elim daemon; ]] + (* + rewrite > assoc_Rtimes;rewrite > sym_Rtimes in ⊢ (??(??%)); rewrite < assoc_Rtimes;apply Rexp_nat_tech [autobatch |assumption - |(* by transitivity y^n < x < a^n and injectivity *) elim daemon]] + |(* by transitivity y^n < x < a^n and injectivity *) elim daemon]]*) |intro;apply (irrefl_Rlt (n*Rexp_nat a (n-1))); rewrite > H11 in ⊢ (?%?);apply pos_times_pos_pos - [lapply (nat_lt_to_R_lt ?? H1);autobatch + [apply (nat_lt_to_R_lt ?? H1); |elim daemon]]]] |elim (R_archimedean R1 ((x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1)))) [|autobatch] @@ -155,13 +162,13 @@ letin bound ≝ (λy:R.R0 < y ∧ Rexp_nat y n < x); assumption |apply lt_R0_Rinv;apply pos_times_pos_pos [apply pos_times_pos_pos - [lapply (nat_lt_to_R_lt ?? H1);autobatch + [apply (nat_lt_to_R_lt ?? H1); |elim daemon] |apply (trans_Rlt ???? H8);apply pos_times_pos_pos [apply Rlt_plus_l_to_r;rewrite > sym_Rplus;rewrite > Rplus_x_R0; assumption |apply lt_R0_Rinv;apply pos_times_pos_pos - [lapply (nat_lt_to_R_lt ?? H1);autobatch + [apply (nat_lt_to_R_lt ?? H1); |elim daemon]]]]] |split [(* show that h > R0, also useful in previous parts of the proof *) @@ -366,7 +373,8 @@ qed. lemma root_root_times : ∀x,n,m,H,H1,H2.root m (root n x H H1) H2 ? = root (m*n) x ? H1. [cases (root_sound n x H H1);assumption -|autobatch +| change in match O with (O*O); apply lt_times; assumption; + (* autobatch paramodulation; non fa narrowing, non fa deep subsumption... *) |intros;lapply (Rexp_nat_Rexp_nat_Rtimes (root m (root n x H H1) H2 ?) m n) [cases (root_sound n x H H1);assumption |cases (root_sound m (root n x H H1)) diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma index f72711aaa..1201c4fdf 100644 --- a/helm/software/matita/library/algebra/groups.ma +++ b/helm/software/matita/library/algebra/groups.ma @@ -264,7 +264,7 @@ apply H1; unfold member_of_subgroup; elim H2; apply (ex_intro ? ? (x'·a \sup -1)); -rewrite > f_morph; +rewrite > f_morph; apply (eq_op_x_y_op_z_y_to_eq ? (a \sub H)); rewrite > (op_associative ? G); rewrite < H3; diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma index 3478ef628..b2b21ccd2 100644 --- a/helm/software/matita/library/decidable_kit/decidable.ma +++ b/helm/software/matita/library/decidable_kit/decidable.ma @@ -56,7 +56,7 @@ qed. lemma prove_reflect : ∀P:Prop.∀b:bool. (b = true → P) → (b = false → ¬P) → reflect P b. -intros 2 (P b); cases b; intros; [left|right] autobatch. +intros 2 (P b); cases b; intros; [left|right] [autobatch.|autobatch;] qed. (* ### standard connectives/relations with reflection predicate ### *) @@ -137,7 +137,7 @@ qed. lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m. intros (n m); apply bool_to_eq; split; intros (H); -[1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch type] +[1:cases (b2pT ? ? (orbP ? ?) H); [2: (*autobatch type;*) apply lebW; assumption; ] rewrite > (eqb_true_to_eq ? ? H1); autobatch |2:cases (b2pT ? ? (lebP ? ?) H); [ elim n; [reflexivity|assumption] diff --git a/helm/software/matita/library/demo/cantor.ma b/helm/software/matita/library/demo/cantor.ma index 3294017d7..754ef24b4 100644 --- a/helm/software/matita/library/demo/cantor.ma +++ b/helm/software/matita/library/demo/cantor.ma @@ -34,7 +34,7 @@ definition Z: Ω \sup axs ≝ {x | x ◃ emptyset}. theorem cantor: ∀a:axs. ¬ (Z ⊆ S' a ∧ S' a ⊆ Z). intros 2; cases H; clear H; cut (a ◃ S' a); - [2: constructor 2; [constructor 1 | whd in ⊢ (? ? ? % ?); autobatch]] + [2: constructor 2; [constructor 1 | whd in ⊢ (? ? ? % ?); apply iter; autobatch]] cut (a ◃ emptyset); [2: apply transitivity; [apply (S' a)] [ assumption diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma index 56a8c4120..8e957e8b6 100644 --- a/helm/software/matita/library/demo/formal_topology.ma +++ b/helm/software/matita/library/demo/formal_topology.ma @@ -122,7 +122,7 @@ theorem covers_elim2: simplify in H4 ⊢ %; apply H1; [ apply (C ? a1 j); - | autobatch; + | autobatch; | assumption; | assumption]] qed. diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma index bca5bbf01..8e7483e96 100644 --- a/helm/software/matita/library/demo/power_derivative.ma +++ b/helm/software/matita/library/demo/power_derivative.ma @@ -244,6 +244,7 @@ theorem derivative_power: ∀n:nat. D[X \sup n] = n·X \sup (pred n). (D[X \sup (1+m)] = (1+m) · X \sup m). we need to prove (m · (X \sup (1+ pred m)) = m · X \sup m) (Ppred). + lapply depth=0 le_n; we proved (0 < m ∨ 0=m) (cases). we proceed by induction on cases to prove (m · (X \sup (1+ pred m)) = m · X \sup m). diff --git a/helm/software/matita/library/logic/coimplication.ma b/helm/software/matita/library/logic/coimplication.ma index 67f04b903..44f8d5b8e 100644 --- a/helm/software/matita/library/logic/coimplication.ma +++ b/helm/software/matita/library/logic/coimplication.ma @@ -32,5 +32,5 @@ theorem iff_sym: \forall A,B. A \liff B \to B \liff A. qed. theorem iff_trans: \forall A,B,C. A \liff B \to B \liff C \to A \liff C. - intros. elim H. elim H1. apply iff_intro;intros;autobatch. + intros. elim H. elim H1. apply iff_intro;intros;autobatch depth=3. qed. diff --git a/helm/software/matita/library/logic/connectives2.ma b/helm/software/matita/library/logic/connectives2.ma index a41c691d5..e38223db7 100644 --- a/helm/software/matita/library/logic/connectives2.ma +++ b/helm/software/matita/library/logic/connectives2.ma @@ -37,6 +37,6 @@ theorem transitive_iff: transitive ? iff. elim H1; split; intro; - autobatch. + autobatch depth=3. qed. diff --git a/helm/software/matita/library/nat/div_and_mod.ma b/helm/software/matita/library/nat/div_and_mod.ma index e31f2d678..cbab87206 100644 --- a/helm/software/matita/library/nat/div_and_mod.ma +++ b/helm/software/matita/library/nat/div_and_mod.ma @@ -147,7 +147,7 @@ apply le_plus_n. rewrite < sym_times. rewrite > distr_times_minus. rewrite > plus_minus. -lapply(plus_to_minus ??? H3); demodulate. reflexivity. +lapply(plus_to_minus ??? H3); demodulate all. (* rewrite > sym_times. rewrite < H5. diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma index 92f64e56d..bfdf947b4 100644 --- a/helm/software/matita/library/nat/factorization.ma +++ b/helm/software/matita/library/nat/factorization.ma @@ -61,13 +61,10 @@ cut (\exists i. nth_prime i = smallest_factor n); [ apply (trans_lt ? (S O)); [ unfold lt; apply le_n; | apply lt_SO_smallest_factor; assumption; ] - | letin x \def le.autobatch. - (* - apply divides_smallest_factor_n; - apply (trans_lt ? (S O)); - [ unfold lt; apply le_n; - | assumption; ] *) ] ] - | autobatch. + | apply divides_smallest_factor_n; + autobatch; ] ] + | apply prime_to_nth_prime; + autobatch. (* apply prime_to_nth_prime; apply prime_smallest_factor_n; @@ -156,27 +153,22 @@ apply divides_max_prime_factor_n. assumption.unfold Not. intro. cut (r \mod (nth_prime (max_prime_factor n)) \neq O); - [unfold Not in Hcut1.autobatch. + [ apply Hcut1; autobatch depth=2; (* apply Hcut1.apply divides_to_mod_O; [ apply lt_O_nth_prime_n. | assumption. ] *) - |letin z \def le. - cut(pair nat nat q r=p_ord_aux n n (nth_prime (max_prime_factor n))); - [2: rewrite < H1.assumption.|letin x \def le.autobatch width = 4 depth = 2] - (* CERCA COME MAI le_n non lo applica se lo trova come Const e non Rel *) - ]. -(* - apply (p_ord_aux_to_not_mod_O n n ? q r); + | unfold p_ord in H2; lapply depth=0 le_n; autobatch width = 4 depth = 2; + (*apply (p_ord_aux_to_not_mod_O n n ? q r); [ apply lt_SO_nth_prime_n. | assumption. | apply le_n. | rewrite < H1.assumption. - ] + ]*) ]. -*) + apply (le_to_or_lt_eq (max_prime_factor r) (max_prime_factor n)). apply divides_to_max_prime_factor. assumption.assumption. diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma index 958fddf97..395b24248 100644 --- a/helm/software/matita/library/nat/gcd.ma +++ b/helm/software/matita/library/nat/gcd.ma @@ -758,12 +758,11 @@ cut (n \divides p \lor n \ndivides p) [(* first case *) rewrite > (times_n_SO q).rewrite < H5. rewrite > distr_times_minus. + elim H1. autobatch; + (* rewrite > (sym_times q (a1*p)). rewrite > (assoc_times a1). - elim H1. - pump 39. - applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *). - (* + applyS (witness n ? ? (refl_eq ? ?)). rewrite < (sym_times n).rewrite < assoc_times. rewrite > (sym_times q).rewrite > assoc_times. rewrite < (assoc_times a1).rewrite < (sym_times n). @@ -774,11 +773,12 @@ cut (n \divides p \lor n \ndivides p) |(* second case *) rewrite > (times_n_SO q).rewrite < H5. rewrite > distr_times_minus. + elim H1. autobatch; + (* rewrite > (sym_times q (a1*p)). rewrite > (assoc_times a1). - elim H1.rewrite > H6. - applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *). - (* + rewrite > H6. + applyS (witness n ? ? (refl_eq ? ?)). rewrite < sym_times.rewrite > assoc_times. rewrite < (assoc_times q). rewrite < (sym_times n). @@ -925,7 +925,7 @@ intros.elim H3. rewrite > H4 in H2. elim (divides_times_to_divides ? ? ? H H2) [apply False_ind.apply H1.assumption - |elim H5. + |elim H5. apply (witness ? ? n2). rewrite > sym_times in ⊢ (? ? ? (? % ?)). rewrite > assoc_times. diff --git a/helm/software/matita/library/nat/generic_iter_p.ma b/helm/software/matita/library/nat/generic_iter_p.ma index 28ef391eb..6956b7fab 100644 --- a/helm/software/matita/library/nat/generic_iter_p.ma +++ b/helm/software/matita/library/nat/generic_iter_p.ma @@ -616,7 +616,7 @@ elim n rewrite > H8 [ reflexivity | assumption - | autobatch + | apply andb_true_true; [2: apply H12] ] | apply eqb_false_to_not_eq. generalize in match H14. @@ -915,8 +915,8 @@ cut (O < p) rewrite < exp_plus_times. apply eq_f. rewrite > sym_plus. - apply plus_minus_m_m. - autobatch + apply plus_minus_m_m. + autobatch; ] ] |intros. @@ -941,8 +941,8 @@ cut (O < p) [apply le_S_S_to_le. change with ((i/S m) < S n). apply (lt_times_to_lt_l m). - apply (le_to_lt_to_lt ? i) - [autobatch|assumption] + apply (le_to_lt_to_lt ? i);[2:assumption] + apply eq_plus_to_le;[2:autobatch] |apply le_exp [assumption |apply le_S_S_to_le. diff --git a/helm/software/matita/library/nat/map_iter_p.ma b/helm/software/matita/library/nat/map_iter_p.ma index ff48d4d06..7550d89b2 100644 --- a/helm/software/matita/library/nat/map_iter_p.ma +++ b/helm/software/matita/library/nat/map_iter_p.ma @@ -267,7 +267,7 @@ elim k 3 apply le_S. assumption ] - |apply H2[autobatch|apply le_n] + |apply H2[autobatch |apply le_n] ] ] ] @@ -325,13 +325,13 @@ apply (nat_case n) apply lt_to_not_eq. apply (le_to_lt_to_lt ? m) [apply (trans_le ? (m-k)) - [assumption|autobatch] + [assumption| autobatch] |apply le_S.apply le_n ] ] |apply not_eq_to_eqb_false. apply lt_to_not_eq. - unfold.autobatch + unfold. autobatch; ] ] |apply le_S_S_to_le.assumption @@ -362,7 +362,7 @@ elim n 2 ] |apply sym_eq. apply plus_to_minus. - autobatch. + autobatch; ] |intros. cut ((S n1) \neq k1) diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma index 92324aae7..a8e987fc4 100644 --- a/helm/software/matita/library/nat/minus.ma +++ b/helm/software/matita/library/nat/minus.ma @@ -235,7 +235,8 @@ theorem lt_minus_l: \forall m,l,n:nat. apply nat_elim2 [intros.apply False_ind.apply (not_le_Sn_O ? H) |intros.rewrite < minus_n_O. - autobatch + change in H1 with (n eq_minus_S_pred. apply lt_pred [unfold lt.apply le_plus_to_minus_r.applyS H1 - |apply H[autobatch|assumption] + |apply H[autobatch depth=2|assumption] ] ] qed. @@ -291,18 +292,21 @@ qed. theorem lt_O_minus_to_lt: \forall a,b:nat. O \lt b-a \to a \lt b. -intros. +intros. applyS (lt_minus_to_plus O a b). assumption; +(* rewrite > (plus_n_O a). rewrite > (sym_plus a O). apply (lt_minus_to_plus O a b). assumption. +*) qed. theorem lt_minus_to_lt_plus: \forall n,m,p. n - m < p \to n < m + p. intros 2. apply (nat_elim2 ? ? ? ? n m) - [simplify.intros.autobatch. + [simplify.intros. + lapply depth=0 le_n; autobatch; |intros 2.rewrite < minus_n_O. intro.assumption |intros. @@ -336,7 +340,7 @@ theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n). intros. apply sym_eq. apply plus_to_minus. -autobatch. +autobatch; qed. theorem distributive_times_minus: distributive nat times minus. @@ -395,7 +399,7 @@ qed. theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to p+(n-m) = n-(m-p). -intros. +intros. apply sym_eq. apply plus_to_minus. rewrite < assoc_plus. diff --git a/helm/software/matita/library/nat/times.ma b/helm/software/matita/library/nat/times.ma index 8de22c1e3..f59622218 100644 --- a/helm/software/matita/library/nat/times.ma +++ b/helm/software/matita/library/nat/times.ma @@ -1,3 +1,4 @@ + (**************************************************************************) (* __ *) (* ||M|| *) @@ -37,7 +38,7 @@ theorem times_n_Sm : intros.elim n. simplify.reflexivity. simplify. -demodulate all steps=3. +demodulate all. (* apply eq_f.rewrite < H. transitivity ((n1+m)+n1*m).symmetry.apply assoc_plus. @@ -112,7 +113,7 @@ unfold distributive. intros.elim x. simplify.reflexivity. simplify. -demodulate all steps=16. +demodulate all. (* rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus. apply eq_f.rewrite < assoc_plus. rewrite < (sym_plus ? z). @@ -127,7 +128,7 @@ unfold associative. intros. elim x. simplify.apply refl_eq. simplify. -demodulate all steps=4. +demodulate all. (* rewrite < sym_times. rewrite > distr_times_plus. -- 2.39.2