| 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>
|
|
Ack-by: JasonGross
Reviewed-by: fajb
Reviewed-by: jfehrle
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: maximedenes
|
|
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: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: vbgl
|
|
This PR deprecates the use of `coqtop` as a compiler.
There is no point on having two binaries with the same purpose; after
the experiment in #8690, IMHO we have a lot to gain in terms of code
organization by splitting the compiler and the interactive binary.
We adapt the documentation and adapt the test-suite.
Note that we don't make `coqc` a true binary yet, but here we take
care only of the user-facing part.
The conversion of the binary will take place in #8690 and will bring
code simplification, including a unified handling of arguments.
|
|
Apparently it's deprecated / doesn't always work, see
https://tex.stackexchange.com/questions/84041/why-does-calm-n-give-m
See #9429 (we also need to fix the distributed file on the server).
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: maximedenes
|
|
Reviewed-by: Zimmi48
|
|
|
|
Z.to_euclidean_division_equations
|
|
This reverts commit b49f4e966443a76ac70d37c4cde68f94de164c01.
It turns out the 4x was due to .nia.cache (because I didn't clean
sufficiently in testing), not due to `subst`.
|
|
This speeds up the file from 2m32s to
```
real 0m41.851s
user 0m41.512s
sys 0m0.376s
```
Also note the `subst` trick in the doc.
|
|
Alas, I have not had time to work on imrpoving the performance of nia,
and there has been a request to include this tactic (which is useful on
its own) without bundling it into `zify`. So that is what we do here.
I leave the definition of it in `PreOmega` in case we want to eventually
include it in `zify`/`nia`.
|
|
The various (micr)omega tactics now support `Z.div` and `Z.modulo`.
I briefly looked into supporting `Nat.div` and `Nat.modulo`, but the
conversions between `Z.div` and `Nat.div` are defined in `ZArith.Zdiv`,
which depends on `Omega`, which depends on `PreOmega`, which is where
`zify` is defined.
|
|
This commit was created via `./dev/tools/update-compat.py --master`
|
|
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".
|
|
Reviewed-by: cpitclaudel
|
|
Ack-by: Zimmi48
Ack-by: anton-trunov
Ack-by: jfehrle
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
\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 intros tactic to its own subsection. Add grammar and examples.
|
