Intuition ne fait plus de Unfold des constantes (il faut les faire

soi-même si nécessaire) : l'idée est d'avoir un comportement clair et
toujours aussi rapide que possible.


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

3 files changed, 21 insertions, 78 deletions

diff --git a/tactics/Tauto.v b/tactics/Tauto.v
index d4fafc277f..e03f896852 100644
--- a/tactics/Tauto.v
+++ b/tactics/Tauto.v
@@ -14,17 +14,9 @@ Grammar tactic simple_tactic: ast :=
   tauto [ "Tauto" ] -> [(Tauto)]
 | intuition [ "Intuition" ] -> [(Intuition)]
 | intuition_t [ "Intuition" tactic($t) ] -> [(Intuition (TACTIC $t))]
-(*
-| intuitionnr [ "Intuitionnr"] -> [(Intuitionnr)]
-| intuitionr [ "Intuitionr"] -> [(Intuitionr)]
-| intuitionnr_t [ "Intuitionnr" tactic($t) ] -> [(Intuitionnr (TACTIC $t))]
-| intuitionr_t [ "Intuitionr" tactic($t) ] -> [(Intuitionr (TACTIC $t))]
-| intsimplif [ "IntSimplif" ] -> [(IntSimplif)]
-| intreduce [ "IntReduce" ] -> [(IntReduce)]
-*)
 .
 
 Syntax tactic level 0:
   tauto [(Tauto)] -> ["Tauto"]
 | intuition [(Intuition)] -> ["Intuition"]
-| intuition_t [<<(Intuition $t)>>] -> ["Intuition" $t].
+| intuition_t [<<(Intuition (TACTIC $t))>>] -> ["Intuition " $t].
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index cfe768acb7..d6e6372acb 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -111,8 +111,6 @@ let rec tauto_intuit t_reduce t_solver ist =
 
 let tauto_main t_reduce ist =
   tauto_intuit t_reduce <:tactic< Failtac >> ist
-let intuition_main t_reduce ist =
-  tauto_intuit t_reduce <:tactic< Auto with * >> ist
 
 let unfold_not_iff = function
   | None -> interp <:tactic<Unfold not iff>>
@@ -122,8 +120,6 @@ let unfold_not_iff = function
 
 let reduction_not_iff = Tacticals.onAllClauses (fun ido -> unfold_not_iff ido)
 
-let no_reduction = tclIDTAC
-
 (* Reduce until finding atoms in head normal form *)
 open Term
 open Termops
@@ -140,54 +136,21 @@ let reduction =
   Tacticals.onAllClauses
     (fun cl -> reduct_option reduce (option_app (fun id -> InHyp id) cl))
 
-let t_no_reduction = valueIn (VTactic no_reduction)
 let t_reduction = valueIn (VTactic reduction)
 let t_reduction_not_iff = valueIn (VTactic reduction_not_iff)
 
 (* As a simple heuristic, first we try to avoid reduction both in tauto and
    intuition *)
-
 let tauto g =
   try
-    (* (tclTHEN init_intros *)
-      (tclORELSE
+(*      (tclORELSE *)
         (interp (tacticIn (tauto_main t_reduction_not_iff)))
-        (interp (tacticIn (tauto_main t_reduction))))
-    (* ) *)
+(*        (interp (tacticIn (tauto_main t_reduction)))) *)
     g
   with UserError _ -> errorlabstrm "tauto" [< str "Tauto failed" >]
-(*
-let intuition =
-  (*  tclTHEN init_intros*)
-    (tclORELSE
-      (interp (tacticIn (intuition_main t_reduction_not_iff)))
-      (interp (tacticIn (intuition_main t_reduction))))
-*)
-
-let intuition_not_reducing tac =
-  interp (tacticIn (tauto_intuit t_no_reduction tac))
-
-let intuition_reducing tac =
-  interp (tacticIn (tauto_intuit t_reduction tac))
 
-let intuition_reducing_not_iff tac =
-  interp (tacticIn (tauto_intuit t_reduction_not_iff tac))
-
-(* Idea: we want to destructure the goal and the hyps but we do not
-   want to unfold constants unless we can solve the obtained goals.
-   Moreover, we need to unfold "not" and "iff" in order to solve all
-   propositionnal tautologies but we should do it only if necessary;
-   otherwise, if tac=Auto, it may fail to recognize that a given goal
-   is an instance of one of its Hints *)
 let intuition_gen tac =
-  let tnored = tclSOLVE [ intuition_not_reducing tac ]
-  and tr = tclTRY (tclSOLVE [ intuition_reducing tac ])
-  and trnotiff = intuition_reducing_not_iff tac in
-  tclORELSE tnored
-    (tclORELSE
-       (tclTHEN trnotiff tr)
-       tr
-    )
+  interp (tacticIn (tauto_intuit t_reduction_not_iff tac))
 
 let v_intuition args =
   match args with
@@ -195,26 +158,7 @@ let v_intuition args =
     | [ Tac(_, t)] -> intuition_gen t
     | _ -> assert false
 
