coq/test-suite/micromega, branch master The formal proof system Merge PR #14108: [zify] bugfix 2021-04-19T11:22:05+00:00 Vincent Laporte 2021-04-19T11:22:05+00:00 b53642ec813178fedd3e646832e7c033b8163f52 Reviewed-by: Zimmi48 Reviewed-by: vbgl 
Reviewed-by: Zimmi48
Reviewed-by: vbgl
[zify] bugfix 2021-04-16T21:53:38+00:00 Frederic Besson 2021-04-12T19:02:51+00:00 d2c7022f0e16e6037c0d8c30c837abaad2c8194f - to zify the conclusion, we are using Tactics.apply (not rewrite) Closes #11089 - constrain the arguments of Add Zify X to be GlobRef.t Unset Primitive Projections so that projections are GlobRef.t. Closes #14043 Update doc/sphinx/addendum/micromega.rst Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> 
- to zify the conclusion, we are using Tactics.apply (not rewrite)

Closes #11089

- constrain the arguments of Add Zify X to be GlobRef.t
Unset Primitive Projections so that projections are GlobRef.t.

Closes #14043

Update doc/sphinx/addendum/micromega.rst

Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
[zify] More aggressive application of saturation rules 2021-04-12T20:03:30+00:00 BESSON Frederic 2021-03-31T20:16:50+00:00 8193ca191cc435c108a4842ae38a11d74c7c20a5 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 
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
[zify] better error reporting 2021-04-12T08:11:32+00:00 BESSON Frederic 2021-04-02T17:58:46+00:00 2e75d6606220cb4b5e80766b82007f94788929fb The vernacular command takes a reference instead of a constr. Moreover, the head symbol is checked i.e Add Zify InjTyp ref checks that the referenced term has type Intyp X1 ... Xn Closes #14054, #13242 Co-authored-by: Vincent Laporte <vbgl@users.noreply.github.com> 
The vernacular command takes a reference instead of a constr.
Moreover, the head symbol is checked i.e
Add Zify InjTyp ref checks that the referenced term has type
Intyp X1 ... Xn

Closes #14054, #13242

Co-authored-by: Vincent Laporte <vbgl@users.noreply.github.com>
[micromega/nia] Improve sharing of proofs 2021-02-10T08:59:18+00:00 BESSON Frederic 2021-02-08T14:07:42+00:00 68c3ffa6db6139081dab196bf3617214862a52af Closes #13794 
Closes #13794
[micromega] Add missing support for `implb` 2021-01-06T09:39:07+00:00 BESSON Frederic 2021-01-05T09:05:47+00:00 ac64cad9e6c0496afc600380d5c21fd1129db400 






[micromega] Updated test-suite
2020-11-18T08:49:22+00:00

BESSON Frederic

2020-11-17T22:35:02+00:00

0f0581b8d37168a54bd8b9f447317cc2cdd6c2d0

Moved bug_13227.v to complexity/bug_13227_i.v





Moved bug_13227.v to complexity/bug_13227_i.v







[micromega] More pre-procesing
2020-11-18T08:49:22+00:00

BESSON Frederic

2020-10-19T17:46:32+00:00

d18fadb8d8120c61d2fc71c840f6e55f71c808d7

- Remove obviously redundant constraints
- Perform (partial) Fourier elimination to detect (easy) cutting-planes

Closes #13227





- Remove obviously redundant constraints
- Perform (partial) Fourier elimination to detect (easy) cutting-planes

Closes #13227







[zify] Add support for Int63.int
2020-10-20T08:02:09+00:00

Frédéric Besson

2020-05-14T13:58:23+00:00

a2f5cc26baca0db087a677196f186ac2f75aa484

Update doc/sphinx/addendum/micromega.rst
Co-authored-by: Jason Gross <jasongross9@gmail.com>

Update theories/micromega/ZifyInt63.v
Co-authored-by: Jason Gross <jasongross9@gmail.com>





Update doc/sphinx/addendum/micromega.rst
Co-authored-by: Jason Gross <jasongross9@gmail.com>

Update theories/micromega/ZifyInt63.v
Co-authored-by: Jason Gross <jasongross9@gmail.com>







Merge PR #12815: [micromega] Fix bug#12790
2020-08-11T08:34:43+00:00

Vincent Laporte

2020-08-11T08:34:43+00:00

873130ae0e8f6079388f4be8259cd893f314e6d5

Reviewed-by: vbgl





Reviewed-by: vbgl