coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-18	[micromega] More pre-procesing	BESSON Frederic
	- Remove obviously redundant constraints - Perform (partial) Fourier elimination to detect (easy) cutting-planes Closes #13227
2020-03-25	[ocamlformat] Use doc-comments=before style.	Emilio Jesus Gallego Arias
	IMHO it is a bit more logical, WDYT?
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-03-04	[micromega] Add numerical compatibility layer.	Emilio Jesus Gallego Arias
	Only significant change is in gcd / lcm which now are typed in `Z.t`
2019-12-17	[micromega] fix efficiency regression	Frédéric Besson
	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
2019-12-13	[micromega] Enable ocamlformat.	Emilio Jesus Gallego Arias

2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-04-01	Several improvements and fixes of Lia	Frédéric Besson
	- 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
2018-10-09	Refactoring of Micromega code using a Simplex linear solver	Frédéric Besson
	- 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.