| Age | Commit message (Collapse) | Author |
|---|
|
- ring/field: detection of constants for ring/field,
detection of power, potential use of euclidean division.
- for BigN and BigZ, x^n now takes a N as 2nd arg instead of a positive
- mention that we can use (r)omega thanks to (ugly) BigN.zify, BigZ.zify.
By the way, BigN.zify could still be improved (no insertion of positivity
hyps yet, unlike the original zify).
- debug of BigQ.qify (autorewrite was looping on spec_0).
- for BigQ, start of a generic functor of properties QProperties.
- BigQ now implements OrderedType, TotalOrder, and contains facts
about min and max.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12681 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We use the <+ operation to regroup all known facts about BigN
(resp BigZ, ...) in a unique module. This uses also the new ! feature
for controling inlining. By the way, we also make sure that these
new BigN and BigZ modules implements OrderedTypeFull and TotalOrder,
and also contains facts about min and max (cf. GenericMinMax).
Side effects:
- In NSig and ZSig, specification of compare and eq_bool is now
done with respect to Zcompare and Zeq_bool, as for other ops.
The order <= and < are also defined via Zle and Zlt, instead
of using compare. Min and max are axiomatized instead of being
macros.
- Some proofs rework in QMake
- QOrderedType and Qminmax were in fact not compiled by make world
Still todo: OrderedType + MinMax for BigQ, etc etc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12680 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12652 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
NB: for declaring div and mod as a morphism, even when divisor is zero,
I've slightly changed the definition of div_eucl: it now starts by a
check of whether the divisor is zero. Not very nice, but this way
we can say that BigN.div and BigZ.div _always_ answer like Zdiv.Zdiv.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12646 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This allow to really finish files about division.
An abs and sgn is added to BigZ.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12644 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
|
|
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@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Now there is a class "SetoidRelation" for registering relations that
should always be considered as setoids and never unfolded. Every "Add
Relation" command adds an instance and impl,iff are there by
default. Now the test is: if there is a SetoidRelation instance, use it
; otherwise, allow unfolding to find an eq or fallback on
setoid_rewrite. To avoid searching for SetoidRelation instances
repeateadly we check that it is really needed first by unfolding the
hyp. Only two scripts relied on the now-forbidden semantics of rewriting
by an @eq inside a setoid relation, in Numbers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11269 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
|
|
* Isolate and put forward the interfaces NSig and ZSig that describe
what should contain structures of natural numbers and integers (specs
are done by translation to ZArith).
* Functors NSigNAxioms and ZSigZAxioms proving that these NSig and
ZSig implements the fully-abstract NAxioms and ZAxioms module types.
* BigN and BigZ now contains more notations, plus an export of all
abstract results proved by Evgeny instantiated thanks to NSigNAxioms
and ZSigZAxioms. In addition, BigN and BigZ are declared as
(semi/full)-rings.
* as a consequence, some incompatibities have to be fixed in BigQ:
- take care of some name masking (via Import, Open Scope ...)
- some additionnal constants like BigN.lt to deal with
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
