Remove parts of the Tactics chapter.

1 files changed, 0 insertions, 459 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 439be0ecf8..adabc56c50 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -53,89 +53,6 @@
 .. exn:: Not the right number of induction arguments.
    :undocumented:
 
-Equality and inductive sets
----------------------------
-
-We describe in this section some special purpose tactics dealing with
-equality and inductive sets or types. These tactics use the
-equality :g:`eq:forall (A:Type), A->A->Prop`, simply written with the infix
-symbol :g:`=`.
-
-.. tacn:: decide equality
-   :name: decide equality
-
-   This tactic solves a goal of the form :g:`forall x y : R, {x = y} + {~ x = y}`,
-   where :g:`R` is an inductive type such that its constructors do not take
-   proofs or functions as arguments, nor objects in dependent types. It
-   solves goals of the form :g:`{x = y} + {~ x = y}` as well.
-
-.. tacn:: compare @term @term
-   :name: compare
-
-   This tactic compares two given objects :n:`@term` and :n:`@term` of an
-   inductive datatype. If :g:`G` is the current goal, it leaves the sub-
-   goals :n:`@term =@term -> G` and :n:`~ @term = @term -> G`. The type of
-   :n:`@term` and :n:`@term` must satisfy the same restrictions as in the
-   tactic ``decide equality``.
-
-.. tacn:: simplify_eq @term
-   :name: simplify_eq
-
-   Let :n:`@term` be the proof of a statement of conclusion :n:`@term = @term`.
-   If :n:`@term` and :n:`@term` are structurally different (in the sense
-   described for the tactic :tacn:`discriminate`), then the tactic
-   ``simplify_eq`` behaves as :n:`discriminate @term`, otherwise it behaves as
-   :n:`injection @term`.
-
-.. note::
-   If some quantified hypothesis of the goal is named :n:`@ident`,
-   then :n:`simplify_eq @ident` first introduces the hypothesis in the local
-   context using :n:`intros until @ident`.
-
-.. tacv:: simplify_eq @num
-
-   This does the same thing as :n:`intros until @num` then
-   :n:`simplify_eq @ident` where :n:`@ident` is the identifier for the last
-   introduced hypothesis.
-
-.. tacv:: simplify_eq @term with @bindings_list
-
-   This does the same as :n:`simplify_eq @term` but using the given bindings to
-   instantiate parameters or hypotheses of :n:`@term`.
-
-.. tacv:: esimplify_eq @num
-          esimplify_eq @term {? with @bindings_list}
-   :name: esimplify_eq; _
-
-   This works the same as :tacn:`simplify_eq` but if the type of :n:`@term`, or the
-   type of the hypothesis referred to by :n:`@num`, has uninstantiated
-   parameters, these parameters are left as existential variables.
-
-.. tacv:: simplify_eq
-
-   If the current goal has form :g:`t1 <> t2`, it behaves as
-   :n:`intro @ident; simplify_eq @ident`.
-
-.. tacn:: dependent rewrite -> @ident
-   :name: dependent rewrite ->
-
-   This tactic applies to any goal. If :n:`@ident` has type
-   :g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each
-   :n:`@term` of the equality has a sigma type :g:`{ a:A & (B a)}`) this tactic
-   rewrites :g:`a` into :g:`a'` and :g:`b` into :g:`b'` in the current goal.
-   This tactic works even if :g:`B` is also a sigma type. This kind of
-   equalities between dependent pairs may be derived by the
-   :tacn:`injection` and :tacn:`inversion` tactics.
-
-.. tacv:: dependent rewrite <- @ident
-   :name: dependent rewrite <-
-
-   Analogous to :tacn:`dependent rewrite ->` but uses the equality from right to
-   left.
-
-Inversion
----------
-
 .. tacn:: functional inversion @ident
    :name: functional inversion
 
@@ -168,379 +85,3 @@ Inversion
       :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to
       functional inversion, this variant allows choosing which :token:`qualid`
       is inverted.
