From: Enrico Tassi Date: Wed, 22 Apr 2009 10:30:55 +0000 (+0000) Subject: demodulate takes an extra argument 'all', if present it attempts to solve X-Git-Tag: make_still_working~4064 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5c10d402b5de7233bc83d7f685b274832e383212;p=helm.git demodulate takes an extra argument 'all', if present it attempts to solve the goal demodulating it in any possible way. an extra steps argument may be used to increase the default maximum number of demodulation steps (1). pump may also affect the result. --- diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index b6930bf0d..21051e12d 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -417,6 +417,8 @@ EXTEND | IDENT "timeout" | IDENT "library" | IDENT "type" + | IDENT "steps" + | IDENT "all" ] ]; auto_params: [ diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 1b172786a..ce4b9357e 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -1725,14 +1725,15 @@ let eq_of_goal = function (* performs steps of rewrite with the universe, obtaining if possible * a trivial goal *) -let solve_rewrite_tac ~automation_cache ~params:(univ,params) (proof,goal as status)= +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:false + init_cache_and_tables ~use_library:false ~use_context automation_cache univ (proof,goal) in let actives, passives, bag = tables in - let _,metasenv,_subst,_,_,_ = proof 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 @@ -1753,6 +1754,11 @@ let solve_rewrite_tac ~automation_cache ~params:(univ,params) (proof,goal as sta 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 -> @@ -1944,9 +1950,13 @@ let demodulate_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)= Equality.build_goal_proof (~contextualize:false) bag eq_uri newproof opengoal ty [] context metasenv in - let extended_metasenv = (maxm,context,newty)::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,extended_metasenv,_subst,pbo,pty, attrs),goal in + (curi,metasenv,_subst,pbo,pty, attrs),goal in let (status,newgoals) = ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac ~term:proofterm) @@ -1963,6 +1973,14 @@ let demodulate_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)= 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/declarative.ml b/helm/software/components/tactics/declarative.ml index 79e627409..0cc52ac1a 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -196,7 +196,8 @@ 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"]) () + Tactics.solve_rewrite ~automation_cache + ~params:([term],["steps","1"; "use_context","false"]) () | `Proof -> Tacticals.id_tac in diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 0c9894680..cdddc6595 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -1080,7 +1080,7 @@ let build_newg bag context goal rule expansion = ;; let rec demod bag env table goal = - let goalproof,menv,t = goal in + let _,menv,t = goal in let _, context, ugraph = env in let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in match res with @@ -1294,7 +1294,7 @@ let solve_demodulating bag env table initgoal steps = when LibraryObjects.is_eq_URI uri -> (try let _ = - Founif.unification m m context left right CicUniv.empty_ugraph + Founif.unification [] m context left right CicUniv.empty_ugraph in Yes newg with CicUnification.UnificationFailure _ -> No [newg]) @@ -1307,43 +1307,47 @@ let solve_demodulating bag env table initgoal steps = with Not_found -> No (List.flatten (List.map (function No s -> s | _-> assert false) newg)) in - let rec first f l = + let rec first f acc l = match l with - | [] -> None + | [] -> acc,None | x::tl -> - match f x with - | None -> first f tl - | Some x as ok -> ok + match f acc x with + | acc,None -> first f acc tl + | acc,Some x as ok -> ok in - let rec aux steps next goal = - if steps = 0 then None else + 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 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) newgoals with - | Some g as success -> success - | None -> aux steps R goal) - | Yes newgoal -> Some newgoal) - | [] -> aux steps R goal) + (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) newgoals with - | Some g as success -> success - | None -> None) - | Yes newgoal -> Some newgoal) - | [] -> None) + (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) in - aux steps L initgoal + let _, res = aux steps L [] initgoal in + res ;; let get_stats () = "" ;; diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma index 63d64bebc..42ae96825 100644 --- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma +++ b/helm/software/matita/library/demo/propositional_sequent_calculus.ma @@ -244,11 +244,20 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F). lapply (H4 i); clear H4; rewrite > symm_orb in ⊢ (? ? (? ? %) ?); rewrite > distributive_orb_andb; - autobatch paramodulation by distributive_orb_andb,symm_orb,symm_orb, Hletin, Hletin1,andb_true. + demodulate. + reflexivity. + (* + autobatch paramodulation + by distributive_orb_andb,symm_orb,symm_orb, + Hletin, Hletin1,andb_true. + *) | simplify in H2 ⊢ %; intros; lapply (H2 i); clear H2; - autobatch paramodulation by andb_assoc, Hletin. + pump 100. pump 100. + demodulate. + reflexivity. + (* autobatch paramodulation by andb_assoc, Hletin. *) | simplify in H2 H4 ⊢ %; intros; lapply (H2 i); clear H2; @@ -258,7 +267,9 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F). rewrite > demorgan2; rewrite > symm_orb; rewrite > distributive_orb_andb; - autobatch paramodulation by symm_andb,symm_orb,andb_true,Hletin,Hletin1. + demodulate. + reflexivity. + (* autobatch paramodulation by symm_andb,symm_orb,andb_true,Hletin,Hletin1. *) | simplify in H2 ⊢ %; intros; lapply (H2 i); clear H2; diff --git a/helm/software/matita/library/nat/div_and_mod.ma b/helm/software/matita/library/nat/div_and_mod.ma index fbf512761..e31f2d678 100644 --- a/helm/software/matita/library/nat/div_and_mod.ma +++ b/helm/software/matita/library/nat/div_and_mod.ma @@ -147,11 +147,14 @@ apply le_plus_n. rewrite < sym_times. rewrite > distr_times_minus. rewrite > plus_minus. +lapply(plus_to_minus ??? H3); demodulate. reflexivity. +(* rewrite > sym_times. rewrite < H5. rewrite < sym_times. apply plus_to_minus. apply H3. +*) apply le_times_r. apply lt_to_le. apply H6. @@ -195,8 +198,8 @@ qed. theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O. intros.constructor 1. -unfold lt.apply le_S_S.apply le_O_n. -rewrite < plus_n_O.rewrite < sym_times.reflexivity. +unfold lt.apply le_S_S.apply le_O_n. demodulate. reflexivity. +(*rewrite < plus_n_O.rewrite < sym_times.reflexivity.*) qed. lemma div_plus_times: \forall m,q,r:nat. r < m \to (q*m+r)/ m = q. @@ -243,8 +246,8 @@ theorem div_n_n: \forall n:nat. O < n \to n / n = S O. intros. apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O). apply div_mod_spec_div_mod.assumption. -constructor 1.assumption. -rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity. +constructor 1.assumption. demodulate. reflexivity. (* +rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.*) qed. theorem eq_div_O: \forall n,m. n < m \to n / m = O. @@ -260,8 +263,8 @@ theorem mod_n_n: \forall n:nat. O < n \to n \mod n = O. intros. apply (div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O). apply div_mod_spec_div_mod.assumption. -constructor 1.assumption. -rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity. +constructor 1.assumption. demodulate. reflexivity.(* +rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.*) qed. theorem mod_S: \forall n,m:nat. O < m \to S (n \mod m) < m \to diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma index 20785c9e8..92324aae7 100644 --- a/helm/software/matita/library/nat/minus.ma +++ b/helm/software/matita/library/nat/minus.ma @@ -267,10 +267,16 @@ qed. lemma lt_to_lt_O_minus : \forall m,n. n < m \to O < m - n. intros. -unfold. apply le_plus_to_minus_r. unfold in H. rewrite > sym_plus. +unfold. apply le_plus_to_minus_r. unfold in H. +cut ((S n ≤ m) = (1 + n ≤ m)) as applyS; + [ rewrite < applyS; assumption; + | demodulate; reflexivity. ] +(* +rewrite > sym_plus. rewrite < plus_n_Sm. rewrite < plus_n_O. assumption. +*) qed. theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p). @@ -357,10 +363,13 @@ theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p theorem eq_minus_plus_plus_minus: \forall n,m,p:nat. p \le m \to (n+m)-p = n+(m-p). intros. apply plus_to_minus. +lapply (plus_minus_m_m ?? H); demodulate. reflexivity. +(* rewrite > sym_plus in \vdash (? ? ? %). rewrite > assoc_plus. rewrite < plus_minus_m_m. reflexivity.assumption. +*) qed. theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p). diff --git a/helm/software/matita/library/nat/times.ma b/helm/software/matita/library/nat/times.ma index 87edf468b..8de22c1e3 100644 --- a/helm/software/matita/library/nat/times.ma +++ b/helm/software/matita/library/nat/times.ma @@ -36,13 +36,17 @@ theorem times_n_Sm : \forall n,m:nat. n+(n*m) = n*(S m). intros.elim n. simplify.reflexivity. -simplify.apply eq_f.rewrite < H. +simplify. +demodulate all steps=3. +(* +apply eq_f.rewrite < H. transitivity ((n1+m)+n1*m).symmetry.apply assoc_plus. transitivity ((m+n1)+n1*m). apply eq_f2. apply sym_plus. reflexivity. apply assoc_plus. +*) qed. theorem times_O_to_O: \forall n,m:nat.n*m = O \to n = O \lor m= O. @@ -56,11 +60,11 @@ apply nat_elim2;intros qed. theorem times_n_SO : \forall n:nat. n = n * S O. -intros. +intros. demodulate. reflexivity. (* rewrite < times_n_Sm. rewrite < times_n_O. rewrite < plus_n_O. -reflexivity. +reflexivity.*) qed. theorem times_SSO_n : \forall n:nat. n + n = S (S O) * n. @@ -93,10 +97,11 @@ qed. theorem symmetric_times : symmetric nat times. unfold symmetric. -intros.elim x. -simplify.apply times_n_O. +intros.elim x; + [ simplify. apply times_n_O. + | demodulate. reflexivity. (* (* applyS times_n_Sm. *) -simplify.rewrite > H.apply times_n_Sm. +simplify.rewrite > H.apply times_n_Sm.*)] qed. variant sym_times : \forall n,m:nat. n*m = m*n \def @@ -106,9 +111,12 @@ theorem distributive_times_plus : distributive nat times plus. unfold distributive. intros.elim x. simplify.reflexivity. -simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus. +simplify. +demodulate all steps=16. +(* +rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus. apply eq_f.rewrite < assoc_plus. rewrite < (sym_plus ? z). -rewrite > assoc_plus.reflexivity. +rewrite > assoc_plus.reflexivity. *) qed. variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p @@ -118,11 +126,15 @@ theorem associative_times: associative nat times. unfold associative. intros. elim x. simplify.apply refl_eq. -simplify.rewrite < sym_times. +simplify. +demodulate all steps=4. +(* +rewrite < sym_times. rewrite > distr_times_plus. rewrite < sym_times. rewrite < (sym_times (times n y) z). rewrite < H.apply refl_eq. +*) qed. variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def @@ -130,7 +142,7 @@ associative_times. lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z). intros. -demodulate. reflexivity; +demodulate. reflexivity. (* autobatch paramodulation. *) qed.