From bdf65b2516b0dd5f4e1a1c6130fc49ee7712dd07 Mon Sep 17 00:00:00 2001 From: Zeimer Date: Sat, 14 Jul 2018 14:20:25 +0200 Subject: Fixed some typos and grammar errors from section 'The language' of the Reference Manual. Removed all mentions of prodT because it is no longer a separate inductive definition (prod has been living in Type for some time) but rather only a notation for prod needed for compatibility purposes. --- doc/sphinx/language/cic.rst | 12 ++++++------ doc/sphinx/language/coq-library.rst | 5 +---- doc/sphinx/language/gallina-extensions.rst | 2 +- 3 files changed, 8 insertions(+), 11 deletions(-) diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index b01a4ef0f..98e81ebc6 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1175,7 +1175,7 @@ ourselves to primitive recursive functions and functionals. For instance, assuming a parameter :g:`A:Set` exists in the local context, we want to build a function length of type :g:`list A -> nat` which computes -the length of the list, so such that :g:`(length (nil A)) = O` and :g:`(length +the length of the list, such that :g:`(length (nil A)) = O` and :g:`(length (cons A a l)) = (S (length l))`. We want these equalities to be recognized implicitly and taken into account in the conversion rule. @@ -1364,7 +1364,7 @@ irrelevance property which is sometimes a useful axiom: The elimination of an inductive definition of type :math:`\Prop` on a predicate :math:`P` of type :math:`I→ Type` leads to a paradox when applied to impredicative inductive definition like the second-order existential quantifier -:g:`exProp` defined above, because it give access to the two projections on +:g:`exProp` defined above, because it gives access to the two projections on this type. @@ -1613,7 +1613,7 @@ then the recursive arguments will correspond to :math:`T_i` in which one of the :math:`I_l` occurs. The main rules for being structurally smaller are the following. -Given a variable :math:`y` of type an inductive definition in a declaration +Given a variable :math:`y` of an inductively defined type in a declaration :math:`\ind{r}{Γ_I}{Γ_C}` where :math:`Γ_I` is :math:`[I_1 :A_1 ;…;I_k :A_k]`, and :math:`Γ_C` is :math:`[c_1 :C_1 ;…;c_n :C_n ]`, the terms structurally smaller than :math:`y` are: @@ -1625,7 +1625,7 @@ Given a variable :math:`y` of type an inductive definition in a declaration Each :math:`f_i` corresponds to a type of constructor :math:`C_q ≡ ∀ p_1 :P_1 ,…,∀ p_r :P_r , ∀ y_1 :B_1 , … ∀ y_k :B_k , (I~a_1 … a_k )` and can consequently be written :math:`λ y_1 :B_1' . … λ y_k :B_k'. g_i`. (:math:`B_i'` is - obtained from :math:`B_i` by substituting parameters variables) the variables + obtained from :math:`B_i` by substituting parameters for variables) the variables :math:`y_j` occurring in :math:`g_i` corresponding to recursive arguments :math:`B_i` (the ones in which one of the :math:`I_l` occurs) are structurally smaller than y. @@ -1801,7 +1801,7 @@ definitions can be found in :cite:`Gimenez95b,Gim98,GimCas05`. .. _The-Calculus-of-Inductive-Construction-with-impredicative-Set: -The Calculus of Inductive Construction with impredicative Set +The Calculus of Inductive Constructions with impredicative Set ----------------------------------------------------------------- |Coq| can be used as a type-checker for the Calculus of Inductive @@ -1834,7 +1834,7 @@ inductive definitions* like the example of second-order existential quantifier (:g:`exSet`). There should be restrictions on the eliminations which can be -performed on such definitions. The eliminations rules in the +performed on such definitions. The elimination rules in the impredicative system for sort :math:`\Set` become: diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index f23e04c3a..848b3891b 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -706,18 +706,15 @@ Accessing the Type level ~~~~~~~~~~~~~~~~~~~~~~~~ The basic library includes the definitions of the counterparts of some data-types and logical -quantifiers at the ``Type``: level: negation, pair, and properties +quantifiers at the ``Type``: level: negation and properties of ``identity``. This is the module ``Logic_Type.v``. .. index:: single: notT (term) - single: prodT (term) - single: pairT (term) .. coqtop:: in Definition notT (A:Type) := A -> False. - Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B). At the end, it defines data-types at the ``Type`` level. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 509ac92f8..d9b249045 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1079,7 +1079,7 @@ The definition of ``N`` using the module type expression ``SIG`` with Module N : SIG' := M. -If we just want to be sure that the our implementation satisfies a +If we just want to be sure that our implementation satisfies a given module type without restricting the interface, we can use a transparent constraint -- cgit v1.2.3 From 227691b56a396eb274a20168454df7d989b68bf2 Mon Sep 17 00:00:00 2001 From: Zeimer Date: Thu, 19 Jul 2018 15:07:12 +0200 Subject: Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' of the Reference Manual. --- doc/sphinx/language/coq-library.rst | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 848b3891b..52c56d2bd 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -705,9 +705,22 @@ fixpoint equation can be proved. Accessing the Type level ~~~~~~~~~~~~~~~~~~~~~~~~ -The basic library includes the definitions of the counterparts of some data-types and logical -quantifiers at the ``Type``: level: negation and properties -of ``identity``. This is the module ``Logic_Type.v``. +The standard library includes ``Type`` level definitions of counterparts of some +logic concepts and basic lemmas about them. + +The module ``Datatypes`` defines ``identity``, which is the ``Type`` level counterpart +of equality: + +.. index:: + single: identity (term) + +.. coqtop:: in + + Inductive identity (A:Type) (a:A) : A -> Type := + identity_refl : identity a a. + +Some properties of ``identity`` are proved in the module ``Logic_Type``, which also +provides the definition of ``Type`` level negation: .. index:: single: notT (term) @@ -716,8 +729,6 @@ of ``identity``. This is the module ``Logic_Type.v``. Definition notT (A:Type) := A -> False. -At the end, it defines data-types at the ``Type`` level. - Tactics ~~~~~~~ -- cgit v1.2.3