Documentation of branch “v8.20” at 39774e3a

v8.20/refman/_sources/proofs/automatic-tactics/auto.rst.txt

@@ -405,10 +405,6 @@ Creating Hints
    + :attr:`global` hints are visible from other modules when they :cmd:`Import` or
      :cmd:`Require` the current module.
 
-   .. versionadded:: 8.14
-
-      The :cmd:`Hint Rewrite` now supports locality attributes like other `Hint` commands.
-
    .. versionchanged:: 8.18
 
       The default value for hint locality outside sections is
@@ -519,11 +515,13 @@ Creating Hints
       :tacn:`unfold`. :n:`@natural` is the cost, :n:`@one_pattern` is the pattern
       to match and :n:`@ltac_expr` is the action to apply.
 
-      .. note::
+      **Usage tip**: tactics that can succeed even if they don't change the context,
+      such as most of the :ref:`conversion tactics <applyingconversionrules>`, should
+      be prefaced with :tacn:`progress` to avoid needless repetition of the tactic.
 
-         Use a :cmd:`Hint Extern` with no pattern to do
-         pattern matching on hypotheses using ``match goal with``
-         inside the tactic.
+      **Usage tip**: Use a :cmd:`Hint Extern` with no pattern to do
+      pattern matching on hypotheses using ``match goal with``
+      inside the tactic.
 
       .. example::
 

v8.20/refman/_sources/proofs/writing-proofs/equality.rst.txt

@@ -456,6 +456,9 @@ Tactics described in this section include:
   term
 - :tacn:`vm_compute` and :tacn:`native_compute`, which are performance-oriented.
 
