From f0f5faa0d02c413f28fb288aa7abfae5d0c807bb Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 27 Apr 2018 01:39:39 +0200 Subject: A few fixes in chapter tactics. --- doc/sphinx/proof-engine/tactics.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index b3537bad80..1ae9e3c724 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -503,7 +503,7 @@ Applying theorems .. tacv:: eapply {+, @term with @bindings_list} in @ident as @intro_pattern. - This works as :tacn:`apply ... in as` but using ``eapply``. + This works as :tacn:`apply ... in ... as` but using ``eapply``. .. tacv:: simple apply @term in @ident @@ -518,8 +518,8 @@ Applying theorems .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} .. tacv:: {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} - This summarizes the different syntactic variants of :n:`apply @term in - @ident` and :n:`eapply @term in @ident`. + This summarizes the different syntactic variants of :n:`apply @term in @ident` + and :n:`eapply @term in @ident`. .. tacn:: constructor @num :name: constructor -- cgit v1.2.3 From 88decfce9eb63c9659e692b41376de7b608e0d43 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 27 Apr 2018 10:38:38 +0200 Subject: Replacing a broken reference by hyperlinks in chapter tactics. --- doc/sphinx/proof-engine/tactics.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 1ae9e3c724..3278bfd47c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -96,10 +96,10 @@ bindings_list`` where ``bindings_list`` may be of two different forms: + A bindings list can also be a simple list of terms :n:`{* term}`. In that case the references to which these terms correspond are - determined by the tactic. In case of ``induction``, ``destruct``, ``elim`` - and ``case`` (see :ref:`ltac`) the terms have to + determined by the tactic. In case of :tacn:`induction`, :tacn:`destruct`, :tacn:`elim` + and :tacn:`case`, the terms have to provide instances for all the dependent products in the type of term while in - the case of ``apply``, or of ``constructor`` and its variants, only instances + the case of :tacn:`apply`, or of :tacn:`constructor` and its variants, only instances for the dependent products that are not bound in the conclusion of the type are required. -- cgit v1.2.3 From 0dc203ee2983594fa064a84739d87f177636f18a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 25 Apr 2018 21:14:59 +0200 Subject: Doc: Some quotes missing in file tactics.rst. --- doc/sphinx/proof-engine/tactics.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 3278bfd47c..064a540ec4 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -632,7 +632,7 @@ context. The new subgoal is :g:`U`. If the goal is a non-dependent product :g:`T`:math:`\rightarrow`:g:`U`, then it puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or -:g:`Prop`) or Xn:T (if the type of :g:`T` is :g:`Type`). The optional index +:g:`Prop`) or :g:`Xn:T` (if the type of :g:`T` is :g:`Type`). The optional index ``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the new subgoal is :g:`U`. -- cgit v1.2.3 From 8f18af6f61f70c0d566bcaba5f8d285e77601f5a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 25 Apr 2018 21:18:10 +0200 Subject: Doc: Moving `\forall` to `forall` in file tactics.rst. Not only are most of "forall"s in the manual in Coq notation, but the math notation leads to have a specially long space after the comma. --- doc/sphinx/proof-engine/tactics.rst | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 064a540ec4..19ab786d15 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -626,7 +626,7 @@ binder. If the goal is a product, the tactic implements the "Lam" rule given in :ref:`Typing-rules` [1]_. If the goal starts with a let binder, then the tactic implements a mix of the "Let" and "Conv". -If the current goal is a dependent product :math:`\forall` :g:`x:T, U` (resp +If the current goal is a dependent product :g:`forall x:T, U` (resp :g:`let x:=t in U`) then ``intro`` puts :g:`x:T` (resp :g:`x:=t`) in the local context. The new subgoal is :g:`U`. @@ -637,11 +637,10 @@ puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or new subgoal is :g:`U`. If the goal is an existential variable, ``intro`` forces the resolution of the -existential variable into a dependent product :math:`\forall`:g:`x:?X, ?Y`, puts +existential variable into a dependent product :math:`forall`:g:`x:?X, ?Y`, puts :g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal allowed to depend on :g:`x`. -If the goal is neither a product, nor starting with a let definition, nor an existential variable, the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can be applied or the goal is not head-reducible. @@ -760,7 +759,7 @@ be applied or the goal is not head-reducible. Assuming a goal of type :g:`Q → P` (non-dependent product), or of type - :math:`\forall`:g:`x:T, P` (dependent product), the behavior of + :g:`forall x:T, P` (dependent product), the behavior of :n:`intros p` is defined inductively over the structure of the introduction pattern :n:`p`: @@ -2153,9 +2152,9 @@ See also: :ref:`advanced-recursive-functions` This variant allows you to specify the generalization of the goal. It is useful when the system fails to generalize the goal automatically. If - :n:`@ident` has type :g:`(I t)` and :g:`I` has type :math:`\forall` - :g:`(x:T), s`, then :n:`@term` must be of type :g:`I:`:math:`\forall` - :g:`(x:T), I x -> s'` where :g:`s'` is the type of the goal. + :n:`@ident` has type :g:`(I t)` and :g:`I` has type :g:`forall (x:T), s`, + then :n:`@term` must be of type :g:`I:forall (x:T), I x -> s'` where + :g:`s'` is the type of the goal. .. tacv:: dependent inversion @ident as @intro_pattern with @term -- cgit v1.2.3 From 9b070738af8fbfb6f76f2963c630414a76817852 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 25 Apr 2018 21:24:37 +0200 Subject: Doc: Renaming an old-style numerical evar in an alphabetical one. --- doc/sphinx/proof-engine/tactics.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 19ab786d15..20a362c4c6 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -511,8 +511,8 @@ Applying theorems on subterms that contain no variables to instantiate. For instance, if :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and :g:`H0 : O = O` then ``simple apply H in H0`` does not succeed because it - would require the conversion of :g:`id ?1234` and :g:`O` where :g:`?1234` is - a variable to instantiate. Tactic :n:`simple apply @term in @ident` does not + would require the conversion of :g:`id ?x` and :g:`O` where :g:`?x` is + an existential variable to instantiate. Tactic :n:`simple apply @term in @ident` does not either traverse tuples as :n:`apply @term in @ident` does. .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} -- cgit v1.2.3