From 00a5cd519efb17d2a5b6762eef35d803039cada6 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Thu, 12 Nov 2015 20:30:10 -0800
Subject: [PATCH] feat(algebra/simplifier): simp rule set for units

---
 library/algebra/simplifier.lean           | 13 +++++++++++++
 tests/lean/simplifier12.lean              | 22 ++--------------------
 tests/lean/simplifier12.lean.expected.out |  2 +-
 3 files changed, 16 insertions(+), 21 deletions(-)

diff --git a/library/algebra/simplifier.lean b/library/algebra/simplifier.lean
index c259d7243..80e2eff9c 100644
--- a/library/algebra/simplifier.lean
+++ b/library/algebra/simplifier.lean
@@ -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
diff --git a/tests/lean/simplifier12.lean b/tests/lean/simplifier12.lean
index 9ca3b1be6..dcde14082 100644
--- a/tests/lean/simplifier12.lean
+++ b/tests/lean/simplifier12.lean
@@ -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)
-
-
diff --git a/tests/lean/simplifier12.lean.expected.out b/tests/lean/simplifier12.lean.expected.out
index 63325e56d..4ab708082 100644
--- a/tests/lean/simplifier12.lean.expected.out
+++ b/tests/lean/simplifier12.lean.expected.out
@@ -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)))))))