-let v_intuitnred args =
-  match args with
-    | [] -> intuition_not_reducing <:tactic< Auto with * >>
-    | [ Tac(_, t)] -> intuition_not_reducing t
-    | _ -> assert false
-
-let v_intuitred args =
-  match args with
-    | [] -> intuition_reducing <:tactic< Auto with * >>
-    | [ Tac(_, t)] -> intuition_reducing t
-    | _ -> assert false
-
-let _ = hide_atomic_tactic "IntSimplif" (interp (tacticIn (simplif t_reduction_not_iff)))
-let _ = hide_atomic_tactic "IntReduce" (interp (tacticIn (simplif t_reduction_not_iff)))
-
 let _ = hide_atomic_tactic "Tauto" tauto
 (* let _ = hide_atomic_tactic "Intuition" intuition*)
 let _ = hide_tactic "Intuition" v_intuition
 
-let _ = hide_tactic "Intuitionr" v_intuitred
-let _ = hide_tactic "Intuitionnr" v_intuitnred
-
-
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index c1f0feb9ad..ca1853405d 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -70,7 +70,7 @@ Hints Resolve imp_not_Req : real.
 
 (**********)
 Lemma Req_EM:(r1,r2:R)(r1==r2)\/``r1<>r2``.
-Intros ; Generalize (total_order_T r1 r2) ; Intuition EAuto with real.
+Intros ; Generalize (total_order_T r1 r2) imp_not_Req ; Intuition EAuto 3. 
 Save.
 Hints Resolve Req_EM : real.
 
@@ -91,7 +91,7 @@ Save.
 
 (**********)
 Lemma Rlt_le:(r1,r2:R)``r1<r2``-> ``r1<=r2``.
-Intuition Auto.
+Intros ; Red ; Tauto.
 Save.
 Hints Resolve Rlt_le : real.
 
@@ -107,14 +107,15 @@ Save.
 
 (**********)
 Lemma not_Rle:(r1,r2:R)~(``r1<=r2``)->``r1>r2``.
-Intros r1 r2 ; Generalize (total_order r1 r2) ; Tauto.
+Intros r1 r2 ; Generalize (total_order r1 r2) ; Unfold Rle; Tauto.
 Save.
 
 Hints Immediate Rle_ge Rge_le not_Rle : real.
 
 (**********)
 Lemma Rlt_le_not:(r1,r2:R)``r2<r1``->~(``r1<=r2``).
-Intros r1 r2 ; Generalize (Rlt_antisym r1 r2) (imp_not_Req r1 r2) ; Intuition.
+Generalize Rlt_antisym imp_not_Req ; Unfold Rle.
+Intuition EAuto 3.
 Save.
 
 Lemma Rle_not:(r1,r2:R)``r1>r2`` -> ~(``r1<=r2``).
@@ -123,12 +124,13 @@ Proof Rlt_le_not.
 Hints Immediate Rlt_le_not : real.
 
 Lemma Rle_not_lt: (r1, r2:R) ``r2 <= r1`` ->~ (``r1<r2``).
-Intros r1 r2. Generalize (Rlt_antisym r1 r2) (imp_not_Req r1 r2); Intuition.
+Intros r1 r2. Generalize (Rlt_antisym r1 r2) (imp_not_Req r1 r2).
+Unfold Rle; Intuition.
 Save.
 
 (**********)
 Lemma Rlt_ge_not:(r1,r2:R)``r1<r2``->~(``r1>=r2``).
-Generalize Rlt_le_not. Intuition EAuto 3.
+Generalize Rlt_le_not. Unfold Rle Rge. Intuition EAuto 3.
 Save.
 
 Hints Immediate Rlt_ge_not : real.
@@ -155,7 +157,7 @@ Save.
 Hints Immediate eq_Rge_sym : real.
 
 Lemma Rle_antisym : (r1,r2:R)``r1<=r2`` -> ``r2<=r1``-> r1==r2.
-Intros r1 r2; Generalize (Rlt_antisym r1 r2) ; Intuition.
+Intros r1 r2; Generalize (Rlt_antisym r1 r2) ; Unfold Rle ; Intuition.
 Save.
 Hints Resolve Rle_antisym : real.
 
@@ -171,17 +173,20 @@ Save.
 (**********)
 Lemma Rle_trans:(r1,r2,r3:R) ``r1<=r2``->``r2<=r3``->``r1<=r3``.
 Generalize trans_eqT Rlt_trans Rlt_rew.
+Unfold Rle.
 Intuition EAuto 2.
 Save.
 
 (**********)
 Lemma Rle_lt_trans:(r1,r2,r3:R)``r1<=r2``->``r2<r3``->``r1<r3``.
-Generalize Rlt_trans Rlt_rew. Intuition EAuto 2.
+Generalize Rlt_trans Rlt_rew. 
+Unfold Rle.
+Intuition EAuto 2.
 Save.
 
 (**********)
 Lemma Rlt_le_trans:(r1,r2,r3:R)``r1<r2``->``r2<=r3``->``r1<r3``.
-Generalize Rlt_trans Rlt_rew; Intuition EAuto 2.
+Generalize Rlt_trans Rlt_rew; Unfold Rle; Intuition EAuto 2.
 Save.
 
 
@@ -192,7 +197,9 @@ Save.
 
 (**********)
 Lemma total_order_Rle:(r1,r2:R)(sumboolT ``r1<=r2`` ~(``r1<=r2``)).
-Intros r1 r2; Generalize (total_order_T r1 r2);Intuition EAuto with real.
+Intros r1 r2.
+Generalize (total_order_T r1 r2) (imp_not_Req r1 r2).
+Intuition EAuto 4 with real.
 Save.
 
 (**********)