Changed Tauto so it displays less 'Unfold not iff'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3706 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 51 insertions, 43 deletions

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index d57b4c2ac5..d568084401 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -21,49 +21,55 @@ open Tacticals
 open Tacinterp
 open Tactics
 open Util
-
+   
 let is_empty ist =
   if (is_empty_type (List.assoc 1 ist.lmatch)) then
     <:tactic<ElimType ?1;Assumption>>
-  else
-    <:tactic<Fail>>
-
+ else
+   <:tactic<Fail>>
+   
 let is_unit ist =
   if (is_unit_type (List.assoc 1 ist.lmatch)) then
     <:tactic<Idtac>>
   else
     <:tactic<Fail>>
-
+    
 let is_conj ist =
   let ind=(List.assoc 1 ist.lmatch) in
-  if (is_conjunction ind) && (is_nodep_ind ind) then
-     <:tactic<Idtac>>
-  else
-    <:tactic<Fail>>
+    if (is_conjunction ind) && (is_nodep_ind ind) then
+      <:tactic<Idtac>>
+    else
+      <:tactic<Fail>>
 
 let is_disj ist =
   if (is_disjunction (List.assoc 1 ist.lmatch)) then
-     <:tactic<Idtac>>
+    <:tactic<Idtac>>
   else
     <:tactic<Fail>>
 
 let not_dep_intros ist =
   <:tactic<
-    Repeat
-      Match Context With
-      | [|- ?1 -> ?2 ] -> Intro>>
-
+  Repeat
+    Match Context With
+| [|- ?1 -> ?2 ] -> Intro
+| [|- (iff ? ?)] -> Unfold iff
+| [|- (not ?)] -> Unfold not
+| [ H:(iff ? ?)|- ?] -> Unfold iff in H
+| [ H:(not ?)|-?] -> Unfold not in H
+| [ H:(iff ? ?)->?|- ?] -> Unfold iff in H
+| [ H:(not ?)->?|-?] -> Unfold not in H >>
+				      
 let axioms ist =
   let t_is_unit = tacticIn is_unit
   and t_is_empty = tacticIn is_empty in
-  <:tactic<
+    <:tactic<
     Match Reverse Context With
-    |[|- ?1] -> $t_is_unit;Constructor 1
-    |[_:?1 |- ?] -> $t_is_empty
-    |[_:?1 |- ?1] -> Assumption>>
+      |[|- ?1] -> $t_is_unit;Constructor 1
+      |[_:?1 |- ?] -> $t_is_empty
+      |[_:?1 |- ?1] -> Assumption>>
 
 
-let simplif t_reduce ist =
+let simplif ist =
   let t_is_unit = tacticIn is_unit
   and t_is_conj = tacticIn is_conj
   and t_is_disj = tacticIn is_disj
@@ -73,8 +79,8 @@ let simplif t_reduce ist =
     Repeat
       ((Match Reverse Context With
         | [id: (?1 ? ?) |- ?] ->
-            $t_is_conj;Elim id;Do 2 Intro;Clear id;$t_reduce
-        | [id: (?1 ? ?) |- ?] -> $t_is_disj;Elim id;Intro;Clear id;$t_reduce
+            $t_is_conj;Elim id;Do 2 Intro;Clear id
+        | [id: (?1 ? ?) |- ?] -> $t_is_disj;Elim id;Intro;Clear id
         | [id0: ?1-> ?2; id1: ?1|- ?] -> Generalize (id0 id1);Intro;Clear id0
         | [id: ?1 -> ?2|- ?] ->
           $t_is_unit;Cut ?2;
@@ -84,7 +90,7 @@ let simplif t_reduce ist =
 	    ]
         | [id: (?1 ?2 ?3) -> ?4|- ?] ->
           $t_is_conj;Cut ?2-> ?3-> ?4;
-	    [Intro;Clear id;$t_reduce
+	    [Intro;Clear id
 	    | (* id: (?1 ?2 ?3) -> ?4 |- ?2 -> ?3 -> ?4 *)
 	      Intro;Intro; Cut (?1 ?2 ?3);[Exact id|Split;Assumption]
 	    ]
@@ -92,23 +98,22 @@ let simplif t_reduce ist =
           $t_is_disj;
 	    Cut ?3-> ?4;
 	      [Cut ?2-> ?4;
-	        [Intro;Intro;Clear id;$t_reduce
+	        [Intro;Intro;Clear id
 		| (* id: (?1 ?2 ?3) -> ?4 |- ?2 -> ?4 *)
 		  Intro; Cut (?1 ?2 ?3);[Exact id|Left;Assumption]
 		]
 	      | (* id: (?1 ?2 ?3) -> ?4 |- ?3 -> ?4 *)
 		Intro; Cut (?1 ?2 ?3);[Exact id|Right;Assumption]
 	      ]
-        | [|- (?1 ? ?)] -> $t_is_conj;Split;$t_reduce);
+        | [|- (?1 ? ?)] -> $t_is_conj;Split);
        $t_not_dep_intros)>>
 
 let rec tauto_intuit t_reduce t_solver ist =
   let t_axioms = tacticIn axioms
