# Refactoring of Micromega plugin (including new Simplex based solver) #8457

Merged
merged 1 commit into from Oct 10, 2018

## Conversation

Projects
None yet
9 participants
Contributor

### fajb commented Sep 11, 2018

This PR aims at improving the Micromega plugin - more specifically the proof procedures.
To get there, some non trivial refactoring has been performed.

### New feature

There is now a Simplex based linear prover enabled by default.
The Fourier based algorithm can be obtained by Unset Simplex.
The Simplex probably requires some polishing but should be more scalable.
Eventually, the objective would be to dump the Fourier code (mfourier.ml)

### Completeness improvement

lia and nia were known to have certain shortcomings regarding completeness.
The following goals (added to the test-suite) were not solvable.
Each of them requires some orthogonal modification to the proof-procedure.

• Lemma cutting_plane is solved by finding cutting planes proofs -- the Simplex is instrumental for doing that.
• Lemma linear_subst is solved by performing some non-linear pivoting before solving the goal.
• Lemma negative_square is solved by performing some more aggressive non-linear pre-processing

`Lemma cutting_plane: forall (m : Z) (M : Z) (x : Z) (i : Z) (e1 : Z) (e2 : Z) (e5 : Z) (e6 : Z) (H2 : e5 >= M) (H11 : i < m) (H5 : 0 <= i) (H15 : m < 4294967296) (H7 : 0 <= x) (H26 : e5 < 4294967296) (H21 : x + i = 4294967296 * e6 + e5) (H9 : x + m = 4294967296 * e2 + e1) (H12 : x < e1) (H13 : e1 < M), False.`

`Lemma linear_subst : forall (x y : Z), 2*x = 0 -> x * y = 0.`

`Lemma negative_square : forall (x y: Z), - x*x >= 0 -> x * y = 0.`

Contributor

### JasonGross left a comment

 I think this deserves an entry in `CHANGES`. Also, it sounds like the `Simplex` option is a compatibility setting, so it should be unset in `theories/Compat/Coq89.v` after a `Declare ML Module` to make the option available.
plugins/micromega/Lia.v Outdated
plugins/micromega/ZMicromega.v Outdated

Member

### Zimmi48 commented Sep 12, 2018

 @fajb Note the "needs: rebase" label which is preventing GitLab CI to run.

Member

### gares commented Sep 12, 2018

 Looks amazing, but the title of the PR only cover the less interesting aspect of the patch as far as I can tell. It should be updated, since it appears in the merge commit. It should contain the word simplex, IMO.

### coqbot removed the needs: rebase label Sep 13, 2018

Contributor Author

### fajb commented Sep 13, 2018

 @JasonGross, I have updated CHANGES. Yet, I really expect the Simplex option to be deprecated as soon as possible. I see this as a way to investigate regressions. @gares, the PR title is updated. It was indeed missing an important point - refactoring can lead farther than initially expected.
Member

### ejgallego commented Sep 13, 2018

 Note that we are hoping to raise the minimal ocaml version to 4.05 , so there is some chance you could remove some cruft from this pr

### Zimmi48 reviewed Sep 25, 2018

 @@ -27,6 +27,11 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``. generating a *proof cache* which makes it possible to rerun scripts even without `csdp`. .. flag:: Simplex This option (set by default) instructs the decision procedures to use the Simplex method for solving linear goals.If it is not set, the decision procedures are using Fourier elimination.

#### Zimmi48 Sep 25, 2018

Member

You are missing a space after `goals.`

 power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following so-called *omega nightmare* :cite:`TheOmegaPaper`. This tactic offers an alternative to the :tacn:`omega` and :tacn:`romega`

#### Zimmi48 Sep 25, 2018

Member

Just a heads-up, #8419 removes `romega` and will be merged soon and it will create a conflict here.

Contributor

### vbgl commented Sep 27, 2018 • edited

 There seem to be two minor issues left: This breaks `fiat-crypto`: will someone fix it? Does the `Unset Simplex.` incantation deserves to be cast in the `Coq89` compatibility module?
Member

### Zimmi48 commented Sep 27, 2018

 The answer to the second question is yes indeed.
Contributor Author

### fajb commented Sep 28, 2018

 For fiat-crypto, I will investigate a bit but would be glad if someone has some insight about what is going on.

Contributor

### andres-erbsen commented Sep 29, 2018 • edited

 @fajb re fiat-crypto: I think this call to lia now succeeds without using the context variable `m_big`, and thus the Ltac caller of this lemma still passing in `m_big` here causes an error. If so, with the new `lia`, it should be possible to just not pass `m_small`, but a backwards-compatible fix would probably involve somehow "using" `m_big` in the original lemma even if `lia` doesn't use it. EDIT: try this version: mit-plv/fiat-crypto#442

