| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12728 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Records of operations and specs in CyclicAxioms are now
type classes (under a module ZnZ for qualification).
We benefit from inference and from generic names:
(ZnZ.mul x y) instead of (znz_mul (some_ops...) x y).
- Beware of typeclasses unfolds: the line about
Typeclasses Opaque w1 w2 ... is critical for decent
compilation time (x2.5 without it).
- Functions defined via same_level are now obtained from a
generic version by (Eval ... in ...) during definition.
The code obtained this way should be just as before, apart
from some (minor?) details. Proofs for these functions
are _way_ simplier and lighter.
- The macro-generated NMake_gen.v contains only generic iterators
and compare, mul, div_gt, mod_gt. I hope to be able to adapt
these functions as well soon.
- Spec of comparison is now fully done with respect to Zcompare
- A log2 function has been added.
- No more unsafe_shiftr, we detect the underflow directly with sub_c
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12713 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12685 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
without scope.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12639 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
As a consequence, revert to some pedestrian proofs of Equivalence here
and there, without the need for the Measure class.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12598 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12563 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Make setoid_rewrite-through-rewrite's selection of occurences more
robust: do not try unification with reduction if not needed.
This changes a few scripts that were using reduction in a far from
obvious way and could break more.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12562 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Now that backtracking is working correctly, we need to avoid a
non-termination issue introduced by the [RelCompFun] definition in
RelationPairs, by adding a [Measure] typeclass. It could be used to have
a uniform notation for measures/interpretations in Numbers and be but in
the interfaces too, only the mimimal change was implemented.
Fix syntax change in test-suite scripts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12547 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
|
|
- No more nesting of Module and Module Type, we rather use Include.
- Instead of in-name-qualification like NZeq, we use uniform
short names + modular qualification like N.eq when necessary.
- Many simplification of proofs, by some autorewrite for instance
- In NZOrder, we instantiate an "order" tactic.
- Some requirements in NZAxioms were superfluous: compatibility
of le, min and max could be derived from the rest.
- NMul removed, since it was containing only an ad-hoc result for
ZNatPairs, that we've inlined in the proof of mul_wd there.
- Zdomain removed (was already not compiled), idea of a module
with eq and eqb reused in DecidableType.BooleanEqualityType.
- ZBinDefs don't contain any definition now, migrate it to ZBinary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12489 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12475 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
TODO: finish removing the "Add Relation", "Add Morphism" fun_* fun2_*
TODO: now that we have Include, flatten the hierarchy...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12464 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Mostly results about Zgcd (commutativity, associativity, ...).
Slight improvement of ZMicromega.
Beware: some lemmas of Zdiv/ Znumtheory were asking for
too strict or useless hypothesis. Some minor glitches may occur.
By the way, some iff lemmas about negb in Bool.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12313 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
rhs) of rewrite lemmas for efficient retrieval of matching lemmas.
Autorewrite's implementation is still unchanged but the dnet can be used
through the [hints] strategy of the new generalized rewrite. Now lemmas
are checked to actually be rewriting lemmas at declaration time hence
the change in DoubleSqrt where some unapplicable constants were declared
as lemmas.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12087 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11906 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Utilisation de notations de type "abbreviation paramétrée" plutôt que
de notations introduisant des mots-clés, là où c'est possible (cela affecte
QDen, in_left/in_right, inhabited, S/P dans NZCyclic).
- Extension du lexeur pour qu'il prenne le plus long token valide au
lieu d'échouer sur un plus long préfixe non valide de token (permet
notamment de faire passer la notation de Georges "'C_ G ( A )"
sans invalider toute séquence commençant par 'C et non suivie de _)
- Rajout d'un point final à certains messages d'erreur qui n'en avaient pas.
- Ajout String.copy dans string_of_label ("trou" de mutabilité signalé
par Georges -- le "trou" lié aux vecteurs des noeuds App restant lui
ouvert).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11225 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
|
|
for increased consistency with bignums parts
(commit part II: names of files + additional translation minus --> sub)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
for increased consistency with bignums parts
(commit part I: content of files)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11039 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11034 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t)))
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11033 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
|
|
transformed into generic functions, and aren't anymore fields of
records znz_op/znz_spec.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11012 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11003 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
proving addmuldiv31
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11002 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@10999 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10997 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10995 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10993 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
one.
Conversion to lists of digits is really the Right Way (TM). Maybe other parts
can also benefit from this idea. To be continued...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10978 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
|
|
part).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10964 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10944 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
|
|
(n _must_ in fact be a power of 2). Worse: Z_31Z is just plain wrong
since it is Z/(2^31)Z and not Z/31Z (my fault).
As a consequence, switch to CyclicAxioms, Cyclic31, DoubleCyclic, etc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10940 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In fact, for the moment, it was only containing a proof that Z/nZ
implements the NatInt NZAxiomsSig. We move it to a more meaningful
place and name.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10937 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
|