-  and t_simplif = tacticIn (simplif t_reduce)
+  and t_simplif = tacticIn simplif
   and t_is_disj = tacticIn is_disj
   and t_tauto_intuit = tacticIn (tauto_intuit t_reduce t_solver) in
   <:tactic<
-   $t_reduce;
    ($t_simplif;$t_axioms
     Orelse
       (Match Reverse Context With
@@ -119,28 +124,37 @@ let rec tauto_intuit t_reduce t_solver ist =
 	       [Exact id|Generalize [y:?2](id [x:?1]y);Intro;Clear id]
 	    ]; Solve [ $t_tauto_intuit ]
       | [|- (?1 ? ?)] ->
-        $t_is_disj;Solve [Left;$t_tauto_intuit | Right;$t_tauto_intuit]
+          $t_is_disj;Solve [Left;$t_tauto_intuit | Right;$t_tauto_intuit]
       )
     Orelse
-      (* NB: [|- ? -> ?] matches any product *)
-      (Match Context With |[ |- ? -> ? ] -> Intro;$t_tauto_intuit)
+    (* NB: [|- ? -> ?] matches any product *)
+    (Match Context With |[ |- ? -> ? ] -> Intro;$t_tauto_intuit
+    |[|-?]->$t_reduce;$t_solver)
     Orelse
-      $t_solver
+    $t_solver
    ) >>
+    
+    (*
+      let unfold_not_iff = function
+      | None -> interp <:tactic<Unfold not iff>>
+      | Some id -> let id = (dummy_loc,id) in interp <:tactic<Unfold not iff in $id>>
+      
+      let reduction_not_iff =
+      Tacticals.onAllClauses (fun ido -> unfold_not_iff ido)
+    *)
+    
+let reduction_not_iff=interp
+ <:tactic<Repeat (Match Context With 
+		 |[|- ?]->Progress Unfold not iff 
+		 |[H:?|- ?]->Progress Unfold not iff in H)>>
 
-let unfold_not_iff = function
-  | None -> interp <:tactic<Unfold not iff>>
-  | Some id -> let id = (dummy_loc,id) in interp <:tactic<Unfold not iff in $id>>
-
-let reduction_not_iff =
-  Tacticals.onAllClauses (fun ido -> unfold_not_iff ido)
 
 let t_reduction_not_iff = Tacexpr.TacArg (valueIn (VTactic reduction_not_iff))
 
 let intuition_gen tac =
   interp (tacticIn (tauto_intuit t_reduction_not_iff tac))
 
-let simplif_gen = interp (tacticIn (simplif t_reduction_not_iff))
+let simplif_gen = interp (tacticIn simplif)
 
 let tauto g =
   try intuition_gen <:tactic<Fail>> g
@@ -185,9 +199,3 @@ TACTIC EXTEND LinearIntuition
 | [ "LinearIntuition" ] -> [ lfo_wrap (-1)]
 | [ "LinearIntuition" integer(n)] -> [ lfo_wrap n]
 END
-
-TACTIC EXTEND Test
-| [ "Test" ] -> [ reduction_not_iff ]
-END
-
-let default =interp <:tactic<Test>>