| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
| |
conversion.
- Fix trans_fconv* to use evars correctly.
- Normalize the goal with respect to evars before rewriting in
[rewrite], allowing to see instanciations from other subgoals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
- a ltac solve_proper which generalizes solve_predicate_wd and co
- using le_elim is nicer that (apply le_lteq; destruct ...)
- "apply ->" can now be "apply" most of the time.
Benefit: NumPrelude is now almost empty
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13762 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
See NatInt/NZBits.v for the common axiomatization of bitwise functions
over naturals / integers. Some specs aren't pretty, but easier to
prove, see alternate statements in property functors {N,Z}Bits.
Negative numbers are considered via the two's complement convention.
We provide implementations for N (in Ndigits.v), for nat (quite dummy,
just for completeness), for Z (new file Zdigits_def), for BigN
(for the moment partly by converting to N, to be improved soon)
and for BigZ.
NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in
the reversed order (for consistency with the rest of the world):
for instance BigN.shiftl 1 10 is 2^10.
NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2)
on negative numbers. For the moment I've kept it intact, and have
just added a Zdiv2' which is truly equivalent to (Zdiv _ 2).
To reorganize someday ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
Btw, we finally declare the original Zpower as the power on Z.
We should switch to a more efficient one someday, but in the
meantime BigN is proved with respect to the old one.
TODO: reform Zlogarithm with respect to Zlog_def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13606 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
We temporary use a hack to convert a module type into a module
Module M := T is refused, so we force an include via
Module M := Nop <+ T where Nop is an empty module.
To be fixed later more beautifully...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13602 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
- Simplification of functor names, e.g. ZFooProp instead of ZFooPropFunct
- The axiomatisations of the different fonctions are now in {N,Z}Axioms.v
apart for Z division (three separate flavours in there own files).
Content of {N,Z}AxiomsSig is extended, old version is {N,Z}AxiomsMiniSig.
- In NAxioms, the recursion field isn't that useful, since we axiomatize
other functions and not define them (apart in the toy NDefOps.v).
We leave recursion there, but in a separate NAxiomsFullSig.
- On Z, the pow function is specified to behave as Zpower : a^(-1)=0
- In BigN/BigZ, (power:t->N->t) is now pow_N, while pow is t->t->t
These pow could be more clever (we convert 2nd arg to N and use pow_N).
Default "^" is now (pow:t->t->t). BigN/BigZ ring is adapted accordingly
- In BigN, is_even is now even, its spec is changed to use Zeven_bool.
We add an odd. In BigZ, we add even and odd.
- In ZBinary (implem of ZAxioms by ZArith), we create an efficient Zpow
to implement pow. This Zpow should replace the current linear Zpower
someday.
- In NPeano (implem of NAxioms by Arith), we create pow, even, odd functions,
and we modify the div and mod functions for them to be linear, structural,
tail-recursive.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13546 85f007b7-540e-0410-9357-904b9bb8a0f7
|
msozeau
letouzey