| Age | Commit message (Collapse) | Author |
|---|
|
The role of the `zify_saturate` tactic is to augment the goal with
positivity constraints. The premisses were previously obtained from
the context. If they are not present, we instantiate the saturation
lemma anyway.
Also,
- Remove saturation rules for Z.mul, the reasoning is performed by lia/nia
- Run zify_saturate after zify_to_euclidean_division_equations
- Better lemma for Z.power
- Ensure that lemma are generated once
Co-authored-by: Andrej Dudenhefner <mrhaandi>
Closes #12184, #11656
|
|
Signed primitive integers defined on top of the existing unsigned ones
with two's complement.
The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.
Additions to the kernel:
les (signed <=), lts (signed <), compares (signed compare),
divs (signed division), rems (signed remainder),
asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)
The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).
A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.
|
|
Also works for simpl.
|
|
|
|
Ack-by: SkySkimmer
Ack-by: ppedrot
Reviewed-by: vbgl
|
|
Following a request from Pierre-Marie Pédrot in #13258
|
|
By default Coq stdlib warnings raise an error, so this is really required.
|
|
We also put them in a module, so users can `Require Int63. Import
Int63.Int63Notations` without needing to unqualify the primitives.
In particular, we change
- `a \% m` into `a mod m` to correspond with the notation in ZArith
- `m == n` into `m =? n` to correspond with the eqb notations elsewhere
- `m < n` into `m <? n` to correspond with the ltb notations elsewhere
- `m <= n` into `m <=? n` to correspond with the leb notations elsewhere
- `m ≤ n` into `m ≤? n` for consistency with the non-unicode notation
The old notations are still accessible as deprecated notations.
Fixes #12454
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
|
|
|
|
Reviewed-by: anton-trunov
|
|
Fixes #11905
|
|
|
|
Add headers to a few files which were missing them.
|
|
We avoid redundant notations for the same concepts and make sure
notations do not break Ltac parsing for users of these libraries.
|
|
Ack-by: fajb
Reviewed-by: ppedrot
|
|
|
|
|
|
implementations.
|
|
This lemma is lsl_add_distr (about “<<” rather than “>>”).
See lemmas bit_add_or and lor_lsr for related properties.
|
|
Most of these files were introduced after #6543 but used older headers
copied from somewhere else.
|
|
|
|
There are three implementations of this primitive:
* one in OCaml on 63 bits integer in kernel/uint63_amd64.ml
* one in OCaml on Int64 in kernel/uint63_x86.ml
* one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h
Its specification is the axiom `diveucl_21_spec` in
theories/Numbers/Cyclic/Int63/Int63.v
* comment the implementations with loop invariants to enable an easy
pen&paper proof of correctness (note to reviewers: the one in
uint63_amd64.ml might be the easiest to read)
* make sure the three implementations are equivalent
* fix the specification in Int63.v
(only the lowest part of the result is actually returned)
* make a little optimisation in div21 enabled by the proof of correctness
(cmp is computed at the end of the first loop rather than at the beginning,
potentially saving one loop iteration while remaining correct)
* update the proofs in Int63.v and Cyclic63.v to take into account the
new specifiation of div21
* add a test
|
|
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>
|
