aboutsummaryrefslogtreecommitdiff
path: root/theories/micromega
AgeCommit message (Collapse)Author
2021-04-19Merge PR #14108: [zify] bugfixVincent Laporte
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2021-04-16[zify] bugfixFrederic Besson
- 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>
2021-04-12[zify] More aggressive application of saturation rulesBESSON Frederic
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
2021-04-12Merge PR #14061: [zify] better error reportingVincent Laporte
Reviewed-by: vbgl
2021-04-12[zify] better error reportingBESSON Frederic
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>
2021-04-06Standardizing spacing for {| ... |} in two files.Hugo Herbelin
2021-04-06Typo in a micromega comment.Hugo Herbelin
2020-12-15Modify micromega/ZMicromega.v to compile with -mangle-namesJasper Hugunin
2020-12-15Catch up to where I was last time.Jasper Hugunin
Many of the changes are a consequence of coq/coq#13132.
2020-11-18[micromega] Simplex uses alternatively Gomory cuts and case splitsBESSON Frederic
2020-11-18[micromega] Optimised cnf in case an hypothesis is trivially False.BESSON Frederic
This optimisation reduces (sometimes) the dependencies of a proof.
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
By default Coq stdlib warnings raise an error, so this is really required.
2020-11-09Merge PR #13173: Lint stdlib with -mangle-names #4coqbot-app[bot]
Reviewed-by: anton-trunov
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all ↵coqbot-app[bot]
pattern-matching clause with unused named variable Reviewed-by: jfehrle Reviewed-by: vbgl Ack-by: gares
2020-10-20[zify] Use flag for Z.to_euclidean_division_equations.Frédéric Besson
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-10-20[zify] Add support for Int63.intFrédéric Besson
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>
2020-10-11Modify micromega/ZifyInst.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZifyClasses.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Ztac.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZCoeff.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/RingMicromega.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Tauto.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Refl.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/EnvRing.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/OrderedRing.v to compile with -mangle-namesJasper Hugunin
2020-10-05Adapting theories to unused pattern-matching variable warning.Hugo Herbelin
2020-08-26Modify lia to work with -mangle-namesJasper Hugunin
We used to be refreshing the names for intros but not using the refreshed names. The same pattern of `intro_using` (which is what `intros ?name` effectively is) messing things up as in coq/coq#12881.
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-14Update zify documentationFrédéric Besson
Add Zify <X> are documented. Add <X> is deprecated as it clashed with the standard Add command
2020-06-14fix according to review by @pi8027Frédéric Besson
2020-06-14Update theories/micromega/ZifyBool.vFrédéric Besson
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com> - insert boolean constraint (b = true \/ b = false) - add specs for b2z - zify_post_hook performs a case-analysis over boolean constraints - Stricter typing constraints for `zify` declared operators The type is syntactically checked against the declaration of injections. Some explicit casts may need to be inserted.
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
The syntax of formulae is extended to support boolean constants (true, false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb, Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and Z.ltb.
2020-05-09Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.Maxime Dénès
Reviewed-by: maximedenes
2020-04-30[zify] add support for Nat.le, Nat.lt and Nat.eqFrédéric Besson
Nat.le, Nat.lt and Nat.eq are aliased to le, lt and @eq nat. The required declarations are now added in ZifyInst.
2020-04-17ZArith: move lia hints to a dedicated moduleVincent Laporte
2020-04-03Avoiding using a fixed introduction name in Ltac code of stdlib.Hugo Herbelin
2020-04-01[micromega] use Coqlib.lib_ref to get Coq constants.Frédéric Besson
2020-03-21Add module ZifyPow to avoid compatibility issue with 8.11.Théo Zimmermann
Also tweak the changelog entry to explain the difference.
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-03[zify] efficiency improvementsFrédéric Besson
- zify_iter_specs is entirely in OCaml - zify_op has been improved * The generation of proof-terms is more direct * It does not `rewrite` but instead either performs a `pose proof` or a `change` * The support for `and`, `or`, `not`, arrow is hardcoded * Avoid generating duplicate hypotheses such as 0 <= Z.of_nat x - zify_elim_let is entirely in OCaml (no Ltac callback) [micromega] fix stack overflow Less naive computation of bounds (online elimination of duplicates)
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:15:45 +0000