michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(algebra/simplifier): simp rule set for units

Browse source
This commit is contained in:
Daniel Selsam 2015-11-12 20:30:10 -08:00
parent e7890fb456
commit 00a5cd519e
3 changed files with 16 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
library/algebra/simplifier.lean
View file

@ -22,6 +22,19 @@ attribute algebra.right_distrib [simp]
end sum_of_monomials
namespace units
attribute algebra.zero_add [simp]
attribute algebra.add_zero [simp]
attribute algebra.zero_mul [simp]
attribute algebra.mul_zero [simp]
attribute algebra.one_mul [simp]
attribute algebra.mul_one [simp]
end units
-- TODO(dhs): remove `add1` from the original lemmas and delete this
namespace numeral_helper
open algebra

22
tests/lean/simplifier12.lean
View file

@ -1,5 +1,5 @@
import algebra.ring
open algebra
import algebra.simplifier
open algebra simplifier.sum_of_monomials simplifier.units
set_option simplify.max_steps 1000
universe l
@ -7,22 +7,4 @@ constants (T : Type.{l}) (s : algebra.comm_ring T)
constants (x1 x2 x3 x4 : T) (f g : T → T)
attribute s [instance]
attribute add.comm [simp]
attribute add.assoc [simp]
attribute left_distrib [simp]
attribute right_distrib [simp]
attribute mul.comm [simp]
attribute mul.assoc [simp]
attribute zero_add [simp]
attribute add_zero [simp]
attribute one_mul [simp]
attribute mul_one [simp]
theorem add.o2 [simp] {A : Type} [s : add_comm_semigroup A] (a b c : A) :
a + (b + c) = b + (a + c) := sorry
#simplify eq 0 x2 + (1 * g x1 + 0 + (f x3 * 3 * 1 * (x2 + 0 + g x1 * 7) * x2 * 1)) + 5 * (x4 + f x1)

2
tests/lean/simplifier12.lean.expected.out
View file

@ -1 +1 @@
x2 + (g x1 + (x4 * 5 + (f x1 * 5 + (x2 * (f x3 * (x2 * 3)) + x2 * (f x3 * (3 * (g x1 * 7)))))))
x2 + (g x1 + (x4 * 5 + (f x1 * 5 + (x2 * (x2 * (f x3 * 3)) + x2 * (f x3 * (g x1 * (3 * 7)))))))