| Age | Commit message (Collapse) | Author |
|---|
|
Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.
This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.
We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.
Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.
This could also imply a performance gain as we now effectively
traverse less directories when locating a library.
See also discussion in #10003
|
|
PR #9725 fixes completness bugs introduces some inefficiency. The
current PR intends to fix the inefficiency while retaining
completness. The fix removes a pre-processing step and instead relies
on a more elaborate proof format introducing positivity constraints on
the fly.
Solve bootstrapping issues: RMicromega <-> Rbase <-> lia.
Fixes #11063 and fixes #11242 and fixes #11270
|
|
|
|
|
|
The logic is implemented in OCaml. By induction over the terms,
guided by registered Coq terms in ZifyInst.v, it generates a rewriting
lemma. The rewriting is only performed if there is some progress. If
the rewriting fails (due to dependencies), a novel hypothesis is
generated.
This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848
ans fixes #10755.
The zify plugin is placed in the micromega directory.
(Though the reason is unclear, having it in a separate directory is
bad for efficiency.) efficiency impact.
There are also a few improvements of lia/lra that are piggybacked.
- more aggressive pruning of useless hypotheses
- slightly optimised conjunctive normal form
- applies exfalso if conclusion is not in Prop
- removal of Timeout in test-suite
|
|
|
|
- Improved reification for Micromega (support for #8764)
- Fixes #9268: Do not take universes into account in lia reification
Improve #9291 by threading the evar_map during reification.
Universes are unified.
- Remove (potentially cyclic) dependency over lra for Rle_abs
- Towards a complete simplex-based lia
fixes #9615
Lia is now exclusively using cutting plane proofs.
For this to always work, all the variables need to be positive.
Therefore, lia is pre-processing the goal for each variable x
it introduces the constraints x = y - z , y>=0 , z >= 0
for some fresh variable y and z.
For scalability, nia is currently NOT performing this pre-processing.
- Lia is using the FSet library
manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4
to work around a "leaked" hint breaking compatibility of eauto
|
|
- Simplex based linear prover
Unset Simplex to get Fourier elimination
For lia and nia, do not enumerate but generate cutting planes.
- Better non-linear support
Factorisation of the non-linear pre-processing
Careful handling of equation x=e, x is only eliminated if x is used linearly
- More opaque interfaces
(Linear solvers Simplex and Mfourier are independent)
- Set Dump Arith "file" so that lia,nia calls generate Coq goals
in filexxx.v. Used to collect benchmarks and regressions.
- Rationalise the test-suite
example.v only tests psatz Z
example_nia.v only tests lia, nia
In both files, the tests are in essence the same.
In particular, if a test is solved by psatz but not by nia,
we finish the goal by an explicit Abort.
There are additional tests in example_nia.v which require specific
integer reasoning out of scope of psatz.
|
|
|
|
|
|
- Assert a purely arihtmetic sub-goal that is proved independently by reflexion.
(This reduces the stress on the conversion test)
- Does not use 'abstract' anymore (more natural proof-term)
- Fix a parsing bug (certain terms in Prop where not recognized)
|
|
If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
|
|
Init/Tauto.v)
|
|
|
|
|
|
* Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking
|
|
* unused terms are generalised
* proof is abstract
|
|
and nia.
|
