diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 35 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 25 |
3 files changed, 57 insertions, 5 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 67683902cd..962d2a94e3 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -51,7 +51,7 @@ function types over these data types. Consequently they also have a type. Because assuming simply that :math:`\Set` has type :math:`\Set` leads to an inconsistent theory :cite:`Coq86`, the language of |Cic| has infinitely many sorts. There are, in addition to :math:`\Set` and :math:`\Prop` -a hierarchy of universes :math:`\Type(i)` for any integer :math:`i`. +a hierarchy of universes :math:`\Type(i)` for any integer :math:`i ≥ 1`. Like :math:`\Set`, all of the sorts :math:`\Type(i)` contain small sets such as booleans, natural numbers, as well as products, subsets and function diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 590d71b5f3..24645a8cc3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -346,11 +346,46 @@ Navigation in the proof tree Goals are just existential variables and existential variables do not get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`. + You may also wrap this in an Ltac-definition like: + + .. coqtop:: in + + Ltac name_goal name := refine ?[name]. .. seealso:: :ref:`existential-variables` .. example:: + This first example uses the Ltac definition above, and the named goals + only serve for documentation. + + .. coqtop:: all + + Goal forall n, n + 0 = n. + Proof. + induction n; [ name_goal base | name_goal step ]. + [base]: { + + .. coqtop:: all + + reflexivity. + + .. coqtop:: in + + } + + .. coqtop:: all + + [step]: { + + .. coqtop:: all + + simpl. + f_equal. + assumption. + } + Qed. + This can also be a way of focusing on a shelved goal, for instance: .. coqtop:: all diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 7eef504ea9..081fef07b9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3307,12 +3307,29 @@ the conversion in hypotheses :n:`{+ @ident}`. :name: fold This tactic applies to any goal. The term :n:`@term` is reduced using the - ``red`` tactic. Every occurrence of the resulting :n:`@term` in the goal is - then replaced by :n:`@term`. + :tacn:`red` tactic. Every occurrence of the resulting :n:`@term` in the goal is + then replaced by :n:`@term`. This tactic is particularly useful when a fixpoint + definition has been wrongfully unfolded, making the goal very hard to read. + On the other hand, when an unfolded function applied to its argument has been + reduced, the :tacn:`fold` tactic won't do anything. -.. tacv:: fold {+ @term} + .. example:: + + .. coqtop:: all + + Goal ~0=0. + unfold not. + Fail progress fold not. + pattern (0 = 0). + fold not. + + .. coqtop:: none + + Abort. + + .. tacv:: fold {+ @term} - Equivalent to :n:`fold @term ; ... ; fold @term`. + Equivalent to :n:`fold @term ; ... ; fold @term`. .. tacn:: pattern @term :name: pattern |