| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Reviewed-by: gares
|
|
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: fajb
|
|
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
Ack-by: JasonGross
Reviewed-by: fajb
Reviewed-by: jfehrle
|
|
We make `coqc` a truly standalone binary, whereas `coqtop` is
restricted to interactive use.
Thus, `coqtop -compile` will emit a warning and call `coqc`.
We have also refactored `Coqargs` into a common `Coqargs` module and a
compilation-specific module `Coqcargs`.
This solves problems related to `coqc` having its own argument
parsing, and reduces the number of strange argument combinations a
lot.
|
|
Ack-by: JasonGross
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: tchajed
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: maximedenes
|
|
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".
|
|
Fixes #9453
|
|
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
|
The former is more succinct and intuitive.
|
|
c can be non-function since c:U.
So, c c' is not typeable.
|
|
|
|
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: vbgl
|
|
|
|
|
|
|
|
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: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: vbgl
|
