From 211a241f81f80cfc17afc9f1f203a4a5805b8b4a Mon Sep 17 00:00:00 2001 From: Lysxia Date: Sat, 16 Mar 2019 19:01:53 -0400 Subject: [Manual] Improve chapter Type classes, and add mention of Context under Variable - More consistent code indentation - Nest command variants properly - Make `Context` explanation a bit less terse, with more links - Typesetting bits, add some :cmd: links --- doc/sphinx/language/gallina-specification-language.rst | 3 +++ 1 file changed, 3 insertions(+) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 02fb9d84ce..158a3f5ffc 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -639,6 +639,9 @@ has type :token:`type`. parametrized (the variable is *discharged*). Using the :cmd:`Variable` command out of any section is equivalent to using :cmd:`Local Parameter`. + See also :cmd:`Context`, a variant of :cmd:`Variable` where variables can be + made implicit and allowing :ref:`implicit-generalization`. + .. exn:: @ident already exists. :name: @ident already exists. (Variable) :undocumented: -- cgit v1.2.3 From 911a3bf975ddb933acc0f7e17c465005a5ee8465 Mon Sep 17 00:00:00 2001 From: Lysxia Date: Sat, 16 Mar 2019 20:49:02 -0400 Subject: [Manual] Gather section-specific commands in Section documentation (fix #9704) --- doc/sphinx/language/gallina-extensions.rst | 41 +++++++++++++++++++++- .../language/gallina-specification-language.rst | 40 ++++++--------------- 2 files changed, 50 insertions(+), 31 deletions(-) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 59506a6ff2..f2d305f4bc 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -768,7 +768,7 @@ Section :ref:`gallina-definitions`). .. cmd:: End @ident This command closes the section named :token:`ident`. After closing of the - section, the local declarations (variables and local definitions) get + section, the local declarations (variables and local definitions, see :cmd:`Variable`) get *discharged*, meaning that they stop being visible and that all global objects defined in the section are generalized with respect to the variables and local definitions they each depended on in the section. @@ -805,6 +805,45 @@ Section :ref:`gallina-definitions`). Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which appear inside a section are canceled when the section is closed. +.. cmd:: Variable @ident : @type + + This command links :token:`type` to the name :token:`ident` in the context of + the current section (see Section :ref:`section-mechanism` for a description of + the section mechanism). When the current section is closed, name :token:`ident` + will be unknown and every object using this variable will be explicitly + parametrized (the variable is *discharged*). + The :cmd:`Variable` command out of any section is equivalent to :cmd:`Local Parameter`. + + .. exn:: @ident already exists. + :name: @ident already exists. (Variable) + :undocumented: + + .. cmdv:: Variable {+ @ident } : @term + + Links :token:`type` to each :token:`ident`. + + .. cmdv:: Variable {+ ( {+ @ident } : @term ) } + + Adds blocks of variables with different specifications. + + .. cmdv:: Variables {+ ( {+ @ident } : @term) } + Hypothesis {+ ( {+ @ident } : @term) } + Hypotheses {+ ( {+ @ident } : @term) } + :name: Variables; Hypothesis; Hypotheses + + These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @term) }`. + +.. cmd:: Context @binders + + Declare variables in the context of the current section, like :cmd:`Variable`, + but also allowing implicit variables and :ref:`implicit-generalization`. + + .. coqdoc:: + + Context {A : Type} (a b : A). + Context `{EqDec A}. + + See also :ref:`contexts` in the chapter :ref:`typeclasses`. Module system ------------- diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 158a3f5ffc..1c6fb4b193 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -630,36 +630,16 @@ has type :token:`type`. These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. -.. cmd:: Variable @ident : @type - - This command links :token:`type` to the name :token:`ident` in the context of - the current section (see Section :ref:`section-mechanism` for a description of - the section mechanism). When the current section is closed, name :token:`ident` - will be unknown and every object using this variable will be explicitly - parametrized (the variable is *discharged*). Using the :cmd:`Variable` command out - of any section is equivalent to using :cmd:`Local Parameter`. - - See also :cmd:`Context`, a variant of :cmd:`Variable` where variables can be - made implicit and allowing :ref:`implicit-generalization`. - - .. exn:: @ident already exists. - :name: @ident already exists. (Variable) - :undocumented: - - .. cmdv:: Variable {+ @ident } : @term - - Links :token:`type` to each :token:`ident`. - - .. cmdv:: Variable {+ ( {+ @ident } : @term ) } - - Adds blocks of variables with different specifications. - - .. cmdv:: Variables {+ ( {+ @ident } : @term) } - Hypothesis {+ ( {+ @ident } : @term) } - Hypotheses {+ ( {+ @ident } : @term) } - :name: Variables; Hypothesis; Hypotheses - - These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @term) }`. + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + Variables {+ ( {+ @ident } : @type ) } + Hypothesis {+ ( {+ @ident } : @type ) } + Hypotheses {+ ( {+ @ident } : @type ) } + :name: Variable-Parameter; Variables-Parameter; Hypothesis-Parameter; Hypotheses-Parameter + + Out of any section, these variants are synonyms of + :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. + For their meaning inside a section, see the documentation on + :ref:`section-mechanism`. .. note:: It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and -- cgit v1.2.3 From 94f9c0c4b6dd517dc3dca031fbcb9ff455309d19 Mon Sep 17 00:00:00 2001 From: Lysxia Date: Sun, 17 Mar 2019 19:15:22 -0400 Subject: [Manual] Move doc on Let into Section mechanism, and more polishing - Put "Section mechanism" example earlier --- doc/sphinx/language/gallina-extensions.rst | 91 +++++++++++++++------- .../language/gallina-specification-language.rst | 43 +++++----- 2 files changed, 80 insertions(+), 54 deletions(-) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index f2d305f4bc..398ad4833d 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -754,49 +754,60 @@ used by ``Function``. A more precise description is given below. Section mechanism ----------------- -The sectioning mechanism can be used to to organize a proof in -structured sections. Then local declarations become available (see -Section :ref:`gallina-definitions`). +Sections create local contexts which can be shared across multiple definitions. +.. example:: -.. cmd:: Section @ident + Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`. - This command is used to open a section named :token:`ident`. - Section names do not need to be unique. + .. coqtop:: all + Section s1. -.. cmd:: End @ident + Inside a section, local parameters can be introduced using :cmd:`Variable`, + :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for + the former two). - This command closes the section named :token:`ident`. After closing of the - section, the local declarations (variables and local definitions, see :cmd:`Variable`) get - *discharged*, meaning that they stop being visible and that all global - objects defined in the section are generalized with respect to the - variables and local definitions they each depended on in the section. + .. coqtop:: all - .. example:: + Variables x y : nat. - .. coqtop:: all + The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions + won't persist when the section is closed, and all persistent definitions which + depend on `y'` will be prefixed with `let y' := y in`. - Section s1. + .. coqtop:: in - Variables x y : nat. + Let y' := y. + Definition x' := S x. + Definition x'' := x' + y'. - Let y' := y. + .. coqtop:: all - Definition x' := S x. + Print x'. + Print x''. - Definition x'' := x' + y'. + End s1. - Print x'. + Print x'. + Print x''. - End s1. + Notice the difference between the value of :g:`x'` and :g:`x''` inside section + :g:`s1` and outside. + +.. cmd:: Section @ident + + This command is used to open a section named :token:`ident`. + Section names do not need to be unique. - Print x'. - Print x''. +.. cmd:: End @ident - Notice the difference between the value of :g:`x'` and :g:`x''` inside section - :g:`s1` and outside. + This command closes the section named :token:`ident`. After closing of the + section, the local declarations (variables and local definitions, see :cmd:`Variable`) get + *discharged*, meaning that they stop being visible and that all global + objects defined in the section are generalized with respect to the + variables and local definitions they each depended on in the section. .. exn:: This is not the last opened section. :undocumented: @@ -808,11 +819,9 @@ Section :ref:`gallina-definitions`). .. cmd:: Variable @ident : @type This command links :token:`type` to the name :token:`ident` in the context of - the current section (see Section :ref:`section-mechanism` for a description of - the section mechanism). When the current section is closed, name :token:`ident` + the current section. When the current section is closed, name :token:`ident` will be unknown and every object using this variable will be explicitly parametrized (the variable is *discharged*). - The :cmd:`Variable` command out of any section is equivalent to :cmd:`Local Parameter`. .. exn:: @ident already exists. :name: @ident already exists. (Variable) @@ -843,7 +852,31 @@ Section :ref:`gallina-definitions`). Context {A : Type} (a b : A). Context `{EqDec A}. - See also :ref:`contexts` in the chapter :ref:`typeclasses`. +.. seealso:: Section :ref:`contexts` in chapter :ref:`typeclasses`. + +.. cmd:: Let @ident := @term + + This command binds the value :token:`term` to the name :token:`ident` in the + environment of the current section. The name :token:`ident` disappears when the + current section is eventually closed, and all persistent definitions and + theorems within the section and depending on :token:`ident` are + prefixed by the let-in definition :n:`let @ident := @term in`. + + .. exn:: @ident already exists. + :name: @ident already exists. (Let) + :undocumented: + + .. cmdv:: Let @ident {? @binders } {? : @type } := @term + :undocumented: + + .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body} + :name: Let Fixpoint + :undocumented: + + .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body} + :name: Let CoFixpoint + :undocumented: + Module system ------------- diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 1c6fb4b193..67e59768d6 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -634,13 +634,18 @@ has type :token:`type`. Variables {+ ( {+ @ident } : @type ) } Hypothesis {+ ( {+ @ident } : @type ) } Hypotheses {+ ( {+ @ident } : @type ) } - :name: Variable-Parameter; Variables-Parameter; Hypothesis-Parameter; Hypotheses-Parameter + :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section) Out of any section, these variants are synonyms of :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. - For their meaning inside a section, see the documentation on + For their meaning inside a section, see :cmd:`Variable` in :ref:`section-mechanism`. + .. warn:: @ident is declared as a local axiom [local-declaration,scope] + + Warning that is emitted when using :cmd:`Variable` instead of + :cmd:`Local Parameter`. + .. note:: It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and :cmd:`Hypothesis` (and their plural forms) for logical postulates (i.e. when @@ -648,6 +653,8 @@ has type :token:`type`. :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases (corresponding to the declaration of an abstract mathematical entity). +.. seealso:: Section :ref:`section-mechanism`. + .. _gallina-definitions: Definitions @@ -704,32 +711,18 @@ Section :ref:`typing-rules`. This is equivalent to :cmd:`Definition`. -.. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. - -.. cmd:: Let @ident := @term - - This command binds the value :token:`term` to the name :token:`ident` in the - environment of the current section. The name :token:`ident` disappears when the - current section is eventually closed, and all persistent objects (such - as theorems) defined within the section and depending on :token:`ident` are - prefixed by the let-in definition :n:`let @ident := @term in`. - Using the :cmd:`Let` command out of any section is equivalent to using - :cmd:`Local Definition`. - - .. exn:: @ident already exists. - :name: @ident already exists. (Let) - :undocumented: + .. cmdv:: Let @ident := @term + :name: Let (outside a section) - .. cmdv:: Let @ident {? @binders } {? : @type } := @term - :undocumented: + Out of any section, this variant is a synonym of + :n:`Local Definition @ident := @term`. + For its meaning inside a section, see :cmd:`Let` in + :ref:`section-mechanism`. - .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body} - :name: Let Fixpoint - :undocumented: + .. warn:: @ident is declared as a local definition [local-declaration,scope] - .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body} - :name: Let CoFixpoint - :undocumented: + Warning that is emitted when using :cmd:`Let` instead of + :cmd:`Local Definition`. .. seealso:: Section :ref:`section-mechanism`, commands :cmd:`Opaque`, :cmd:`Transparent`, and tactic :tacn:`unfold`. -- cgit v1.2.3 From b64dc640d2af26b1ccf2524c1050c16f57d2be35 Mon Sep 17 00:00:00 2001 From: Lysxia Date: Mon, 18 Mar 2019 08:20:10 -0400 Subject: [Manual] Move command Context after Let, and more polishing - Refine some `@term` into `@type` --- doc/sphinx/language/gallina-extensions.rst | 51 +++++++++++----------- .../language/gallina-specification-language.rst | 12 ++--- 2 files changed, 32 insertions(+), 31 deletions(-) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 398ad4833d..497504e706 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -766,7 +766,7 @@ Sections create local contexts which can be shared across multiple definitions. Inside a section, local parameters can be introduced using :cmd:`Variable`, :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for - the former two). + the first two). .. coqtop:: all @@ -827,40 +827,28 @@ Sections create local contexts which can be shared across multiple definitions. :name: @ident already exists. (Variable) :undocumented: - .. cmdv:: Variable {+ @ident } : @term + .. cmdv:: Variable {+ @ident } : @type Links :token:`type` to each :token:`ident`. - .. cmdv:: Variable {+ ( {+ @ident } : @term ) } + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } - Adds blocks of variables with different specifications. + Declare one or more variables with various types. - .. cmdv:: Variables {+ ( {+ @ident } : @term) } - Hypothesis {+ ( {+ @ident } : @term) } - Hypotheses {+ ( {+ @ident } : @term) } + .. cmdv:: Variables {+ ( {+ @ident } : @type) } + Hypothesis {+ ( {+ @ident } : @type) } + Hypotheses {+ ( {+ @ident } : @type) } :name: Variables; Hypothesis; Hypotheses - These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @term) }`. - -.. cmd:: Context @binders - - Declare variables in the context of the current section, like :cmd:`Variable`, - but also allowing implicit variables and :ref:`implicit-generalization`. - - .. coqdoc:: - - Context {A : Type} (a b : A). - Context `{EqDec A}. - -.. seealso:: Section :ref:`contexts` in chapter :ref:`typeclasses`. + These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. .. cmd:: Let @ident := @term This command binds the value :token:`term` to the name :token:`ident` in the - environment of the current section. The name :token:`ident` disappears when the - current section is eventually closed, and all persistent definitions and - theorems within the section and depending on :token:`ident` are - prefixed by the let-in definition :n:`let @ident := @term in`. + environment of the current section. The name :token:`ident` is accessible + only within the current section. When the section is closed, all persistent + definitions and theorems within it and depending on :token:`ident` + will be prefixed by the let-in definition :n:`let @ident := @term in`. .. exn:: @ident already exists. :name: @ident already exists. (Let) @@ -877,6 +865,19 @@ Sections create local contexts which can be shared across multiple definitions. :name: Let CoFixpoint :undocumented: +.. cmd:: Context @binders + + Declare variables in the context of the current section, like :cmd:`Variable`, + but also allowing implicit variables, :ref:`implicit-generalization`, and + let-binders. + + .. coqdoc:: + + Context {A : Type} (a b : A). + Context `{EqDec A}. + Context (b' := b). + +.. seealso:: Section :ref:`binders`. Section :ref:`contexts` in chapter :ref:`typeclasses`. Module system ------------- @@ -2100,7 +2101,7 @@ or :g:`m` to the type :g:`nat` of natural numbers). This is useful for declaring the implicit type of a single variable. -.. cmdv:: Implicit Types {+ ( {+ @ident } : @term ) } +.. cmdv:: Implicit Types {+ ( {+ @ident } : @type ) } Adds blocks of implicit types with different specifications. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 67e59768d6..e67f53c950 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -636,14 +636,14 @@ has type :token:`type`. Hypotheses {+ ( {+ @ident } : @type ) } :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section) - Out of any section, these variants are synonyms of + Outside of any section, these variants are synonyms of :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. For their meaning inside a section, see :cmd:`Variable` in :ref:`section-mechanism`. .. warn:: @ident is declared as a local axiom [local-declaration,scope] - Warning that is emitted when using :cmd:`Variable` instead of + Warning generated when using :cmd:`Variable` instead of :cmd:`Local Parameter`. .. note:: @@ -694,10 +694,10 @@ Section :ref:`typing-rules`. .. exn:: The term @term has type @type while it is expected to have type @type'. :undocumented: - .. cmdv:: Definition @ident @binders {? : @term } := @term + .. cmdv:: Definition @ident @binders {? : @type } := @term This is equivalent to - :n:`Definition @ident : forall @binders, @term := fun @binders => @term`. + :n:`Definition @ident : forall @binders, @type := fun @binders => @term`. .. cmdv:: Local Definition @ident {? @binders } {? : @type } := @term :name: Local Definition @@ -714,14 +714,14 @@ Section :ref:`typing-rules`. .. cmdv:: Let @ident := @term :name: Let (outside a section) - Out of any section, this variant is a synonym of + Outside of any section, this variant is a synonym of :n:`Local Definition @ident := @term`. For its meaning inside a section, see :cmd:`Let` in :ref:`section-mechanism`. .. warn:: @ident is declared as a local definition [local-declaration,scope] - Warning that is emitted when using :cmd:`Let` instead of + Warning generated when using :cmd:`Let` instead of :cmd:`Local Definition`. .. seealso:: Section :ref:`section-mechanism`, commands :cmd:`Opaque`, -- cgit v1.2.3 From e7ddf978adbf441d34b8c17502caaa05ee8da04b Mon Sep 17 00:00:00 2001 From: Lysxia Date: Mon, 18 Mar 2019 08:20:10 -0400 Subject: [Manual] Parametrize -> ParametErize - Refine some `@term` into `@type` --- doc/sphinx/language/gallina-extensions.rst | 2 +- doc/sphinx/language/gallina-specification-language.rst | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 497504e706..18cafd1f21 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -821,7 +821,7 @@ Sections create local contexts which can be shared across multiple definitions. This command links :token:`type` to the name :token:`ident` in the context of the current section. When the current section is closed, name :token:`ident` will be unknown and every object using this variable will be explicitly - parametrized (the variable is *discharged*). + parameterized (the variable is *discharged*). .. exn:: @ident already exists. :name: @ident already exists. (Variable) diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index e67f53c950..8a5e9d87f8 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -853,8 +853,8 @@ which is a type whose conclusion is a sort. successor :g:`(S (S n))` satisfies also :g:`P`. This is indeed analogous to the structural induction principle we got for :g:`nat`. -Parametrized inductive types -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Parameterized inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmdv:: Inductive @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type} @@ -930,7 +930,7 @@ Parametrized inductive types because the conclusion of the type of constructors should be :g:`listw A` in both cases. - + A parametrized inductive definition can be defined using annotations + + A parameterized inductive definition can be defined using annotations instead of parameters but it will sometimes give a different (bigger) sort for the inductive definition and will produce a less convenient rule for case elimination. @@ -990,7 +990,7 @@ Mutually defined inductive types .. cmdv:: Inductive @ident @binders {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident @binders {? : @type } } } - In this variant, the inductive definitions are parametrized + In this variant, the inductive definitions are parameterized with :token:`binders`. However, parameters correspond to a local context in which the whole set of inductive declarations is done. For this reason, the parameters must be strictly the same for each inductive types. @@ -1026,7 +1026,7 @@ Mutually defined inductive types Check forest_rec. - Assume we want to parametrize our mutual inductive definitions with the + Assume we want to parameterize our mutual inductive definitions with the two type variables :g:`A` and :g:`B`, the declaration should be done the following way: -- cgit v1.2.3