| Age | Commit message (Collapse) | Author |
|---|
|
|
|
In fixpoint typing rule section, a type of constructor is described
twice:
- ∀ p_1:P_1,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_r:T_r,~(I_j~p_1 … p_r~t_1 … t_s)
- ∀ p_1:P_1,~…,∀ p_r :P_r,~∀ y_1:B_1,~… ∀ y_k:B_k,~(I~a_1 … a_k)
Both seems invalid.
The former require that the number of parameters and
the number of (non-parameter) constructor argumets is same.
The latter require that the number of (non-parameter) constructor
argumets and the number of inductive type arguments (including paramters) is
same.
Also, "k" is already used for the number of inductive types in
a inductive definition.
So, I changed the number of (non-parameter) constructor
argumets to "m". I choose "m" because "m" is used for the purpose
in the description for iota-reduction of destructors.
Also, I changed the inductive type parameters and arguments of latter
consistent with the former.
|
|
In the description of destructors,
"Type of branches" section and "Typing rule" section shares
the definition of "r" (and "s" from previous commit).
However actual parameters are p_1...p_r in the former section and
q_1...q_r in the latter section.
I guess it's because the latter section uses
p_1...p_l in other purpose: index of constructor for a inductive type.
So, I change the parameter p_1...p_r to q_1...q_r in the former section
to consistent with the latter section.
|
|
In the description of destuctors,
"Type of branches" section uses "p" as the number of arguments.
It is confusing because "p" is used as the number of parameters.
After the section, "Typing rule." section uses "s" without definition as
I q1...qr t1...ts.
It seems that it is the number of arguments.
So, I changed "p" to "s".
"s" is also confusing with sorts, though.
|
|
In Cic admissible rules section, c and c' are exchanged at
https://github.com/coq/coq/commit/8654b03544f0efe4b418a0afdc871ff84784ff83 .
But the exchange is not complete.
This commit complete it.
|
|
|
|
|
|
"'" in the extended (k_i added) form of Fix syntax should be removed.
In the following sentence, A_i' is referenced as A_i.
```
Each :math:`A_i` should be a type (reducible to a term) starting
with at least :math:`k_i` products
:math:`∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'`
```
Also, A_i' is used in ∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i' and
A_i' must not equal to ∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'.
The old reference manual, coq-8.7.2-reference-manual.pdf,
doesn't have "'".
They are added by
https://github.com/coq/coq/commit/47dca6c5da585212f69b6b83b25896ff990781e3
which ports Cic document from TeX to sphinx.
So, the change seems just an accident.
|
|
Remove the 2nd premise "(E[Γ_P ] ⊢ A_j : s_j)_(j=1...k)".
Also, "Γ" in "c_i ∉ Γ ∪ E" is changed to "Γ_I".
"E[Γ_P ] ⊢ A_j : s_j" contradicts with a side condition
"A_j is an arity of sort s_j".
The latter means that A_j is ∀ x1:T1, ... ∀ xm:Tm, s_j.
So, "(∀ x1:T1, ..., s_j) : s_j)" is required.
Using Prod-{Prop,Set,Type}, it needs "s_j : s_j" which cannot be proved.
This problem is introduced at 2018-07-22:
https://github.com/coq/coq/commit/f25c1d252ad61b4dc4321e3a11f33b1e6d4e3dff
Before that, the premise describes "A_j : s'_j".
And "s'_j" is not explained anywhere.
I think "A_j : s'_j" describes that A_j is a type (a value of a sort).
Thus, "A_j is an arity of sort s_j" imply "A_j : s'_j".
So, I removed the 2nd premise.
Also, a side condition describes "c_i ∉ Γ ∪ E" but "Γ" is not explained.
I think that Γ should be Γ_I.
Γ should include Γ_I because a constructor, c_i, and inductive types are
both defined in global environment and it cannot accept duplicate name.
Actually, such definition fails:
```
Fail Inductive X := X : X.
(* The following names are used both as type names and constructor names: X.*)
```
Γ doesn't include Γ_P because parameters are not defined in global
environment.
Actually, a parameter can be same name as a constructor name:
```
Inductive I (X : nat) := X : I X.
Check X. (* X : forall X : nat, I X *)
```
|
|
Cic description doesn't describe the lowest universe level clearly.
- "Type(i) for any integer i" seems Type(-1) is possible
- "S = {Prop,Set,Type(i)| i ∈ ℕ }" depends on the definition of "ℕ"
which is not described.
It is well known that there are two definitions that ℕ includes 0 or not.
In Coq, it is natural that ℕ includes 0 because the inductive type
nat includes 0.
- "Prop:Type(1), Set:Type(1)" suggests the lowest level is 1.
- AX-Prop and AX-Set describes Prop:Type(1) and Set:Type(1).
So, Prop and Set are not belongs to Type(0).
Also, CPDT describes that "The type of Set is Type(0)".
http://adam.chlipala.net/cpdt/html/Universes.html
I think the lowest universe level is 1 because AX-Prop and AX-Set.
I'm not certain to fix this problem but
my idea to fix this problem is changing
"Type(i) for any integer i" to
"Type(i) for any integer i ≥ 1".
|
|
The former is more succinct and intuitive.
|
|
c can be non-function since c:U.
So, c c' is not typeable.
|
|
|
|
|
|
|
|
|
|
|
|
This commit basically ajusts spaces as
- ∀x:T,t to ∀x:T,~t
- λx:T.t to λx:T.~t
- E;c:T to E;~c:T
x and T are more related than T and t.
So, T and t should not positioned closely than x and T.
Unfortunately, they are formatted that T and t are positioned closely
without "~".
(Similary, c and T are more related than E and c.)
|
|
The former is more succinct and consistent with most of
other parts in cic.rst.
|
|
Add :math:`...` for mathematical expressions.
|
|
|
|
"∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, \Sort" is changed to
"∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S" because
\Sort is not a term.
"S" is choosen to be consistent with the description of
Inductive Definitions.
|
|
|
|
|
|
|
|
Exchange a closing parenthesis and a :math: closing backquote.
|
|
In the note about η-reduction,
two lambda-abstraction used "," instead of ".".
|
|
After #9435 (Use \mathcal instead of \cal), \Sort doesn't have
font changing effect.
So, {\Sort} is same as \Sort now and the former is changed to latter in
cic.rst.
|
|
|
|
|
|
|
|
This corresponds to "Module TreeExample." removed at
2018-04-24 bcf5352cc7a26a672e719f7dad4021c69d723833.
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
|
|
The definition of \plus and \tri in cic.rst is not effective
for HTML output.
So, move them into refman-preamble.sty.
Also, \tri is renamed to \trii to express
the suffix of "\triangleright_\iota".
|
|
Ack-by: Zimmi48
Ack-by: anton-trunov
Ack-by: jfehrle
|
|
\nO, \nS, \evenO, \evenS, \oddS, \length, \Nil and \cons are used.
don't use \kw in \kw{n} in Fixpoint typing rule section.
|
|
Fix small errors in cic.rst:
* 3.4.1 Free variables: use :math: for "∀ x:T,~U".
:g: doesn't show "∀" in PDF.
"λx:T.~U" is also changed to :math: to use consistent font.
* 3.4.3 Zeta: ":U" added in "let x:=u:U in t" to be valid let-in expression.
* 3.4.3 convertibility: add :math: for u_2' to apply math formatting.
* 3.4.4.6: fix index. "n" should be "k" because they corresponds k-th
constructor.
* 3.4.5 Type constructor: I changed the section title "Type constructor" to
"Type of constructor".
"Type constructor" means a feature to construct new type.
But this section describes about a type of constructor.
* 3.4.5 Example nattree: The reason of
"``nattree`` occurs only strictly positively in ``A``" should be
bullet 1 instead of bullet 3.
The bullet 3 of strict positivity definition is about product, "∀x ∶ U , V",
but "A" is not a product.
* 3.4.5 Destructors: use :math: for "∀".
:g: doesn't show "∀" in PDF.
Also, :math: is used for expressions which has no "∀" character
for font consistency.
Note that I use \kw{has}\_\kw{length} instead of
\kw{has\_length} because the latter is formatted as has\_length in HTML.
(the backslash is retained.)
* 3.4.5 list example: curly braces added.
* 3.4.5 Fixpoint definition: add :math: for Γ_i to apply math formatting.
* 3.4.6 2nd rule of First abstracting property: use \subst.
This adds a curly brace.
Also, spacing and fonts are adjusted as follows.
* 3.4.1 let-in term: use :math: for variable x, consistent with other term
descriptions.
* 3.4.1 let-in term: use \letin command for concrete let-in term.
* 3.4.2 Note: insert spaces as ((λ x:T.~u)~t).
Since T is more closely reated to x than u, T should be positioned
close to x than u.
Since it seems most application has a space, I inserted a space here
for consistency.
* 3.4.3 beta-reduction: insert spaces as 3.4.2.
* 3.4.3 eta-expansion: insert spaces as 3.4.2.
* 3.4.5 Example: use sans-serif fonts for constructor "O" and "S".
* 3.4.5 Fixpoint definition: insert spaces around "with".
* 3.4.5 Fixpoint typing rule: fix fonts for "O" and "S" as 3.4.5 and
insert spaces as 3.4.2.
* 3.4.5 Fixpoint reduction rule: insert a space between {F} and a_1 for
consistency.
* 3.4.6 First abstracting property: insert spaces as 3.4.2.
|
|
The previous language makes it seem as if record parameters are automatically set as implicit for the projection functions, but (per discussion with @jasongross) the omission of parameters from primitive projection only takes effect in Coq's internal AST.
|
|
|
|
The code to generate the legacy bodies is moved to its only user in
extraction.
It almost seems like we could remove it (ie no special extraction code
for primitive projection constants) but then we run into issues with
automatic unboxing eg `Record foo := { a : nat; b : a <= 5 }.` gets
extracted to `type foo = nat` and (if we remove the special code) `let
a = a`.
|
|
|
|
|
|
to fix all misuses.
|
|
And a few more Sphinx fixes in passing.
|
|
Remove objects without body from most chapters.
The remaining problems are all in the SSReflect chapter.
|
|
|
|
This adds an optional [Subgraph] part to the Print Universes command,
eg [Print Universes Subgraph(i j)] to print only constraints related
to i and j (and Prop/Set).
|
|
|
|
|