+Except for :tacn:`red`, conversion tactics succeed even if the context is left
+unchanged.
+
 Conversion tactics, with two exceptions, only change the types and contexts
 of existential variables
 and leave the proof term unchanged.  (The :tacn:`vm_compute` and :tacn:`native_compute`

v8.20/refman/proof-engine/ltac.html

@@ -3374,7 +3374,7 @@ <h3>Timing a tactic that evaluates to a term: time_constr<a class="headerlink" h
   </span><span class="coqdoc-tactic">pose</span><span> </span><span class="coqdoc-var">v</span><span>.</span><span>
 </span></dt><dd><span>Tactic evaluation (depth 1) ran for 0. secs (0.u,0.s)
 Tactic evaluation (depth 1) ran for 0. secs (0.u,0.s)
-Tactic evaluation ran for 0. secs (0.u,0.s)
+Tactic evaluation ran for 0.001 secs (0.u,0.s)
 1 goal
 
   n := 100 : nat
@@ -4288,40 +4288,40 @@ <h3>Profiling <code class="docutils literal notranslate"><span class="pre">L</sp
 </span></dt><dd><span>No more goals.
 </span></dd>
 <dt><span></span><span class="coqdoc-keyword">Show</span><span> </span><span class="coqdoc-keyword">Ltac</span><span> </span><span class="coqdoc-var">Profile</span><span>.</span><span>
-</span></dt><dd><span>total time:      1.721s
+</span></dt><dd><span>total time:      1.162s
 
  tactic                                  local  total   calls       max
 ───────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac ----------------------------------   5.1% 100.0%       1    1.721s
-─&lt;Coq.Init.Tauto.with_uniform_flags&gt; --   0.0%  92.0%      26    0.204s
-─&lt;Coq.Init.Tauto.tauto_gen&gt; -----------   0.0%  92.0%      26    0.204s
-─&lt;Coq.Init.Tauto.tauto_intuitionistic&gt;    0.0%  91.9%      26    0.204s
-─t_tauto_intuit -----------------------   0.1%  91.8%      26    0.204s
-─&lt;Coq.Init.Tauto.simplif&gt; -------------  58.8%  89.0%      26    0.202s
-─&lt;Coq.Init.Tauto.is_conj&gt; -------------  20.7%  20.7%   28756    0.053s
-─elim id ------------------------------   6.2%   6.2%     650    0.014s
-─&lt;Coq.Init.Tauto.axioms&gt; --------------   2.0%   2.8%       0    0.003s
-─lia ----------------------------------   0.1%   2.4%      28    0.020s
+─tac ----------------------------------   4.1% 100.0%       1    1.162s
+─&lt;Coq.Init.Tauto.with_uniform_flags&gt; --   0.0%  93.4%      26    0.119s
+─&lt;Coq.Init.Tauto.tauto_gen&gt; -----------   0.0%  93.3%      26    0.119s
+─&lt;Coq.Init.Tauto.tauto_intuitionistic&gt;    0.0%  93.3%      26    0.119s
+─t_tauto_intuit -----------------------   0.1%  93.2%      26    0.119s
+─&lt;Coq.Init.Tauto.simplif&gt; -------------  58.0%  90.1%      26    0.118s
+─&lt;Coq.Init.Tauto.is_conj&gt; -------------  23.2%  23.2%   28756    0.032s
+─elim id ------------------------------   5.6%   5.6%     650    0.010s
+─&lt;Coq.Init.Tauto.axioms&gt; --------------   2.0%   3.0%       0    0.001s
+─lia ----------------------------------   0.1%   2.2%      28    0.012s
 
  tactic                                    local  total   calls       max
 ─────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac ------------------------------------   5.1% 100.0%       1    1.721s
- ├─&lt;Coq.Init.Tauto.with_uniform_flags&gt; --   0.0%  92.0%      26    0.204s
- │└&lt;Coq.Init.Tauto.tauto_gen&gt; -----------   0.0%  92.0%      26    0.204s
- │└&lt;Coq.Init.Tauto.tauto_intuitionistic&gt;    0.0%  91.9%      26    0.204s
- │└t_tauto_intuit -----------------------   0.1%  91.8%      26    0.204s
- │ ├─&lt;Coq.Init.Tauto.simplif&gt; -----------  58.8%  89.0%      26    0.202s
- │ │ ├─&lt;Coq.Init.Tauto.is_conj&gt; ---------  20.7%  20.7%   28756    0.053s
- │ │ └─elim id --------------------------   6.2%   6.2%     650    0.014s
- │ └─&lt;Coq.Init.Tauto.axioms&gt; ------------   2.0%   2.8%       0    0.003s
- └─lia ----------------------------------   0.1%   2.4%      28    0.020s
+─tac ------------------------------------   4.1% 100.0%       1    1.162s
+ ├─&lt;Coq.Init.Tauto.with_uniform_flags&gt; --   0.0%  93.4%      26    0.119s
+ │└&lt;Coq.Init.Tauto.tauto_gen&gt; -----------   0.0%  93.3%      26    0.119s
+ │└&lt;Coq.Init.Tauto.tauto_intuitionistic&gt;    0.0%  93.3%      26    0.119s
+ │└t_tauto_intuit -----------------------   0.1%  93.2%      26    0.119s
+ │ ├─&lt;Coq.Init.Tauto.simplif&gt; -----------  58.0%  90.1%      26    0.118s
+ │ │ ├─&lt;Coq.Init.Tauto.is_conj&gt; ---------  23.2%  23.2%   28756    0.032s
+ │ │ └─elim id --------------------------   5.6%   5.6%     650    0.010s
+ │ └─&lt;Coq.Init.Tauto.axioms&gt; ------------   2.0%   3.0%       0    0.001s
+ └─lia ----------------------------------   0.1%   2.2%      28    0.012s
 </span></dd>
 <dt><span></span><span class="coqdoc-keyword">Show</span><span> </span><span class="coqdoc-keyword">Ltac</span><span> </span><span class="coqdoc-var">Profile</span><span> &quot;lia&quot;.</span><span>
-</span></dt><dd><span>total time:      1.721s
+</span></dt><dd><span>total time:      1.162s
 
  tactic  local  total   calls       max
 ───────┴──────┴──────┴───────┴─────────┘
-─lia --   0.1%   2.4%      28    0.020s
+─lia --   0.1%   2.2%      28    0.012s
 
  tactic  local  total   calls       max
 ───────┴──────┴──────┴───────┴─────────┘

v8.20/refman/proofs/automatic-tactics/auto.html

@@ -1722,9 +1722,6 @@ <h3>Hint databases defined in the Coq standard library<a class="headerlink" href
 <li><p><a class="reference internal" href="../../language/core/modules.html#coq:attr.global" title="global"><code class="xref coq coq-attr docutils literal notranslate"><span class="pre">global</span></code></a> hints are visible from other modules when they <a class="reference internal" href="../../language/core/modules.html#coq:cmd.Import" title="Import"><code class="xref coq coq-cmd docutils literal notranslate"><span class="pre">Import</span></code></a> or
 <a class="reference internal" href="../../proof-engine/vernacular-commands.html#coq:cmd.Require" title="Require"><code class="xref coq coq-cmd docutils literal notranslate"><span class="pre">Require</span></code></a> the current module.</p></li>
 </ul>
-<div class="versionadded">
-<p><span class="versionmodified added">New in version 8.14: </span>The <a class="reference internal" href="#coq:cmd.Hint-Rewrite" title="Hint Rewrite"><code class="xref coq coq-cmd docutils literal notranslate"><span class="pre">Hint</span> <span class="pre">Rewrite</span></code></a> now supports locality attributes like other <code class="docutils literal notranslate"><span class="pre">Hint</span></code> commands.</p>
-</div>
 <div class="versionchanged">
 <p><span class="versionmodified changed">Changed in version 8.18: </span>The default value for hint locality outside sections is
 now <a class="reference internal" href="../../language/core/modules.html#coq:attr.export" title="export"><code class="xref coq coq-attr docutils literal notranslate"><span class="pre">export</span></code></a>. It used to be <a class="reference internal" href="../../language/core/modules.html#coq:attr.global" title="global"><code class="xref coq coq-attr docutils literal notranslate"><span class="pre">global</span></code></a>.</p>
@@ -1845,12 +1842,12 @@ <h3>Hint databases defined in the Coq standard library<a class="headerlink" href
 <dd><p>Extends <a class="reference internal" href="#coq:tacn.auto" title="auto"><code class="xref coq coq-tacn docutils literal notranslate"><span class="pre">auto</span></code></a> with tactics other than <a class="reference internal" href="../../proof-engine/tactics.html#coq:tacn.apply" title="apply"><code class="xref coq coq-tacn docutils literal notranslate"><span class="pre">apply</span></code></a> and
 <a class="reference internal" href="../writing-proofs/equality.html#coq:tacn.unfold" title="unfold"><code class="xref coq coq-tacn docutils literal notranslate"><span class="pre">unfold</span></code></a>. <code class="docutils literal notranslate"><span class="notation"><a class="reference internal" href="../../language/core/basic.html#grammar-token-natural"><span class="hole"><span class="pre">natural</span></span></a></span></code> is the cost, <code class="docutils literal notranslate"><span class="notation"><a class="reference internal" href="#grammar-token-one_pattern"><span class="hole"><span class="pre">one_pattern</span></span></a></span></code> is the pattern
 to match and <code class="docutils literal notranslate"><span class="notation"><a class="reference internal" href="../../proof-engine/ltac.html#grammar-token-ltac_expr"><span class="hole"><span class="pre">ltac_expr</span></span></a></span></code> is the action to apply.</p>
-<div class="admonition note">
-<p class="admonition-title">Note</p>
-<p>Use a <a class="reference internal" href="#coq:cmd.Hint-Extern" title="Hint Extern"><code class="xref coq coq-cmd docutils literal notranslate"><span class="pre">Hint</span> <span class="pre">Extern</span></code></a> with no pattern to do
+<p><strong>Usage tip</strong>: tactics that can succeed even if they don't change the context,
+such as most of the <a class="reference internal" href="../writing-proofs/equality.html#applyingconversionrules"><span class="std std-ref">conversion tactics</span></a>, should
+be prefaced with <a class="reference internal" href="../../proof-engine/ltac.html#coq:tacn.progress" title="progress"><code class="xref coq coq-tacn docutils literal notranslate"><span class="pre">progress</span></code></a> to avoid needless repetition of the tactic.</p>
+<p><strong>Usage tip</strong>: Use a <a class="reference internal" href="#coq:cmd.Hint-Extern" title="Hint Extern"><code class="xref coq coq-cmd docutils literal notranslate"><span class="pre">Hint</span> <span class="pre">Extern</span></code></a> with no pattern to do
 pattern matching on hypotheses using <code class="docutils literal notranslate"><span class="pre">match</span> <span class="pre">goal</span> <span class="pre">with</span></code>
 inside the tactic.</p>
-</div>
 <div class="admonition note">
 <p class="admonition-title">Example</p>
 <div class="coqtop literal-block docutils container">

v8.20/refman/proofs/writing-proofs/equality.html

@@ -1820,6 +1820,8 @@ <h2>Rewriting with definitional equality<a class="headerlink" href="#rewriting-w
 term</p></li>
 <li><p><a class="reference internal" href="#coq:tacn.vm_compute" title="vm_compute"><code class="xref coq coq-tacn docutils literal notranslate"><span class="pre">vm_compute</span></code></a> and <a class="reference internal" href="#coq:tacn.native_compute" title="native_compute"><code class="xref coq coq-tacn docutils literal notranslate"><span class="pre">native_compute</span></code></a>, which are performance-oriented.</p></li>
 </ul>
+<p>Except for <a class="reference internal" href="#coq:tacn.red" title="red"><code class="xref coq coq-tacn docutils literal notranslate"><span class="pre">red</span></code></a>, conversion tactics succeed even if the context is left
+unchanged.</p>
 <p>Conversion tactics, with two exceptions, only change the types and contexts
 of existential variables
 and leave the proof term unchanged.  (The <a class="reference internal" href="#coq:tacn.vm_compute" title="vm_compute"><code class="xref coq coq-tacn docutils literal notranslate"><span class="pre">vm_compute</span></code></a> and <a class="reference internal" href="#coq:tacn.native_compute" title="native_compute"><code class="xref coq coq-tacn docutils literal notranslate"><span class="pre">native_compute</span></code></a>
@@ -2619,15 +2621,15 @@ <h3>Computing in a term: eval and Eval<a class="headerlink" href="#computing-in-
   True
 </span></dd>
 <dt><span></span><span class="coqdoc-keyword">Time</span><span> </span><span class="coqdoc-tactic">assert</span><span> (</span><span class="coqdoc-var">id</span><span> (</span><span class="coqdoc-var">fact</span><span> 8) = </span><span class="coqdoc-var">fact</span><span> 8) </span><span class="coqdoc-tactic">by</span><span> </span><span class="coqdoc-tactic">reflexivity</span><span>.</span><span>
-</span></dt><dd><span>Finished transaction in 0.295 secs (0.184u,0.096s) (successful)
+</span></dt><dd><span>Finished transaction in 0.181 secs (0.159u,0.022s) (successful)
 1 goal
 
   H : id (fact 8)</span><span> =</span><span> fact 8
   ============================
   True
 </span></dd>
 <dt><span></span><span class="coqdoc-keyword">Time</span><span> </span><span class="coqdoc-tactic">assert</span><span> (</span><span class="coqdoc-var">id</span><span> (</span><span class="coqdoc-var">fact</span><span> 9) = </span><span class="coqdoc-var">fact</span><span> 9) </span><span class="coqdoc-tactic">by</span><span> </span><span class="coqdoc-tactic">reflexivity</span><span>.</span><span>
-</span></dt><dd><span>Finished transaction in 1.121 secs (1.079u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 1.042 secs (1.038u,0.004s) (successful)
 1 goal
 
   H : id (fact 8)</span><span> =</span><span> fact 8
@@ -2655,7 +2657,7 @@ <h3>Computing in a term: eval and Eval<a class="headerlink" href="#computing-in-
 Timeout!
 </span></dd>
 <dt><span></span><span class="coqdoc-keyword">Time</span><span> </span><span class="coqdoc-tactic">assert</span><span> (</span><span class="coqdoc-var">id</span><span> (</span><span class="coqdoc-var">fact</span><span> 100) = </span><span class="coqdoc-var">fact</span><span> 100) </span><span class="coqdoc-tactic">by</span><span> </span><span class="coqdoc-var">with_strategy</span><span> -1 [</span><span class="coqdoc-var">id</span><span>] </span><span class="coqdoc-tactic">reflexivity</span><span>.</span><span>
-</span></dt><dd><span>Finished transaction in 0.002 secs (0.002u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 0.001 secs (0.001u,0.s) (successful)
 1 goal
 
   H : id (fact 100)</span><span> =</span><span> fact 100
@@ -2690,7 +2692,7 @@ <h3>Computing in a term: eval and Eval<a class="headerlink" href="#computing-in-
   True
 </span></dd>
 <dt><span></span><span class="coqdoc-keyword">Time</span><span> </span><span class="coqdoc-tactic">assert</span><span> (</span><span class="coqdoc-var">id</span><span> (</span><span class="coqdoc-var">fact</span><span> 100) = </span><span class="coqdoc-var">fact</span><span> 100) </span><span class="coqdoc-tactic">by</span><span> </span><span class="coqdoc-var">with_strategy</span><span> -1 [</span><span class="coqdoc-var">id</span><span>] </span><span class="coqdoc-tactic">abstract</span><span> </span><span class="coqdoc-tactic">reflexivity</span><span>.</span><span>
-</span></dt><dd><span>Finished transaction in 0.003 secs (0.003u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 0.001 secs (0.001u,0.s) (successful)
 1 goal
 
   H : id (fact 100)</span><span> =</span><span> fact 100
@@ -2701,7 +2703,7 @@ <h3>Computing in a term: eval and Eval<a class="headerlink" href="#computing-in-
 </span></dt><dd><span>No more goals.
 </span></dd>
 <dt><span></span><span class="coqdoc-keyword">Time</span><span> </span><span class="coqdoc-keyword">Defined</span><span>.</span><span>
-</span></dt><dd><span>Finished transaction in 0.001 secs (0.001u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 0. secs (0.u,0.s) (successful)
 </span></dd>
 </dl>
 </div>