| Age | Commit message (Collapse) | Author |
|---|
|
Keep Numeral Notation wit a deprecation warning.
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
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>
|
|
The compilation to bytecode of the elimination schemes for int31 must
happen after the int31 type is registered to the retroknowledge.
Otherwise, the “decompint” instruction is not emitted.
|
|
|
|
|
|
|
|
|
|
|
|
Removing in passing two Local which are no-ops in practice.
|
|
Because that's the sane thing to do.
This will inevitably cause issues for projects which do not `Import
Coq.Strings.Ascii` before trying to use ascii notations.
We also move the syntax plugin for `int31` notations from `Cyclic31` to
`Int31`, so that users (like CompCert) who merely `Require Import
Coq.Numbers.Cyclic.Int31.Int31` get the `int31` numeral syntax. Since
`Cyclic31` `Export`s `Int31`, this should not cause any additional
incompatibilities.
|
|
|
|
|
|
|
|
|
|
|
|
Thanks to Yves for reporting it!
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- For instance, refl_equal --> eq_refl
- Npos, Zpos, Zneg now admit more uniform qualified aliases
N.pos, Z.pos, Z.neg.
- A new module BinInt.Pos2Z with results about injections from
positive to Z
- A result about Z.pow pushed in the generic layer
- Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
- Using tactic Z.le_elim instead of Zle_lt_or_eq
- Some cleanup in ring, field, micromega
(use of "Equivalence", "Proper" ...)
- Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
- In ZMake and ZMake, functor parameters are now named NN and ZZ
instead of N and Z for avoiding confusions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14413 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
According to B. Gregoire, this stuff is obsolete. Fine control
on when to launch the VM in conversion problems is now provided
by VMcast. We were already almost never boxing definitions anymore
in stdlib files.
"(Un)Boxed Definition foo" will now trigger a parsing error,
same with Fixpoint. The option "(Un)Set Boxed Definitions"
aren't there anymore, but tolerated (as no-ops), since unknown
options raise a warning instead of an error by default.
Some more cleaning could be done in the vm.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12685 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
on the way:
- Added a testsuite output file
- Try to avoid nasty unfolding (fix nfun ...) in type of I31.
Idealy we would need a "Eval compute in" for the type of a inductive
constructor
- Stop opening Scopes for BigQ, BigN, BigZ by default
The user should do some Open Scope.
TODO: there's a bug that prevent BigQ.opp to have arg in bigQ_scope
(and so on for other operations), even with some Bind Scope around.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12504 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Ajout clause "in" à "remember" (et passage du code en ML).
- Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute
aussi une égalité pour se souvenir du terme sur lequel l'induction
ou l'analyse de cas s'applique.
- Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de
Programs qui avait la sémantique de "pose proof" tandis que le nouveau
a la même sémantique que "pose (id:=t)").
- Un peu de réorganisation, uniformisation de noms dans Arith, et
ajout EqNat dans Arith.
- Documentation tactiques et notations de tactiques.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11034 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
now dumb wrappers around Zsqrt_plain. Wanted (dead or alive): better
implemntations _and_ their proofs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11013 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Suite à une modification faite maladroitement, on ne se contentait pas
de comparer le nom de la supposition quand on l'insérait dans l'ensemble
des suppositions utilisées, mais aussi son type, ce qui était
inutilement long (mais pas le facteur principal)
- L'environnement était parcouru deux fois pour chaque variable de
section. Ce n'était pas très grave vu qu'en général on a assez peu de
variables de sections sous la main. Mais ça restait inutile.
- Les noms qui ont déjà étés explorés sont maintenant memoizés, ce qui
gagne dans le cas les pires (comme les théorèmes sur les réels
typiquement) une exponentiel dans le temps de recherche (si on visualise
l'espace de recherche comme un DAG, l'ancienne procédure le parcourais
comme si il était un arbre, ce qui a une complexité exponentielle en la
taille du DAG).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11001 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10995 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
CyclicAxioms specs
Currently, 8 lemmas remains to tackle. One proof is done via a _very_
brute-force ugly approach. The all story for proving composition of
phi and phi_inv (and the other way around) is surprisingly long and
tricky. In both cases, comments are welcome, I may have missed an
easier road (?)
As a consequence of the above, we have a additional time-eager
file in the stdlib (about a minute to compile here).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10973 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
idea :-(
(some bad interaction with Arnaud's framework ??)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Vouillon)
As said at the beginning of the file:
This file contains basic definitions of a 31-bit integer
arithmetic. In fact it is more general than that. The only reason
for this use of 31 is the underlying mecanism for hardware-efficient
computations by A. Spiwack. Apart from this, a switch to, say,
63-bit integers is now just a matter of replacing every occurences
of 31 by 63. This is actually made possible by the use of
dependently-typed n-ary constructions for the inductive type
[int31], its constructor [I31] and any pattern matching on it.
If you modify this file, please preserve this genericity.
From the user point-of-view, almost nothing has changed: functions
like On, In, shiftr, shiftl and a few others now have a
syntactically-different definition, but thanks to Eval compute in their
definition, this leads to the exact same coq objects as before. The only
difference is "Check I31" that shows the compact n-ary version
(nfun digits 31 int31) instead of (digits -> ... -> digits -> int31).
But even "Print int31" shows the same answer as before (the above type
of I31 is shown after expansion).
Arnaud, could you check whether all this works fine with your
retroknowledge ?
Notice the new file NaryFunction that contain generic stuff about
n-ary dependent functions. It should end some day in another place
than theories/Numbers, but I cant figure where for now. This file is
also quite skinny yet, but it's a start.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10967 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This isn't useful for BigN et BigZ, but it can't hurt; and moreover
it's a simple way to understand CyclicAxioms. Next step: proving that
Int31 is also an implementation of CyclicAxiom.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10942 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* View of Int31 as a Z/nZ moved to file Z31Z.v (TO FINISH: specs are still admitted!)
* Modular specification of Z/nZ moved to ZnZ and renamed CyclicType
* More isolation between Cyclic/Abstract and Cyclic/DoubleCyclic
* A few comments
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10936 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10934 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
For the moment, the Ints files are simply moved into directories in
theories/Numbers with meaningful names. No filenames changed, apart
from:
Zaux.v -> theories/Numbers/BigNumPrelude.v
MemoFn.v -> theories/Lists/StreamMemo.v
More to come...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10899 85f007b7-540e-0410-9357-904b9bb8a0f7
|
