Merge PR #13315: Convert logic chapter to prodn

Reviewed-by: Zimmi48

4 files changed, 129 insertions, 182 deletions

diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index d46dea1f5d..c93d621048 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -567,6 +567,19 @@ Dealing with fields
     intros x y H H1; field [H1]; auto.
     Abort.
 
+
+.. example:: :tacn:`field` that generates side goals
+
+   .. 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.
+
 .. tacn:: field_simplify {? [ {+ @one_term__eq } ] } {+ @one_term } {? in @ident }
  
    Performs the simplification in the conclusion of the
@@ -679,7 +692,7 @@ First Samuel Boutin designed the tactic ``ACDSimpl``. This tactic did lot
 of rewriting. But the proofs terms generated by rewriting were too big
 for Coq’s type checker. Let us see why:
 
-.. coqtop:: all
+.. coqtop:: reset all
 
   Require Import ZArith.
   Open Scope Z_scope.
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index e1f57c9bea..6464f085b8 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -60,7 +60,7 @@ The constructs in :token:`ltac_expr` are :term:`left associative`.
    ltac_expr3 ::= @l3_tactic
    | @ltac_expr2
    ltac_expr2 ::= @ltac_expr1 + {| @ltac_expr2 | @binder_tactic }
-   | @ltac_expr1 || {| @ltac_expr2 | @binder_tactic }
+   | @ltac_expr1 %|| {| @ltac_expr2 | @binder_tactic }
    | @l2_tactic
    | @ltac_expr1
    ltac_expr1 ::= @tactic_value
@@ -729,7 +729,7 @@ First tactic to make progress: ||
 Yet another way of branching without backtracking is the following
 structure:
 
-.. tacn:: @ltac_expr1 || {| @ltac_expr2 | @binder_tactic }
+.. tacn:: @ltac_expr1 %|| {| @ltac_expr2 | @binder_tactic }
    :name: || (first tactic making progress)
 
    :n:`@ltac_expr1 || @ltac_expr2` is
@@ -1353,8 +1353,8 @@ Pattern matching on goals and hypotheses: match goal
    .. insertprodn goal_pattern match_hyp
 
    .. prodn::
-      goal_pattern ::= {*, @match_hyp } |- @match_pattern
-      | [ {*, @match_hyp } |- @match_pattern ]
+      goal_pattern ::= {*, @match_hyp } %|- @match_pattern
+      | [ {*, @match_hyp } %|- @match_pattern ]
       | _
       match_hyp ::= @name : @match_pattern
       | @name := @match_pattern
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index b912bcbdf8..a46f4fb894 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -562,7 +562,7 @@ Built-in quotations
    | ltac1 : ( @ltac1_expr_in_env )
    | ltac1val : ( @ltac1_expr_in_env )
    ltac1_expr_in_env ::= @ltac_expr
-   | {* @ident } |- @ltac_expr
+   | {* @ident } %|- @ltac_expr
 
 The current implementation recognizes the following built-in quotations:
 
@@ -978,7 +978,7 @@ Match over goals
    .. prodn::
       goal_match_list ::= {? %| } {+| @gmatch_rule }
       gmatch_rule ::= @gmatch_pattern => @ltac2_expr
-      gmatch_pattern ::= [ {*, @gmatch_hyp_pattern } |- @ltac2_match_pattern ]
+      gmatch_pattern ::= [ {*, @gmatch_hyp_pattern } %|- @ltac2_match_pattern ]
       gmatch_hyp_pattern ::= @name : @ltac2_match_pattern
 
    Matches over goals, similar to Ltac1 :tacn:`match goal`.
@@ -1602,8 +1602,8 @@ Here is the syntax for the :n:`q_*` nonterminals:
    ltac2_clause ::= in @ltac2_in_clause
    | at @ltac2_occs_nums
    ltac2_in_clause ::= * {? @ltac2_occs }
-   | * |- {? @ltac2_concl_occ }
-   | {*, @ltac2_hypident_occ } {? |- {? @ltac2_concl_occ } }
+   | * %|- {? @ltac2_concl_occ }
+   | {*, @ltac2_hypident_occ } {? %|- {? @ltac2_concl_occ } }
 
 .. insertprodn q_occurrences ltac2_hypident
 
@@ -1633,7 +1633,7 @@ Here is the syntax for the :n:`q_*` nonterminals:
 .. insertprodn ltac2_oriented_rewriter ltac2_rewriter
 
 .. prodn::
