diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 2 |
4 files changed, 14 insertions, 20 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index c0a57763b9..5d219ebd0d 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -35,7 +35,7 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``. The tactics solve propositional formulas parameterized by atomic -arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}. +arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`. The syntax of the formulas is the following: .. productionlist:: `F` @@ -46,8 +46,8 @@ The syntax of the formulas is the following: where :math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the operators :math:`−, +, ×` are respectively subtraction, addition, and product; :math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition. -For :math:`\mathbb{Q}`, equality is not Leibniz equality = but the equality of -rationals ==. +For :math:`\mathbb{Q}`, equality is not Leibniz equality ``=`` but the equality of +rationals ``==``. For :math:`\mathbb{Z}` (resp. :math:`\mathbb{Q}`), :math:`c` ranges over integer constants (resp. rational constants). For :math:`\mathbb{R}`, the tactic recognizes as real constants the @@ -58,7 +58,7 @@ following expressions: c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q | Rdiv(c,c) | Rinv c where :math:`z` is a constant in :math:`\mathbb{Z}` and :math:`q` is a constant in :math:`\mathbb{Q}`. -This includes integer constants written using the decimal notation, *i.e.*, c%R. +This includes integer constants written using the decimal notation, *i.e.*, ``c%R``. *Positivstellensatz* refutations @@ -94,7 +94,7 @@ general form :math:`(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False}` and For each conjunct :math:`C_i`, the tactic calls an oracle which searches for :math:`-1` within the cone. Upon success, the oracle returns a *cone -expression* that is normalized by the ring tactic (see :ref:`theringandfieldtacticfamilies`) +expression* that is normalized by the :tacn:`ring` tactic (see :ref:`theringandfieldtacticfamilies`) and checked to be :math:`-1`. `lra`: a decision procedure for linear real and rational arithmetic @@ -245,11 +245,11 @@ proof by abstracting monomials by variables. As shown, such a goal is solved by ``intro x. psatz Z 2.``. The oracle returns the cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + -x^2` (polynomial hypotheses are printed in bold). By construction, this expression -belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running `ring` we +belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running :tacn:`ring` we obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. .. [#] Support for `nat` and :math:`\mathbb{N}` is obtained by pre-processing the goal with - the `zify` tactic. + the ``zify`` tactic. .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#] Variants deal with equalities and strict inequalities. .. [#] In practice, the oracle might fail to produce such a refutation. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 3ddfc9aec1..391afcb1f7 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2155,6 +2155,12 @@ If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT language, and can be processed by Graphviz tools. The format is unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. +.. cmdv:: Print Universes Subgraph(@names) + +Prints the graph restricted to the requested names (adjusting +constraints to preserve the implied transitive constraints between +kept universes). + .. _existential-variables: Existential variables diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 741f9fe5b0..0b059f92ee 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -758,18 +758,6 @@ Controlling the effect of proof editing commands available hypotheses. -.. flag:: Automatic Introduction - - This option controls the way binders are handled - in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the - option is on, which is the default, binders are automatically put in - the local context of the goal to prove. - - When the option is off, binders are discharged on the statement to be - proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`) - has to be used to move the assumptions to the local context. - - .. flag:: Nested Proofs Allowed When turned on (it is off by default), this option enables support for nested diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index eacd7b4676..8f76085d88 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -167,7 +167,7 @@ Combined Scheme Combined Scheme tree_forest_mutind from tree_forest_ind,forest_tree_ind. - The type of tree_forest_mutrec will be: + The type of tree_forest_mutind will be: .. coqtop:: all |