### vbgl approved these changes Oct 5, 2018

 @@ -10,667 +10,901 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) (* Frédéric Besson (Irisa/Inria) 2006-20011 *) (* Frédéric Besson (Irisa/Inria) 2006-20018 *)

#### vbgl Oct 5, 2018

Contributor

This change is very funny ;-)

Contributor

### vbgl commented Oct 5, 2018

 @JasonGross I think your comments have been addressed. Do you have any objection to merging? Also, it seems that the `Simplex` option is not a compatibility option but a debugging feature.
Member

### Zimmi48 commented Oct 5, 2018

 I can't see this: Does the Unset Simplex. incantation deserves to be cast in the Coq89 compatibility module? being implemented. But I think it was asked by Jason and also by me.
Member

### Zimmi48 commented Oct 5, 2018

 Also, it seems that the Simplex option is not a compatibility option but a debugging feature. Ah, I hadn't missed this part of your message. So this idea is that normally the behavior should not change and thus the option not be needed?
Contributor Author

### fajb commented Oct 5, 2018

 @Zimmi48 , for most of the cases, the behaviour will be the same. What can change is the set of hypotheses used by a proof. In the CI, this has manifested in fiat-crypto. When no other regression is found, the goal is to remove this option.
Contributor

### vbgl commented Oct 9, 2018

 Frédéric, can you please rebase so as to fix the `CHANGES` file; then I’ll merge. Thanks.

### vbgl self-assigned this Oct 9, 2018

``` Refactoring of Micromega code using a Simplex linear solver ```
```- 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.```
``` 7f445d1 ```

### vbgl removed needs: fixing needs: testing labels Oct 9, 2018

Contributor Author

### fajb commented Oct 9, 2018

 @vbgl rebase done. Thanks for taking care of the merge.
Contributor

