Commit 2019-12-09 20:49 5c093726

View on Github →

A ring_exp tactic for dealing with exponents in rings (#1715)

Test for ring_exp
Implement -a/b * -a/b = a/b * a/b
Hide extra information in the ex type in ex_info
Some attempts to make the proof returned by ring_exp shorter
Fix that ring_exp wouldn't handle pow that isn't monomial.has_pow
Some optimizations in ring_exp
Make all proofs explicit, halving execution time more or less
Cache has_add and has_mul instances for another 2x speedup
ring_exp can replace ring to compile mathlib
Revert ring to non-test version
Code cleanup and documentation
Revert the test changes to linarith
Undo the test changes to ring2
Whitespace cleanup
Fix overzealous error handling Instead of catching any fail in eval, we just catch the operations that can safely fail (i.e. invert and negate). This should make internal errors visible again.
Fix the TODO's
Example use of ring_exp in data.polynomial
Check that ring_exp deals well with natural number subtraction
Fix incorrect docstring
Improve documentation
Small stylistic fixes
Fix slow behaviour on large exponents
Add ring_exp to the default tactics
Use applicative notation where appropriate
The ring_exp tactic also does normalization Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
Move normalize from tactic.interactive to ring_exp namespace
Fix name collision between equiv in data.equiv.basic and equiv in test/tactics.lean I just renamed the definition in test/tactics.lean to my_equiv and the operator to my≅.
Fixes for the linter
Fix the usage of type classes for sub_pf and div_pf
Fix an additional linting error
Optimization: we don't need norm_num to determine x * 1 = x
Improve documentation of test/ring_exp.lean
Rename resolve_atoms to resolve_atom_aux for clarity
Small stylistic fixes
Remove unneccessary hidden fields to ex
Control how much unfolding ring_exp does by putting a ! after it
Reword comment for ex_type
Use ring_exp! to deal with (n : ℕ) + 1 - 1 = n
Document the ! flag for ring, ring_exp and ring_exp_eq
Get rid of searching for another cached instance
Fix ring_exp failing on terms on the form 0^succ (succ ...)