-   ltac2_oriented_rewriter ::= {| -> | <- } @ltac2_rewriter
+   ltac2_oriented_rewriter ::= {? {| -> | <- } } @ltac2_rewriter
    ltac2_rewriter ::= {? @natural } {? {| ? | ! } } @ltac2_constr_with_bindings
 
 .. insertprodn ltac2_for_each_goal ltac2_goal_tactics
diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst
index c4faa7284f..5aaded2726 100644
--- a/doc/sphinx/proofs/automatic-tactics/logic.rst
+++ b/doc/sphinx/proofs/automatic-tactics/logic.rst
@@ -5,7 +5,6 @@ Solvers for logic and equality
 ==============================
 
 .. tacn:: tauto
-   :name: tauto
 
    This tactic implements a decision procedure for intuitionistic propositional
    calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff
@@ -13,53 +12,58 @@ Solvers for logic and equality
    intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and
    logical equivalence but does not unfold any other definition.
 
-.. example::
+   .. example::
+
+      The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would
+      fail:
 
-   The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would
-   fail:
+      .. coqtop:: reset all
 
-   .. coqtop:: reset all
+         Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x.
+         intros.
+         tauto.
 
-      Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x.
-      intros.
-      tauto.
+   Moreover, if it has nothing else to do, :tacn:`tauto` performs introductions.
+   Therefore, the use of :tacn:`intros` in the previous proof is unnecessary.
+   :tacn:`tauto` can for instance for:
 
-Moreover, if it has nothing else to do, :tacn:`tauto` performs introductions.
-Therefore, the use of :tacn:`intros` in the previous proof is unnecessary.
-:tacn:`tauto` can for instance for:
+   .. example::
 
-.. example::
+      .. coqtop:: reset all
 
-   .. coqtop:: reset all
+         Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x.
+         tauto.
 
-      Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x.
-      tauto.
+   .. note::
+     In contrast, :tacn:`tauto` cannot solve the following goal
+     :g:`Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) ->`
+     :g:`forall x:nat, ~ ~ (A \/ P x).`
+     because :g:`(forall x:nat, ~ A -> P x)` cannot be treated as atomic and
+     an instantiation of `x` is necessary.
 
-.. note::
-  In contrast, :tacn:`tauto` cannot solve the following goal
-  :g:`Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) ->`
-  :g:`forall x:nat, ~ ~ (A \/ P x).`
-  because :g:`(forall x:nat, ~ A -> P x)` cannot be treated as atomic and
-  an instantiation of `x` is necessary.
+   .. tacn:: dtauto
 
-.. tacv:: dtauto
-   :name: dtauto
+      While :tacn:`tauto` recognizes inductively defined connectives isomorphic to
+      the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``,
+      ``Empty_set``, ``unit`` and ``True``, :tacn:`dtauto` also recognizes all inductive
+      types with one constructor and no indices, i.e. record-style connectives.
 
-   While :tacn:`tauto` recognizes inductively defined connectives isomorphic to
-   the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``,
-   ``Empty_set``, ``unit``, ``True``, :tacn:`dtauto` also recognizes all inductive
-   types with one constructor and no indices, i.e. record-style connectives.
+.. todo would be nice to explain/discuss the various types of flags
+   that define the differences between these tactics.  See Tauto.v/tauto.ml.
 
-.. tacn:: intuition @tactic
-   :name: intuition
+.. tacn:: intuition {? @ltac_expr }
 
