f_equal, revert, specialize in ML, contradict in better Ltac (+doc)

 * "f_equal" is now a tactic in ML (placed alongside congruence since
   it uses it). Normally, it should be completely compatible with the
   former Ltac version, except that it doesn't suffer anymore from the
   "up to 5 args" earlier limitation.

 * "revert" also becomes an ML tactic. This doesn't bring any real 
   improvement, just some more uniformity with clear and generalize.  

 * The experimental "narrow" tactic is removed from Tactics.v, and 
   replaced by an evolution of the old & undocumented "specialize" 
   ML tactic: 
   - when specialize is called on an hyp H, the specialization is 
     now done in place on H. For instance "specialize (H t u v)"
     removes the three leading forall of H and intantiates them by 
     t u and v.
   - otherwise specialize still works as before (i.e. as a kind of 
     generalize).
   See the RefMan and test-suite/accept/specialize.v for more infos. 
   Btw, specialize can still accept an optional number for specifying 
   how many premises to instantiate. This number should normally 
   be useless now (some autodetection mecanism added). Hence this 
   feature is left undocumented. For the happy few still using 
   specialize in the old manner, beware of the slight incompatibities...

 * finally, "contradict" is left as Ltac in Tactics.v, but it has 
   now a better shape (accepts unfolded nots and/or things in Type), 
   and also some documentation in the RefMan



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

6 files changed, 56 insertions, 109 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 993f1ae79..832829135 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -584,8 +584,8 @@ Proof.
  rewrite in_find_iff, in_find_iff, H; intuition.
  rewrite find_mapsto_iff in H0,H1; congruence.
  destruct H.
- narrow H with y.
- narrow H0 with y.
+ specialize (H y).
+ specialize (H0 y).
  do 2 rewrite in_find_iff in H.
  generalize (find_mapsto_iff m y)(find_mapsto_iff m' y).
  do 2 destruct find; auto; intros.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 1c8bac6d9..e8d639003 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -387,19 +387,6 @@ the above form:
         end);
       cbv zeta beta in *.
 