### vbgl commented Oct 10, 2018

 Benchmark results ``````┌──────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬──────────────────────────┬───────────────────┐ │ │ user time [s] │ CPU cycles │ CPU instructions │ max resident mem [KB] │ mem faults │ │ │ │ │ │ │ │ │ package_name │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-sf-vfa │ 45.91 46.28 -0.80 % │ 126923496387 127287091232 -0.29 % │ 201801036949 201920772893 -0.06 % │ 536212 534944 +0.24 % │ 28 5 +460.00 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-gpfsl │ 1194.46 1201.86 -0.62 % │ 3328297021142 3347920485805 -0.59 % │ 4375643012786 4412360037465 -0.83 % │ 1922356 1707752 +12.57 % │ 19 11 +72.73 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-bignums │ 96.81 96.77 +0.04 % │ 268160783473 267577219986 +0.22 % │ 381354045758 381261217503 +0.02 % │ 537280 533668 +0.68 % │ 6 0 +nan % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-flocq │ 585.12 584.84 +0.05 % │ 1626760932676 1625351157779 +0.09 % │ 2360279645247 2355732360180 +0.19 % │ 1714236 1712344 +0.11 % │ 176 20 +780.00 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-mathcomp-field │ 465.50 464.64 +0.19 % │ 1295674879169 1291856412326 +0.30 % │ 2115220170176 2115519266743 -0.01 % │ 807696 803440 +0.53 % │ 0 212 -100.00 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-vst │ 1684.59 1681.46 +0.19 % │ 4680449021173 4673894764169 +0.14 % │ 6419173834660 6421869185122 -0.04 % │ 2226996 2227004 -0.00 % │ 374 186 +101.08 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-unimath │ 1324.78 1322.23 +0.19 % │ 3677306879780 3663059316110 +0.39 % │ 6220333290772 6216566887491 +0.06 % │ 1076300 1072828 +0.32 % │ 240 21 +1042.86 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-fiat-crypto │ 6282.72 6270.32 +0.20 % │ 17477500871123 17435666663143 +0.24 % │ 28490054885928 28479544451172 +0.04 % │ 2466256 2481344 -0.61 % │ 1093 1099 -0.55 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-mathcomp-real-closed │ 186.60 186.22 +0.20 % │ 517828381241 516674086546 +0.22 % │ 784449325326 784331452136 +0.02 % │ 837488 831624 +0.71 % │ 0 8 -100.00 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-fiat-parsers │ 712.47 710.91 +0.22 % │ 1977382336703 1971992320622 +0.27 % │ 3034373511520 3031247617415 +0.10 % │ 2858796 2847208 +0.41 % │ 4 217 -98.16 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-mathcomp-character │ 291.62 290.77 +0.29 % │ 809278622075 806740496391 +0.31 % │ 1175166405093 1175903635028 -0.06 % │ 1100640 1119852 -1.72 % │ 0 0 +nan % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-math-classes │ 245.32 244.56 +0.31 % │ 676281999035 673120965823 +0.47 % │ 883148940972 881253384162 +0.22 % │ 526648 524848 +0.34 % │ 83 83 +0.00 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-sf-plf │ 72.97 72.73 +0.33 % │ 201675971033 201320693904 +0.18 % │ 291994683610 292162271003 -0.06 % │ 517096 515684 +0.27 % │ 15 0 +nan % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-mathcomp-solvable │ 218.80 217.94 +0.39 % │ 607331307079 604271720803 +0.51 % │ 865077783523 863970151823 +0.13 % │ 861244 861564 -0.04 % │ 1 44 -97.73 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-hott │ 329.99 328.66 +0.40 % │ 918751820045 916391143141 +0.26 % │ 1383554900327 1383415170418 +0.01 % │ 641552 598524 +7.19 % │ 61 0 +nan % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-compcert │ 888.38 884.74 +0.41 % │ 2463340519084 2451104766873 +0.50 % │ 3534693360002 3544171619024 -0.27 % │ 1345212 1349540 -0.32 % │ 102 32 +218.75 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-mathcomp-fingroup │ 83.53 83.15 +0.46 % │ 231172730781 229706593649 +0.64 % │ 342129752862 341203937777 +0.27 % │ 591724 587856 +0.66 % │ 51 0 +nan % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-sf-lf │ 43.18 42.98 +0.47 % │ 118435858370 118331727843 +0.09 % │ 191600758269 191403637684 +0.10 % │ 425144 422224 +0.69 % │ 129 0 +nan % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-mathcomp-odd-order │ 1411.50 1404.66 +0.49 % │ 3928588252719 3913101070567 +0.40 % │ 6597440627897 6592367881629 +0.08 % │ 1362848 1354808 +0.59 % │ 0 0 +nan % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-mathcomp-algebra │ 204.60 203.54 +0.52 % │ 565525978362 562710905646 +0.50 % │ 792990022337 791897383765 +0.14 % │ 647968 644172 +0.59 % │ 176 5 +3420.00 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-fiat-core │ 133.26 132.54 +0.54 % │ 371634099141 369524887824 +0.57 % │ 494136555625 493539663948 +0.12 % │ 503896 500328 +0.71 % │ 67 56 +19.64 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-geocoq │ 2831.38 2812.86 +0.66 % │ 7870580666678 7819337125032 +0.66 % │ 12531121501649 12527252327483 +0.03 % │ 1391304 1390120 +0.09 % │ 125 84 +48.81 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-corn │ 1545.27 1534.66 +0.69 % │ 4287062364537 4260973935395 +0.61 % │ 6345265660369 6336355184377 +0.14 % │ 841692 846640 -0.58 % │ 44 44 +0.00 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-color │ 732.92 727.28 +0.78 % │ 2029265627611 2017285501914 +0.59 % │ 2443821663827 2439598250129 +0.17 % │ 1391412 1389416 +0.14 % │ 38 226 -83.19 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-coquelicot │ 102.64 101.59 +1.03 % │ 283034052842 281454751796 +0.56 % │ 379235498090 377382267630 +0.49 % │ 715880 717128 -0.17 % │ 280 13 +2053.85 % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-mathcomp-ssreflect │ 64.53 63.84 +1.08 % │ 176926239299 175645112850 +0.73 % │ 250292904298 249407860867 +0.35 % │ 541224 535144 +1.14 % │ 2 0 +nan % │ ├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼───────────────────┤ │ coq-formal-topology │ 56.83 56.21 +1.10 % │ 154427768035 154063457029 +0.24 % │ 232351047970 231863084608 +0.21 % │ 480620 479788 +0.17 % │ 0 0 +nan % │ └──────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┴───────────────────┘ ``````

### vbgl dismissed JasonGross’s stale reviewOct 10, 2018

Requested changes have been performed.

### vbgl merged commit `7f445d1` into coq:master Oct 10, 2018 4 checks passed

#### 4 checks passed

ci/gitlab/pr-8457 Pipeline passed on GitLab
Details
continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
doc:refman Link to refman build artifact.
Details

### vbgl added a commit that referenced this pull request Oct 10, 2018

``` Merge PR #8457: Refactoring of Micromega plugin (including new Simple… ```
`…x based solver)`
``` 71280c8 ```
Contributor Author

### fajb commented Oct 16, 2018

 @vbgl the tests are fairly dispointing -- to say the least. Would it be possible to get finer grained results? On a goal basis? And wether it is lia or nia. I would like to understand better before starting optimising...
Member

### ejgallego commented Oct 16, 2018

 Indeed @fajb you can access the per-goal data here. I'd dare to say that the tests show now same timing, this kind of 1% noise is normal within the current infrastructure. https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/ws/518/html/ Well, it shows "not found" which I dunno why. Maybe you can rerun and see?