-   The tactic :tacn:`intuition` takes advantage of the search-tree built by the
-   decision procedure involved in the tactic :tacn:`tauto`. It uses this
-   information to generate a set of subgoals equivalent to the original one (but
-   simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If
-   this tactic fails on some goals then :tacn:`intuition` fails. In fact,
+   Uses the search tree built by the decision procedure for :tacn:`tauto`
+   to generate a set of subgoals equivalent to the original one (but
+   simpler than it) and applies :n:`@ltac_expr` to them :cite:`Mun94`. If
+   :n:`@ltac_expr` is not specified, it defaults to :n:`auto with *`
+   If :n:`@ltac_expr` fails on some goals then :tacn:`intuition` fails. In fact,
    :tacn:`tauto` is simply :g:`intuition fail`.
 
+   :tacn:`intuition` recognizes inductively defined connectives
+   isomorphic to the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``,
+   ``Empty_set``, ``unit`` and ``True``.
+
    .. example::
 
       For instance, the tactic :g:`intuition auto` applied to the goal::
@@ -72,98 +76,76 @@ Therefore, the use of :tacn:`intros` in the previous proof is unnecessary.
 
       and then uses :tacn:`auto` which completes the proof.
 
-Originally due to César Muñoz, these tactics (:tacn:`tauto` and
-:tacn:`intuition`) have been completely re-engineered by David Delahaye using
-mainly the tactic language (see :ref:`ltac`). The code is
-now much shorter and a significant increase in performance has been noticed.
-The general behavior with respect to dependent types, unfolding and
-introductions has slightly changed to get clearer semantics. This may lead to
-some incompatibilities.
+   .. tacn:: dintuition {? @ltac_expr }
 
-.. tacv:: intuition
-
-   Is equivalent to :g:`intuition auto with *`.
-
-.. tacv:: dintuition
-   :name: dintuition
-
-   While :tacn:`intuition` recognizes inductively defined connectives
-   isomorphic to the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``,
-   ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` also recognizes all inductive
-   types with one constructor and no indices, i.e. record-style connectives.
+      In addition to the inductively defined connectives recognized by :tacn:`intuition`,
+      :tacn:`dintuition` also recognizes all inductive
+      types with one constructor and no indices, i.e. record-style connectives.
 
-.. flag:: Intuition Negation Unfolding
+   .. flag:: Intuition Negation Unfolding
 
-   Controls whether :tacn:`intuition` unfolds inner negations which do not need
-   to be unfolded. This flag is on by default.
+      Controls whether :tacn:`intuition` unfolds inner negations which do not need
+      to be unfolded. The flag is on by default.
 
 .. tacn:: rtauto
-   :name: rtauto
 
-   The :tacn:`rtauto` tactic solves propositional tautologies similarly to what
-   :tacn:`tauto` does. The main difference is that the proof term is built using a
+   Solves propositional tautologies similarly to
+   :tacn:`tauto`, but the proof term is built using a
    reflection scheme applied to a sequent calculus proof of the goal.  The search
    procedure is also implemented using a different technique.
 
-   Users should be aware that this difference may result in faster proof-search
-   but slower proof-checking, and :tacn:`rtauto` might not solve goals that
+   Users should be aware that this difference may result in faster proof search
+   but slower proof checking, and :tacn:`rtauto` might not solve goals that
    :tacn:`tauto` would be able to solve (e.g. goals involving universal
    quantifiers).
 
    Note that this tactic is only available after a ``Require Import Rtauto``.
 
-.. tacn:: firstorder
-   :name: firstorder
+.. tacn:: firstorder {? @ltac_expr } {? using {+, @qualid } } {? with {+ @ident } }
 
-   The tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to
-   first- order reasoning, written by Pierre Corbineau. It is not restricted to
-   usual logical connectives but instead may reason about any first-order class
+   An experimental extension of :tacn:`tauto` to
+   first-order reasoning. It is not restricted to
+   usual logical connectives but instead can reason about any first-order class
    inductive definition.
 
-.. opt:: Firstorder Solver @tactic
-   :name: Firstorder Solver
-
-   The default tactic used by :tacn:`firstorder` when no rule applies is
-   :g:`auto with core`, it can be reset locally or globally using this option.
-
-   .. cmd:: Print Firstorder Solver
-
-      Prints the default tactic used by :tacn:`firstorder` when no rule applies.
-
-.. tacv:: firstorder @tactic
-
-   Tries to solve the goal with :n:`@tactic` when no logical rule may apply.
-
-.. tacv:: firstorder using {+ @qualid}
+   :token:`ltac_expr`
+     Tries to solve the goal with :token:`ltac_expr` when no logical rule applies.
+     If unspecified, the tactic uses the default from the :opt:`Firstorder Solver`
+     option.
 
-   .. deprecated:: 8.3
+   :n:`using {+, @qualid }`
+     Adds the lemmas :n:`{+, @qualid }` to the proof search environment. If :n:`@qualid`
+     refers to an inductive type, its constructors are
+     added to the proof search environment.
 
-      Use the syntax below instead (with commas).
+   :n:`with {+ @ident }`
+     Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident }` to the proof search
+     environment.
 
-.. tacv:: firstorder using {+, @qualid}
+   .. opt:: Firstorder Solver @ltac_expr
 
-  Adds lemmas :n:`{+, @qualid}` to the proof-search environment. If :n:`@qualid`
-  refers to an inductive type, it is the collection of its constructors which are
-  added to the proof-search environment.
+      The default tactic used by :tacn:`firstorder` when no rule applies in
+      :g:`auto with core`.  It can be set locally or globally using this option.
 
-.. tacv:: firstorder with {+ @ident}
+   .. cmd:: Print Firstorder Solver
 
-  Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident}` to the proof-search
-  environment.
+      Prints the default tactic used by :tacn:`firstorder` when no rule applies.
 
-.. tacv:: firstorder @tactic using {+, @qualid} with {+ @ident}
+   .. opt:: Firstorder Depth @natural
 
-  This combines the effects of the different variants of :tacn:`firstorder`.
+      Controls the proof search depth bound.
 
-.. opt:: Firstorder Depth @natural
-   :name: Firstorder Depth
+.. tacn:: congruence {? @natural } {? with {+ @one_term } }
 
-   This option controls the proof-search depth bound.
+   :token:`natural`
+     Specifies the maximum number of hypotheses stating quantified equalities that may be added
+     to the problem in order to solve it. The default is 1000.
 
-.. tacn:: congruence
-   :name: congruence
+   :n:`{? with {+ @one_term } }`
+     Adds :n:`{+ @one_term }` to the pool of terms used by :tacn:`congruence`. This helps
+     in case you have partially applied constructors in your goal.
 
-   The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard
+   Implements the standard
    Nelson and Oppen congruence closure algorithm, which is a decision procedure
    for ground equalities with uninterpreted symbols. It also includes
    constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal
@@ -178,53 +160,45 @@ some incompatibilities.
    equality must contain all the quantified variables in order for congruence to
    match against it.
 
-.. example::
-
-   .. coqtop:: reset all
-
-      Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a.
-      intros.
-      congruence.
-      Qed.
-
-      Theorem inj (A:Type) (f:A -> A * A) (a c d: A) : f = pair a -> Some (f c) = Some (f d) -> c=d.
-      intros.
-      congruence.
-      Qed.
+   Increasing the maximum number of hypotheses may solve
+   problems that would have failed with a smaller value.  It will make failures slower but it
+   won't make successes found with the smaller value any slower.
+   You may want to use :tacn:`assert` to add some lemmas as
+   hypotheses so that :tacn:`congruence` can use them.
 
-.. tacv:: congruence @natural
+   .. example::
 
-  Tries to add at most :token:`natural` instances of hypotheses stating quantified equalities
-  to the problem in order to solve it. A bigger value of :token:`natural` does not make
-  success slower, only failure. You might consider adding some lemmas as
-  hypotheses using assert in order for :tacn:`congruence` to use them.
+      .. coqtop:: reset all
 
-.. tacv:: congruence with {+ @term}
-   :name: congruence with
+         Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a.
+         intros.
+         congruence.
+         Qed.
 
-   Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps
-   in case you have partially applied constructors in your goal.
+         Theorem inj (A:Type) (f:A -> A * A) (a c d: A) : f = pair a -> Some (f c) = Some (f d) -> c=d.
+         intros.
+         congruence.
+         Qed.
 
-.. exn:: I don’t know how to handle dependent equality.
+   .. exn:: I don’t know how to handle dependent equality.
 
-  The decision procedure managed to find a proof of the goal or of a
-  discriminable equality but this proof could not be built in Coq because of
-  dependently-typed functions.
+      The decision procedure managed to find a proof of the goal or of a
+      discriminable equality but this proof could not be built in Coq because of
+      dependently-typed functions.
 
-.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms.
+   .. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms.
 
-  The decision procedure could solve the goal with the provision that additional
-  arguments are supplied for some partially applied constructors. Any term of an
-  appropriate type will allow the tactic to successfully solve the goal. Those
-  additional arguments can be given to congruence by filling in the holes in the
-  terms given in the error message, using the :tacn:`congruence with` variant described above.
+      The decision procedure could solve the goal with the provision that additional
+      arguments are supplied for some partially applied constructors. Any term of an
+      appropriate type will allow the tactic to successfully solve the goal. Those
+      additional arguments can be given to congruence by filling in the holes in the
+      terms given in the error message, using the `with` clause.
 
-.. flag:: Congruence Verbose
+   .. flag:: Congruence Verbose
 
-  This flag makes :tacn:`congruence` print debug information.
+      Makes :tacn:`congruence` print debug information.
 
 .. 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
@@ -252,43 +226,3 @@ some incompatibilities.
 
       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.
-
-.. tacv:: field
-          field_simplify {* @term}
-          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/ring/RealField.v for an example of instantiation,
-   theory theories/Reals for many examples of use of field.