Merge PR #13762: Remove double induction tactic

Ack-by: Zimmi48
Reviewed-by: ppedrot

7 files changed, 9 insertions, 122 deletions

diff --git a/doc/changelog/04-tactics/13762-remove_double_induction.rst b/doc/changelog/04-tactics/13762-remove_double_induction.rst
new file mode 100644
index 0000000000..4ea54a1ab6
--- /dev/null
+++ b/doc/changelog/04-tactics/13762-remove_double_induction.rst
@@ -0,0 +1,9 @@
+- **Removed:**
+  double induction tactic.  Replace :n:`double induction @ident @ident`
+  with :n:`induction @ident; induction @ident` (or
+  :n:`induction @ident ; destruct @ident` depending on the exact needs).
+  Replace :n:`double induction @natural__1 @natural__2` with
+  :n:`induction @natural__1; induction natural__3` where :n:`natural__3` is the result
+  of :n:`natural__2 - natural__1`
+  (`#13762 <https://github.com/coq/coq/pull/13762>`_,
+  by Jim Fehrle).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 25efca563a..72970f46b0 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2073,19 +2073,6 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    is the name given by :n:`intros until @natural` to the :n:`@natural`-th non-dependent
    premise of the goal.
 
-.. tacn:: double induction @ident @ident
-   :name: double induction
-
-   This tactic is deprecated and should be replaced by
-   :n:`induction @ident; induction @ident` (or
-   :n:`induction @ident ; destruct @ident` depending on the exact needs).
-
-.. tacv:: double induction @natural__1 @natural__2
-
-   This tactic is deprecated and should be replaced by
-   :n:`induction num1; induction num3` where :n:`num3` is the result
-   of :n:`num2 - num1`
-
 .. tacn:: dependent induction @ident
    :name: dependent induction
 
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index e39c066c95..b20c4d173d 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -259,13 +259,6 @@ TACTIC EXTEND simple_destruct
 | [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h }
 END
 
-(** Double induction *)
-
-TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () }
-| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
-  { Elim.h_double_induction h1 h2 }
-END
-
 (* Admit *)
 
 TACTIC EXTEND admit
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 9a55cabc86..9e7843b2bb 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -19,7 +19,6 @@ open Tacmach.New
 open Tacticals.New
 open Clenv
 open Tactics
-open Proofview.Notations
 
 type branch_args = {
   branchnum  : int;         (* the branch number *)
@@ -28,8 +27,6 @@ type branch_args = {
                                true=assumption, false=let-in *)
   branchnames : Tactypes.intro_patterns}
 
-module NamedDecl = Context.Named.Declaration
-
 type elim_kind = Case of bool | Elim
 
 (* Find the right elimination suffix corresponding to the sort of the goal *)
@@ -217,52 +214,3 @@ let h_decompose l c = decompose_these c l
 let h_decompose_or = decompose_or
 
 let h_decompose_and = decompose_and
-
-(* The tactic Double performs a double induction *)
-
-let induction_trailer abs_i abs_j bargs =
-  tclTHEN
-    (tclDO (abs_j - abs_i) intro)
-    (onLastHypId
-       (fun id ->
-          Proofview.Goal.enter begin fun gl ->
-          let idty = pf_get_type_of gl (mkVar id) in
-          let fvty = global_vars (pf_env gl) (project gl) idty in
-          let possible_bring_hyps =
-            (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs
-          in
-          let (hyps,_) =
-            List.fold_left
-              (fun (bring_ids,leave_ids) d ->
-                 let cid = NamedDecl.get_id d in
-                 if not (List.mem cid leave_ids)
-                 then (d::bring_ids,leave_ids)
-                 else (bring_ids,cid::leave_ids))
-              ([],fvty) possible_bring_hyps
-          in
-          let ids = List.rev (ids_of_named_context hyps) in
-          (tclTHENLIST
-            [revert ids; elimination_then (fun _ -> tclIDTAC) id])
-          end
-          ))
-
-let double_ind h1 h2 =
-  Proofview.Goal.enter begin fun gl ->
-  let abs_i = depth_of_quantified_hypothesis true h1 gl in
-  let abs_j = depth_of_quantified_hypothesis true h2 gl in
-  let abs =
-    if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else
-    if abs_i > abs_j then  Proofview.tclUNIT (abs_j,abs_i) else
-      let info = Exninfo.reify () in
-      tclZEROMSG ~info (Pp.str "Both hypotheses are the same.") in
-  abs >>= fun (abs_i,abs_j) ->
-  (tclTHEN (tclDO abs_i intro)
-     (onLastHypId
-        (fun id ->
-           elimination_then
-             (introElimAssumsThen (induction_trailer abs_i abs_j)) id)))
-  end
-
-let h_double_induction = double_ind
-
-
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 01053502e4..a603b472f7 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -21,4 +21,3 @@ val case_tac : bool -> or_and_intro_pattern option ->
 val h_decompose       : inductive list -> constr -> unit Proofview.tactic
 val h_decompose_or    : constr -> unit Proofview.tactic
 val h_decompose_and   : constr -> unit Proofview.tactic
-val h_double_induction : quantified_hypothesis -> quantified_hypothesis-> unit Proofview.tactic
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d93f3bc434..c07073a91a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -77,11 +77,6 @@ val auto_intros_tac : Names.Name.t list -> unit Proofview.tactic
 
 val intros               : unit Proofview.tactic
 
-(** [depth_of_quantified_hypothesis b h g] returns the index of [h] in
-   the conclusion of goal [g], up to head-reduction if [b] is [true] *)
-val depth_of_quantified_hypothesis :
-  bool -> quantified_hypothesis -> Proofview.Goal.t -> int
-
 val intros_until         : quantified_hypothesis -> unit Proofview.tactic
 
 val intros_clearing      : bool list -> unit Proofview.tactic
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 4983ee3c0d..615350c58c 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -154,50 +154,6 @@ induction H.
 change (0 = z -> True) in IHrepr''.
 Abort.
 
-(* Test double induction *)
-
-(* This was failing in 8.5 and before because of a bug in the order of
-   hypotheses *)
-
-Set Warnings "-deprecated".
-
-Inductive I2 : Type :=
-  C2 : forall x:nat, x=x -> I2.
-Goal forall a b:I2, a = b.
-double induction a b.
-Abort.
-
-(* This was leaving useless hypotheses in 8.5 and before because of
-   the same bug. This is a change of compatibility. *)
-
-Inductive I3 : Prop :=
-  C3 : forall x:nat, x=x -> I3.
-Goal forall a b:I3, a = b.
-double induction a b.
-Fail clear H. (* H should have been erased *)
-Abort.
-
-(* This one had quantification in reverse order in 8.5 and before *)
-(* This is a change of compatibility. *)
-
-Goal forall m n, le m n -> le n m -> n=m.
-intros m n. double induction 1 2.
-3:destruct 1. (* Should be "S m0 <= m0" *)
-Abort.
-
-(* Idem *)
-
-Goal forall m n p q, le m n -> le p q -> n+p=m+q.
-intros *. double induction 1 2.
-3:clear H2. (* H2 should have been erased *)
-Abort.
-
-(* This is unchanged *)
-
-Goal forall m n:nat, n=m.
-double induction m n.
-Abort.
-
 (* Mentioned as part of bug #12944 *)
 
 Inductive test : Set := cons : forall (IHv : nat) (v : test), test.