A `ring_exp` tactic for dealing with exponents in rings #1715
mergify
merged
41 commits into
leanprover-community:master
from
Vierkantor:ring_exp
robertylewis
commented
on 2019-11-21
Test for ring_exp
b6bf70cf
Implement -a/b * -a/b = a/b * a/b
203073d1
Hide extra information in the `ex` type in `ex_info`
e55954b5
Some attempts to make the proof returned by ring_exp shorter
e8c0ba71
Fix that ring_exp wouldn't handle pow that isn't monomial.has_pow
28dd76b1
Some optimizations in ring_exp
aa10b727
Make all proofs explicit, halving execution time more or less
f9ff2ac9
Cache `has_add` and `has_mul` instances for another 2x speedup
117d47e9
ring_exp can replace ring to compile mathlib
e1f360ce
Revert `ring` to non-test version
5bcdb4ef
Code cleanup and documentation
afb2679b
Revert the test changes to `linarith`
c701de5a
Undo the test changes to `ring2`
6f11d5f5
Whitespace cleanup
46985518
Fix overzealous error handling
804e25e8
Fix the TODO's
238b1c64
Example use of ring_exp in data.polynomial
13c2d877
Check that `ring_exp` deals well with natural number subtraction
141435db
Fix incorrect docstring
1fa8b8a7
Improve documentation
b076112d
Small stylistic fixes
ce97e7ac
Fix slow behaviour on large exponents
3a30e268
Add `ring_exp` to the default tactics
b9c5b40a
Use applicative notation where appropriate
aec9b6a3
The `ring_exp` tactic also does normalization
c4802c29
Move `normalize` from `tactic.interactive` to `ring_exp` namespace
fded7ec5
Fix name collision between `equiv` in data.equiv.basic and `equiv` in…
c3da4532
Fixes for the linter
3ef04cfc
Fix the usage of type classes for `sub_pf` and `div_pf`
97749c20
Fix an additional linting error
5dba765e
Optimization: we don't need norm_num to determine `x * 1 = x`
a56b1a37
Improve documentation of `test/ring_exp.lean`
0231adfb
Rename `resolve_atoms` to `resolve_atom_aux` for clarity
61e25494
Small stylistic fixes
65e6367d
Remove unneccessary hidden fields to `ex`
74d448ba
Control how much unfolding `ring_exp` does by putting a `!` after it
6f99d017
Reword comment for `ex_type`
c18a237a
Use `ring_exp!` to deal with `(n : ℕ) + 1 - 1 = n`
d3367ee2
Document the `!` flag for `ring`, `ring_exp` and `ring_exp_eq`
026a2261
Get rid of searching for another cached instance
33d947cc
Fix `ring_exp` failing on terms on the form `0^succ (succ ...)`
6452f3ed
digama0
approved these changes
on 2019-12-09
Login to write a write a comment.
Login via GitHub