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 b6930bf0df234357e2a4e5f51e673d892726e204..21051e12d5e87922f4489dcd6062a7921d6d5f0c 100644 (file)
--- 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 1b172786a7a44a071f28079c8dbdf409a8c996ec..ce4b9357e389da2588ae4b7932b681c1a0cb2c6d 100644 (file)
--- 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 79e627409ed5794f451f23b40c13316bde7e3379..0cc52ac1ab523a8cd7464619dde45d143709a8a4 100644 (file)
--- 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 0c98946802bb3cf19dd95c5b8ba0f510af664dd4..cdddc6595fa7fa01b68546776607e71ba2a801b1 100644 (file)
--- 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 63d64bebc48d1cd7575e499e5cc15430707fb0c0..42ae9682532ce8f65811f23944ec7e0f2a83cf0c 100644 (file)
--- 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 fbf51276189b1524bb8418eb0f611606cd5f5f54..e31f2d678cd739a075e5e33b5847998157f5d4fc 100644 (file)
--- 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 20785c9e88e87c49b8aa386dd59d8947ef3fbe4e..92324aae7610481c69fdc15a3fef5e5da8db0fb2 100644 (file)
--- 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 87edf468bc958e990d337271656bfaac181756b9..8de22c1e3c1d4c4c7867cbe24c08b4c6575ef006 100644 (file)
--- 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.