| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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>
|
|
Reviewed-by: fajb
|
|
Ack-by: JasonGross
Reviewed-by: fajb
Reviewed-by: jfehrle
|
|
Reviewed-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: vbgl
|
|
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: maximedenes
|
|
|
|
|
|
Z.to_euclidean_division_equations
|
|
Also fold it into `Z.div_mod_to_quot_rem`
Note that the test-suite file is a bit slow. On my machine, it is
```
real 2m32.983s
user 2m32.544s
sys 0m0.492s
```
|
|
Alas, I have not had time to work on imrpoving the performance of nia,
and there has been a request to include this tactic (which is useful on
its own) without bundling it into `zify`. So that is what we do here.
I leave the definition of it in `PreOmega` in case we want to eventually
include it in `zify`/`nia`.
|
|
Disjunctions seem to have a negative performance impact, so let's try
implications instead.
|
|
The various (micr)omega tactics now support `Z.div` and `Z.modulo`.
I briefly looked into supporting `Nat.div` and `Nat.modulo`, but the
conversions between `Z.div` and `Nat.div` are defined in `ZArith.Zdiv`,
which depends on `Omega`, which depends on `PreOmega`, which is where
`zify` is defined.
|
|
DAG nodes hold now a system state and a parsing state.
The latter is always passed to the parser.
This paves the way to decoupling the effect of commands on the parsing
state and the system state, and hence never force to interpret, say,
Notation.
Handling proof modes is now done explicitly in the STM, not by interpreting
VernacStartLemma.
Similarly Notation execution could be split in two phases in order to obtain a
parsing state without fully executing it (that requires executing all
commands before it).
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
|
|
Ack-by: Zimmi48
Ack-by: anton-trunov
Ack-by: jfehrle
|
|
the intros tactic to its own subsection. Add grammar and examples.
|
|
|
|
|
|
This is for consistency with "rewrite {x..} y"
|
|
|
|
|
|
|
|
This is slightly blunt, it might be the case that we get delayed constraints
that cannot be solved resulting in a later universe inconsistency, but it looks
highly unlikely on arithmetical statements.
Alternatively we would have threaded the unification state, but this would
have required a much deeper change.
Fixes #9268.
|
|
This commit fixes a leftover of the merge of ssrmatching where
the .ml code received the appropriate banner, while the .v and
.mli di dnot.
|
|
|
|
|
|
|
|
(in case of side effects)
Also:
Fix #4781
Fix #4496
|
|
|
|
The warning can be avoided with the attributes, (or just disable the
warning itself I guess).
|
|
|
|
|
|
This commit implements the following intro patterns:
Temporary "=> +"
"move=> + stuff" ==== "move=> tmp stuff; move: tmp"
It preserves the original name.
"=>" can be chained to force generalization as in
"move=> + y + => x z"
Tactics as views "=> /ltac:(tactic)"
Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo".
Limited to views on the right of "=>", views that decorate a tactic
as move or case are not supported to be tactics.
Dependent "=> >H"
move=> >H ===== move=> ???? H, with enough ? to
name H the first non-dependent assumption (LHS of the first arrow).
TC isntances are skipped.
Block intro "=> [^ H] [^~ H]"
after "case" or "elim" or "elim/v" it introduces in one go
all new assumptions coming from the eliminations. The names are
picked from the inductive type declaration or the elimination principle
"v" in "elim/v" and are appended/prepended the seed "H"
The implementation makes crucial use of the goal_with_state feature of
the tactic monad. For example + schedules a generalization to be performed
at the end of the intro pattern and [^ .. ] reads the name seeds from
the state (that is filled in by case and elim).
|
|
|
|
workers
|
|
- deprecate the old 5-tuple accessor in favor of a view record,
- move `name` and `kind` proof data from `Proof_global` to `Proof`,
this will prove useful in subsequent functionalizations of the
interface, in particular this is what abstract, which lives in the
monads, needs in order no to access global state.
- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
|
|
This should improve correctness and will be needed for the PRs that
remove global access to the proof state.
|
|
|
|
|
|
|
|
|
|
|
|
These modules do actually belong there.
We have to slightly reorganize printers, removing a couple of
duplicated ones in the way.
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
|
|
Also remove a few undocumented settings
|
|
We make `declaration_hook`s optional arguments everywhere, and thus we
avoid some "fake" functions having to be passed.
This identifies positively the code really using hooks [funind,
rewrite, coercions, program, and canonicals] and helps moving toward
some hope of reification.
|
|
|