-
-Classical tactics
------------------
-
-In order to ease the proving process, when the ``Classical`` module is
-loaded, a few more tactics are available. Make sure to load the module
-using the ``Require Import`` command.
-
-.. tacn:: classical_left
-          classical_right
-   :name: classical_left; classical_right
-
-   These tactics are the analog of :tacn:`left` and :tacn:`right`
-   but using classical logic. They can only be used for
-   disjunctions. Use :tacn:`classical_left` to prove the left part of the
-   disjunction with the assumption that the negation of right part holds.
-   Use :tacn:`classical_right` to prove the right part of the disjunction with
-   the assumption that the negation of left part holds.
-
-.. _tactics-automating:
-
-Automating
-------------
-
-
-.. tacn:: btauto
-   :name: btauto
-
-   The tactic :tacn:`btauto` implements a reflexive solver for boolean
-   tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are
-   constructed over the following grammar:
-
-   .. _btauto_grammar:
-
-   .. productionlist:: sentence
-      btauto_term : `ident`
-                  : true
-                  : false
-                  : orb `btauto_term` `btauto_term`
-                  : andb `btauto_term` `btauto_term`
-                  : xorb `btauto_term` `btauto_term`
-                  : negb `btauto_term`
-                  : if `btauto_term` then `btauto_term` else `btauto_term`
-
-   Whenever the formula supplied is not a tautology, it also provides a
-   counter-example.
-
-   Internally, it uses a system very similar to the one of the ring
-   tactic.
-
-   Note that this tactic is only available after a ``Require Import Btauto``.
-
-   .. exn:: Cannot recognize a boolean equality.
-
-      The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto`
-      doesn't introduce variables into the context on its own.
-
-.. tacn:: omega
-   :name: omega
-
-   The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision
-   procedure for Presburger arithmetic. It solves quantifier-free
-   formulas built with `~`, `\\/`, `/\\`, `->` on top of equalities,
-   inequalities and disequalities on both the type :g:`nat` of natural numbers
-   and :g:`Z` of binary integers. This tactic must be loaded by the command
-   ``Require Import Omega``. See the additional documentation about omega
-   (see Chapter :ref:`omega`).
-
-
-.. tacn:: ring
-   :name: ring
-
-   This tactic solves equations upon polynomial expressions of a ring
-   (or semiring) structure. It proceeds by normalizing both hand sides
-   of the equation (w.r.t. associativity, commutativity and
-   distributivity, constant propagation) and comparing syntactically the
-   results.
-
-.. tacn:: ring_simplify {* @term}
-   :name: ring_simplify
-
-   This tactic applies the normalization procedure described above to
-   the given terms. The tactic then replaces all occurrences of the terms
-   given in the conclusion of the goal by their normal forms. If no term
-   is given, then the conclusion should be an equation and both hand
-   sides are normalized.
-
-See :ref:`Theringandfieldtacticfamilies` for more information on
-the tactic and how to declare new ring structures. All declared field structures
-can be printed with the ``Print Rings`` command.
-
-.. tacn:: field
-          field_simplify {* @term}
-          field_simplify_eq
-   :name: field; field_simplify; field_simplify_eq
-
-   The field tactic is built on the same ideas as ring: this is a
-   reflexive tactic that solves or simplifies equations in a field
-   structure. The main idea is to reduce a field expression (which is an
-   extension of ring expressions with the inverse and division
-   operations) to a fraction made of two polynomial expressions.
-
-   Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}`
-   replaces the provided terms by their reduced fraction.
-   :n:`field_simplify_eq` applies when the conclusion is an equation: it
-   simplifies both hand sides and multiplies so as to cancel
-   denominators. So it produces an equation without division nor inverse.
-
-   All of these 3 tactics may generate a subgoal in order to prove that
-   denominators are different from zero.
-
-   See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to
-   declare new field structures. All declared field structures can be
-   printed with the Print Fields command.
-
-.. example::
-
-   .. coqtop:: reset all
-
-      Require Import Reals.
-      Goal forall x y:R,
-      (x * y > 0)%R ->
-      (x * (1 / x + x / (x + y)))%R =
-      ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R.
-
-      intros; field.
-
-.. seealso::
-
-   File plugins/setoid_ring/RealField.v for an example of instantiation,
-   theory theories/Reals for many examples of use of field.
-
-Non-logical tactics
-------------------------
-
-
-.. tacn:: cycle @num
-   :name: cycle
-
-   This tactic puts the :n:`@num` first goals at the end of the list of goals.
-   If :n:`@num` is negative, it will put the last :math:`|num|` goals at the
-   beginning of the list.
-
-.. example::
-
-   .. coqtop:: none reset
-
-      Parameter P : nat -> Prop.
-
-   .. coqtop:: all abort
-
-      Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
-      repeat split.
-      all: cycle 2.
-      all: cycle -3.
-
-.. tacn:: swap @num @num
-   :name: swap
-
-   This tactic switches the position of the goals of indices :n:`@num` and
-   :n:`@num`. If either :n:`@num` or :n:`@num` is negative then goals are
-   counted from the end of the focused goal list. Goals are indexed from 1,
-   there is no goal with position 0.
-
-.. example::
-
-   .. coqtop:: all abort
-
-      Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
-      repeat split.
-      all: swap 1 3.
-      all: swap 1 -1.
-
-.. tacn:: revgoals
-   :name: revgoals
-
-   This tactics reverses the list of the focused goals.
-
-   .. example::
-
-      .. coqtop:: all abort
-
-         Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
-         repeat split.
-         all: revgoals.
-
-.. tacn:: shelve
-   :name: shelve
-
-   This tactic moves all goals under focus to a shelf. While on the
-   shelf, goals will not be focused on. They can be solved by
-   unification, or they can be called back into focus with the command
-   :cmd:`Unshelve`.
-
-   .. tacv:: shelve_unifiable
-      :name: shelve_unifiable
-
-      Shelves only the goals under focus that are mentioned in other goals.
-      Goals that appear in the type of other goals can be solved by unification.
-
-      .. example::
-
-         .. coqtop:: all abort
-
-            Goal exists n, n=0.
-            refine (ex_intro _ _ _).
-            all: shelve_unifiable.
-            reflexivity.
-
-.. cmd:: Unshelve
-
-   This command moves all the goals on the shelf (see :tacn:`shelve`)
-   from the shelf into focus, by appending them to the end of the current
-   list of focused goals.
-
-.. tacn:: unshelve @tactic
-   :name: unshelve
-
-   Performs :n:`@tactic`, then unshelves existential variables added to the
-   shelf by the execution of :n:`@tactic`, prepending them to the current goal.
-
-.. tacn:: give_up
-   :name: give_up
-
-   This tactic removes the focused goals from the proof. They are not
-   solved, and cannot be solved later in the proof. As the goals are not
-   solved, the proof cannot be closed.
-
-   The ``give_up`` tactic can be used while editing a proof, to choose to
-   write the proof script in a non-sequential order.
-
-Delaying solving unification constraints
-----------------------------------------
-
-.. tacn:: solve_constraints
-   :name: solve_constraints
-   :undocumented:
-
-.. flag:: Solve Unification Constraints
-
-   By default, after each tactic application, postponed typechecking unification
-   problems are resolved using heuristics. Unsetting this flag disables this
-   behavior, allowing tactics to leave unification constraints unsolved. Use the
-   :tacn:`solve_constraints` tactic at any point to solve the constraints.
-
-Proof maintenance
------------------
-
-*Experimental.*  Many tactics, such as :tacn:`intros`, can automatically generate names, such
-as "H0" or "H1" for a new hypothesis introduced from a goal.  Subsequent proof steps
-may explicitly refer to these names.  However, future versions of Coq may not assign
-names exactly the same way, which could cause the proof to fail because the
-new names don't match the explicit references in the proof.
-
-The following "Mangle Names" settings let users find all the
-places where proofs rely on automatically generated names, which can
-then be named explicitly to avoid any incompatibility.  These
-settings cause Coq to generate different names, producing errors for
-references to automatically generated names.
-
-.. flag:: Mangle Names
-
-   When set, generated names use the prefix specified in the following
-   option instead of the default prefix.
-
-.. opt:: Mangle Names Prefix @string
-   :name: Mangle Names Prefix
-
-   Specifies the prefix to use when generating names.
-
-Performance-oriented tactic variants
-------------------------------------
-
-.. tacn:: change_no_check @term
-   :name: change_no_check
-
-   For advanced usage. Similar to :n:`change @term`, but as an optimization,
-   it skips checking that :n:`@term` is convertible to the goal.
-
-   Recall that the Coq kernel typechecks proofs again when they are concluded to
-   ensure safety. Hence, using :tacn:`change` checks convertibility twice
-   overall, while :tacn:`change_no_check` can produce ill-typed terms,
-   but checks convertibility only once.
-   Hence, :tacn:`change_no_check` can be useful to speed up certain proof
-   scripts, especially if one knows by construction that the argument is
-   indeed convertible to the goal.
-
-   In the following example, :tacn:`change_no_check` replaces :g:`False` by
-   :g:`True`, but :g:`Qed` then rejects the proof, ensuring consistency.
-
-   .. example::
-
-      .. coqtop:: all abort
-
-         Goal False.
-           change_no_check True.
-           exact I.
-         Fail Qed.
-
-   :tacn:`change_no_check` supports all of `change`'s variants.
-
-   .. tacv:: change_no_check @term with @term’
-      :undocumented:
-
-   .. tacv:: change_no_check @term at {+ @num} with @term’
-      :undocumented:
-
-   .. tacv:: change_no_check @term {? {? at {+ @num}} with @term} in @ident
-
-      .. example::
-
-         .. coqtop:: all abort
-
-            Goal True -> False.
-              intro H.
-              change_no_check False in H.
-              exact H.
-            Fail Qed.
-
-   .. tacv:: convert_concl_no_check @term
-      :name: convert_concl_no_check
-
-      .. deprecated:: 8.11
-
-      Deprecated old name for :tacn:`change_no_check`. Does not support any of its
-      variants.
-
-.. tacn:: exact_no_check @term
-   :name: exact_no_check
-
-   For advanced usage. Similar to :n:`exact @term`, but as an optimization,
-   it skips checking that :n:`@term` has the goal's type, relying on the kernel
-   check instead. See :tacn:`change_no_check` for more explanations.
-
-   .. example::
-
-      .. coqtop:: all abort
-
-         Goal False.
-           exact_no_check I.
-         Fail Qed.
-
-   .. tacv:: vm_cast_no_check @term
-      :name: vm_cast_no_check
-
-      For advanced usage. Similar to :n:`exact_no_check @term`, but additionally
-      instructs the kernel to use :tacn:`vm_compute` to compare the
-      goal's type with the :n:`@term`'s type.
-
-      .. example::
-
-        .. coqtop:: all abort
-
-            Goal False.
-              vm_cast_no_check I.
-            Fail Qed.
-
-   .. tacv:: native_cast_no_check @term
-      :name: native_cast_no_check
-
-      for advanced usage. similar to :n:`exact_no_check @term`, but additionally
-      instructs the kernel to use :tacn:`native_compute` to compare the goal's
-      type with the :n:`@term`'s type.
-
-      .. example::
-
-        .. coqtop:: all abort
-
-            Goal False.
-              native_cast_no_check I.
-            Fail Qed.
-
-.. [1] Actually, only the second subgoal will be generated since the
-  other one can be automatically checked.
-.. [2] This corresponds to the cut rule of sequent calculus.
-.. [3] Reminder: opaque constants will not be expanded by δ reductions.