-    (** If you have a negated goal and [H] is a negated
-        hypothesis, then [contra H] exchanges your goal and [H],
-        removing the negations.  (Just like [swap] but reuses
-        the same name. *)
-    Ltac contra H :=
-      let J := fresh in
-      unfold not;
-      unfold not in H;
-      intros J;
-      apply H;
-      clear H;
-      rename J into H.
-
     (** [decompose records] calls [decompose record H] on every
         relevant hypothesis [H]. *)
     Tactic Notation "decompose" "records" :=
@@ -704,15 +691,15 @@ the above form:
     unfold not in *;
     match goal with
     | H: (In ?x ?r) -> False |- (In ?x ?s) -> False =>
-      contra H; fsetdec_body
+      contradict H; fsetdec_body
     | H: (In ?x ?r) -> False |- (E.eq ?x ?y) -> False =>
-      contra H; fsetdec_body
+      contradict H; fsetdec_body
     | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
-      contra H; fsetdec_body
+      contradict H; fsetdec_body
     | H: ?P -> False |- ?Q -> False =>
       if prop (FSet_elt_Prop P) holds by
         (auto 100 with FSet_Prop)
-      then (contra H; fsetdec_body)
+      then (contradict H; fsetdec_body)
       else fsetdec_body
     | |- _ =>
       fsetdec_body
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index f61e9422e..50653c420 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -11,43 +11,43 @@
 Require Import Notations.
 Require Import Logic.
 
-(** Useful tactics *)
-
-(* A shorter name for generalize + clear, can be seen as an anti-intro *)
-
-Tactic Notation "revert" ne_hyp_list(l) := generalize l; clear l.
-
-(**************************************
- A tactic for proof by contradiction
-     with contradict H 
-         H: ~A |-   B      gives           |-   A
-         H: ~A |- ~ B     gives  H: B |-   A
-         H:   A |-   B      gives           |- ~ A
-         H:   A |-   B      gives           |- ~ A
-         H:   A |- ~ B     gives  H: A |- ~ A
-**************************************)
-
-Ltac contradict name := 
-     let term := type of name in (
-     match term with 
-       (~_) => 
-          match goal with 
-            |- ~ _  => let x := fresh in
-                     (intros x; case name; 
-                      generalize x; clear x name;
-                      intro name)
-          | |- _    => case name; clear name
-          end
-     | _ => 
-          match goal with 
-            |- ~ _  => let x := fresh in
-                    (intros x;  absurd term;
-                       [idtac | exact name]; generalize x; clear x name;
-                       intros name)
-          | |- _    => generalize name; absurd term;
-                       [idtac | exact name]; clear name
-          end
-     end).
+(** * Useful tactics *)
+
+(** A tactic for proof by contradiction. With contradict H, 
+    -   H:~A |-  B    gives       |-  A
+    -   H:~A |- ~B    gives  H: B |-  A
+    -   H: A |-  B    gives       |- ~A
+    -   H: A |- ~B    gives  H: B |- ~A
+   Moreover, negations may be in unfolded forms, 
+   and A or B may live in Type *)
+
+Ltac contradict H :=
+  let save tac H := let x:=fresh in intro x; tac H; rename x into H
+  in 
+  let negpos H := case H; clear H 
+  in 
+  let negneg H := save negpos H
+  in
+  let pospos H := 
+    let A := type of H in (elimtype False; revert H; try fold (~A))
+  in
+  let posneg H := save pospos H
+  in 
+  let neg H := match goal with 
+   | |- (~_) => negneg H
+   | |- (_->False) => negneg H
+   | |- _ => negpos H
+  end in 
+  let pos H := match goal with 
+   | |- (~_) => posneg H
+   | |- (_->False) => posneg H
+   | |- _ => pospos H
+  end in
+  match type of H with 
+   | (~_) => neg H
+   | (_->False) => neg H
+   | _ => pos H
+  end.
 
 (* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
 
@@ -55,62 +55,22 @@ Ltac swap H :=
   idtac "swap is OBSOLETE: use contradict instead.";
   intro; apply H; clear H.
 
-(* to contradict an hypothesis without copying its type. *)
+(* To contradict an hypothesis without copying its type. *)
 
-Ltac absurd_hyp h := 
+Ltac absurd_hyp H := 
   idtac "absurd_hyp is OBSOLETE: use contradict instead.";
-  let T := type of h in 
+  let T := type of H in 
   absurd T.
 
-(* A useful complement to contradict. Here t : ~ A where H : A. *)
+(* A useful complement to contradict. Here H : A and G allows to conclude ~A *)
 
-Ltac false_hyp h t := 
-  let T := type of h in absurd T; [ apply t | assumption ].
+Ltac false_hyp H G := 
+  let T := type of H in absurd T; [ apply G | assumption ].
 
 (* A case with no loss of information. *)
 
 Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x.
 
-(* A tactic for easing the use of lemmas f_equal, f_equal2, ... *)
-
-Ltac f_equal := 
-  let cg := try congruence in
-  let r := try reflexivity in 
-  match goal with 
-   | |- ?f ?a = ?f' ?a' => cut (a=a'); [cg|r]
-   | |- ?f ?a ?b = ?f' ?a' ?b' => 
-      cut (b=b');[cut (a=a');[cg|r]|r]
-   | |- ?f ?a ?b ?c = ?f' ?a' ?b' ?c'=> 
-      cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]
-   | |- ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d'=> 
-      cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]
-   | |- ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e'=> 
-      cut (e=e');[cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]|r]
-   | |- ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g' => 
-      cut (f=f');[cut (e=e');[cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]|r]|r]
-   | _ => idtac
-  end.
-
-(* Specializing universal hypothesis. 
-   The word "specialize" is already used for a not-documented-anymore 
-   tactic still used in some users contribs. Any idea for a better name?
-*)
-
-Tactic Notation "narrow" hyp(H) "with" constr(x) := 
- generalize (H x); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) := 
- generalize (H x y); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z):= 
- generalize (H x y z); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t):= 
- generalize (H x y z t); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t) constr(u):= 
- generalize (H x y z t u); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t) constr(u) constr(v) := 
- generalize (H x y z t u v); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t) constr(u) constr(v) constr(w) := 
- generalize (H x y z t u v w); clear H; intro H.
-
 (* Rewriting in all hypothesis several times everywhere *)
 
 Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index f30c5b763..6b02e8383 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -162,7 +162,7 @@ Section Infinite_sets.
     generalize (H'3 x).
     intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
       auto with sets.
-    specialize  5Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
+    specialize Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
       intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ];
 	auto with sets.
     intros x1 H'4; try assumption.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 88cdabe3f..ec44a6e58 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -87,7 +87,7 @@ Section Integers_sect.
     apply Totally_ordered_definition.
     simpl in |- *.
     intros H' x y H'0.
-    specialize  2le_or_lt with (n := x) (m := y); intro H'2; elim H'2.
+    elim le_or_lt with (n := x) (m := y).
     intro H'1; left; auto with sets arith.
     intro H'1; right.
     cut (y <= x); auto with sets arith.
@@ -142,8 +142,8 @@ Section Integers_sect.
     elim H'0; intros H'1 H'2.
     cut (In nat Integers (S x)).
     intro H'3.
-    specialize  1H'2 with (y := S x); intro H'4; lapply H'4;
-      [ intro H'5; clear H'4 | try assumption; clear H'4 ].
+    specialize H'2 with (y := S x); lapply H'2;
+      [ intro H'5; clear H'2 | try assumption; clear H'2 ].
     simpl in H'5.
     absurd (S x <= x); auto with arith.
     apply triv_nat.
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index a7da7db9a..d5257c12c 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -140,10 +140,10 @@ intros U R H' x b H'0; elim H'0.
 intros x0 a H'1; exists a; auto with sets.
 intros x0 y z H'1 H'2 H'3 a H'4.
 red in H'.
-specialize  3H' with (x := x0) (a := a) (b := y); intro H'7; lapply H'7;
+specialize H' with (x := x0) (a := a) (b := y); lapply H'; 
  [ intro H'8; lapply H'8;
-    [ intro H'9; try exact H'9; clear H'8 H'7 | clear H'8 H'7 ]
- | clear H'7 ]; auto with sets.
+    [ intro H'9; try exact H'9; clear H'8 H' | clear H'8 H' ]
+ | clear H' ]; auto with sets.
 elim H'9.
 intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5.
 elim (H'3 t); auto with sets.