Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-02 20:07 059f9374

View on Github →

feat(tactic): add linear arithmetic tactic (#301)

  • feat(data/list, tactic): small helper functions
  • feat(meta/rb_map): extra operations on native rb_maps
  • feat(tactic/linarith): add tactic for solving linear arithmetic goals
  • doc(tactic/linarith): add documentation and tests
  • chore(tactic/linarith): add copyright
  • feat(tactic/linarith): allow products of coefficients
  • feat(tactic/linarith): cut off search early if contradiction is found
  • feat(tests/linarith_tests): add test
  • doc(doc/tactics): update doc
  • feat(tactic/linarith): add config options
  • feat(tactic/linarith): support equality goals
  • chore(tactic/linarith): move non-tactic code out of tactic monad
  • feat(tactic/linarith): support rational coefficients
  • doc(tactic/linarith): update doc
  • feat(tactic/linarith): fix obvious inefficiency in canceling denoms
  • feat(tactic/linarith): efficiency improvements
  • fix(tactic/linarith): remove unnecessary import and dead code
  • fix(data/list/basic, meta/rb_map): shorter proofs

Estimated changes

modified theorem list.index_of_eq_length
added theorem linarith.add_subst
added theorem linarith.div_subst
added inductive linarith.ineq
added theorem linarith.mul_eq
added theorem linarith.mul_neg
added theorem linarith.mul_nonpos
added theorem linarith.mul_subst
added theorem linarith.neg_subst
added theorem linarith.sub_into_lt
added theorem linarith.sub_subst
added inductive linarith.{u}