-
Notifications
You must be signed in to change notification settings - Fork 259
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: port linarith #526
Conversation
This PR/issue depends on:
|
I've just brought this up to date with |
There are still some style things to clean up, and ideally it would use bors merge |
TODO: * Before merge - [x] fix a bug in linarith in mathlib3 I just found ... - [x] depends on: #519 - [x] style lint - [x] docs - [X] move theory stubs to a separate PR, for easier tracking: #733 - [x] failing to parse the `LinarithConfig` option * Before or after merge? - [ ] Implement the `removeNe` preprocessor. - [ ] Add support for restricting to a single type. How to store a `Type` in `LinarithConfig`? * After merge - [ ] Teach `norm_num` to solve `example [LinearOrderedRing α] : (0 : α) < 37 := by norm_num`. - [ ] Port `zify_proof` (plumbing for `zify`), and add the `natToInt` preprocessor. Mostly done now, but see #741 before all the tests will work. - [ ] Port `cancel_denoms` tactic, and add the `cancelDenoms` preprocessor. - [ ] Add the `nlinarith` preprocessor and front-end syntax. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Build failed: |
bors p=10 |
bors merge |
TODO: * Before merge - [x] fix a bug in linarith in mathlib3 I just found ... - [x] depends on: #519 - [x] style lint - [x] docs - [X] move theory stubs to a separate PR, for easier tracking: #733 - [x] failing to parse the `LinarithConfig` option * Before or after merge? - [ ] Implement the `removeNe` preprocessor. - [ ] Add support for restricting to a single type. How to store a `Type` in `LinarithConfig`? * After merge - [ ] Teach `norm_num` to solve `example [LinearOrderedRing α] : (0 : α) < 37 := by norm_num`. - [ ] Port `zify_proof` (plumbing for `zify`), and add the `natToInt` preprocessor. Mostly done now, but see #741 before all the tests will work. - [ ] Port `cancel_denoms` tactic, and add the `cancelDenoms` preprocessor. - [ ] Add the `nlinarith` preprocessor and front-end syntax. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Build failed: |
bors r- |
bors r+ |
TODO: * Before merge - [x] fix a bug in linarith in mathlib3 I just found ... - [x] depends on: #519 - [x] style lint - [x] docs - [X] move theory stubs to a separate PR, for easier tracking: #733 - [x] failing to parse the `LinarithConfig` option * Before or after merge? - [ ] Implement the `removeNe` preprocessor. - [ ] Add support for restricting to a single type. How to store a `Type` in `LinarithConfig`? * After merge - [ ] Teach `norm_num` to solve `example [LinearOrderedRing α] : (0 : α) < 37 := by norm_num`. - [ ] Port `zify_proof` (plumbing for `zify`), and add the `natToInt` preprocessor. Mostly done now, but see #741 before all the tests will work. - [ ] Port `cancel_denoms` tactic, and add the `cancelDenoms` preprocessor. - [ ] Add the `nlinarith` preprocessor and front-end syntax. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |
* master: (26 commits) docs (Order.BoundedOrder): fix typos (#775) feat: port Algebra.Order.Monoid.Cancel.Defs (#774) feat: port Order.Disjoint (#773) feat: port linarith (#526) feat: port Algebra.Order.Monoid.Defs (#771) feat: port control.functor (#612) feat(Algebra/GroupWithZero/Commute): port file (#762) feat: port Logic.Equiv.Option (#674) chore: fix todos in `to_additive` (#765) feat(Algebra/Order/Monoid/MinMax): port file (#763) fix: update context in recursive calls in split_ifs (#761) feat(Algebra/Regular/Basic): port file (#758) feat: port Order.BoundedOrder (#697) feat: port Data.Pi.Algebra (#564) feat: port Algebra.Hom.Embedding (#764) fix: to_additive generates equation lemmas for target (#767) fix: fix translation errors in various files (#716) fix: remove submodules (#766) feat(Algebra/Group/Commute): port file (#750) feat(Algebra/Ring/Commute): port file (#759) ...
TODO:
ring_exp
tactic, subtraction inring
#519LinarithConfig
optionremoveNe
preprocessor.Type
inLinarithConfig
?norm_num
to solveexample [LinearOrderedRing α] : (0 : α) < 37 := by norm_num
.zify_proof
(plumbing forzify
), and add thenatToInt
preprocessor.Mostly done now, but see
zify
incorrectly useseq.refl
#741 before all the tests will work.cancel_denoms
tactic, and add thecancelDenoms
preprocessor.nlinarith
preprocessor and front-end syntax.