Intuition: temporary(?) restore the unconditional unfolding of not

 Let's check tomorrow the impact on contribs: are the recent build
 failures related to the "not" unfolding stategy or to the new
 handling of conjonction-like constructors ?

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

5 files changed, 32 insertions, 26 deletions

diff --git a/CHANGES b/CHANGES
index 95ddcc040..1963d7157 100644
--- a/CHANGES
+++ b/CHANGES
@@ -48,9 +48,7 @@ Tactics
   to destruct any record-like inductive types, superseding the old
   version of "tauto".
 - Similarly, "intuition" has been made more uniform and, where it now
-  fails, "dintuition" can be used. Moreover, both of them are now only
-  lazily unfolding the occurrences of "not" in goal. Some extra
-  "unfold not in *" might have to be added for compatibility.
+  fails, "dintuition" can be used.
 - Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl,
   harvey, zenon, gwhy) have been removed, since Why2 has not been
   maintained for the last few years. The Why3 plugin should be a suitable
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 12bb36eb4..570c6c7a1 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -48,11 +48,11 @@ type tauto_flags = {
 
 (* Whether unit type includes equality types *)
   strict_unit : bool;
-
-(* Whether inner unfolding is allowed *)
-  inner_unfolding : bool
 }
 
+(* Whether inner not are unfolded *)
+let negation_unfolding = ref true
+
 (* Whether inner iff are unfolded *)
 let iff_unfolding = ref false
 
@@ -63,7 +63,16 @@ let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
-      optname  = "unfolding of iff and not in intuition";
+      optname  = "unfolding of not in intuition";
+      optkey   = ["Intuition";"Negation";"Unfolding"];
+      optread  = (fun () -> !negation_unfolding);
+      optwrite = (:=) negation_unfolding }
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "unfolding of iff in intuition";
       optkey   = ["Intuition";"Iff";"Unfolding"];
       optread  = (fun () -> !iff_unfolding);
       optwrite = (:=) iff_unfolding }
@@ -271,18 +280,17 @@ let rec tauto_intuit flags t_reduce solver ist =
     $t_solver
    ) >>
 
-let reduction_not _ist =
-  if unfold_iff () then
-    <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >>
-  else
-    <:tactic< unfold Coq.Init.Logic.not in * >>
+let reduction_not_iff _ist =
+  match !negation_unfolding, unfold_iff () with
+    | true, true -> <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >>
+    | true, false -> <:tactic< unfold Coq.Init.Logic.not in * >>
+    | false, true -> <:tactic< unfold Coq.Init.Logic.iff in * >>
+    | false, false -> <:tactic< idtac >>
 
-let t_reduction_not = tacticIn reduction_not
+let t_reduction_not_iff = tacticIn reduction_not_iff
 
 let intuition_gen flags tac =
-  let t_reduce =
-    if flags.inner_unfolding then t_reduction_not else  <:tactic<idtac>> in
-  interp (tacticIn (tauto_intuit flags t_reduce tac))
+  interp (tacticIn (tauto_intuit flags t_reduction_not_iff tac))
 
 let tauto_intuitionistic flags g =
   try intuition_gen flags <:tactic<fail>> g
@@ -309,15 +317,14 @@ let tauto_gen flags g =
 let default_intuition_tac = <:tactic< auto with * >>
 
 (* This is the uniform mode dealing with ->, not, iff and types isomorphic to
-   /\ and *, \/ and +, False and Empty_set, True and unit, _and_ eq-like types;
-   not and iff are unfolded only if necessary *)
+   /\ and *, \/ and +, False and Empty_set, True and unit, _and_ eq-like types.
+   For the moment not and iff are still always unfolded. *)
 let tauto_uniform_unit_flags = {
   binary_mode = true;
   binary_mode_bugged_detection = false;
   strict_in_contravariant_hyp = true;
   strict_in_hyp_and_ccl = true;
-  strict_unit = false;
-  inner_unfolding = false
+  strict_unit = false
 }
 
 (* This is the compatibility mode (not used) *)
@@ -326,8 +333,7 @@ let tauto_legacy_flags = {
   binary_mode_bugged_detection = true;
   strict_in_contravariant_hyp = true;
   strict_in_hyp_and_ccl = false;
-  strict_unit = false;
-  inner_unfolding = true
+  strict_unit = false
 }
 
 (* This is the improved mode *)
@@ -336,8 +342,7 @@ let tauto_power_flags = {
   binary_mode_bugged_detection = false;
   strict_in_contravariant_hyp = false; (* supports non-regular connectives *)
   strict_in_hyp_and_ccl = false;
-  strict_unit = false;
-  inner_unfolding = false
+  strict_unit = false
 }
 
 let tauto = tauto_gen tauto_uniform_unit_flags
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 9fef1dc63..dc33167a6 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -1871,8 +1871,9 @@ Module OrdProperties (M:S).
     find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
     add_mapsto_iff by (auto with *).
   unfold O.eqke, O.ltk; simpl.
-  destruct (E.compare t0 x); intuition.
-  elim H; exists e0; apply MapsTo_1 with t0; auto.
+  destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto.
+  - elim H; exists e0; apply MapsTo_1 with t0; auto.
+  - fold (~E.lt t0 x); auto.
   Qed.
 
   Lemma elements_Add_Above : forall m m' x e,
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index eec7196b7..8651a96f7 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -995,6 +995,7 @@ Module OrdProperties (M:S).
    leb_1, gtb_1, (H0 a) by auto with *.
   intuition.
   destruct (E.compare a x); intuition.
+  fold (~E.lt a x); auto with *.
   Qed.
 
   Definition Above x s := forall y, In y s -> E.lt y x.
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 02eadf091..8b11f09b9 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -89,6 +89,7 @@ intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
 *)
 
 Set Implicit Arguments.
+Local Unset Intuition Negation Unfolding.
 
 (**********************************************************************)
 (** * Definitions *)