From b7322e28c12d274ccec992b7fc49d35b2e56a2a4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 3 Dec 2017 15:03:07 -0800
Subject: [PATCH] feat(library): do not using simp lemmas for sorting arguments
 of AC operators by default

---
 doc/changes.md                               |  4 ++++
 library/data/bitvec.lean                     |  2 ++
 library/data/rbmap/default.lean              |  8 ++++----
 library/data/rbtree/basic.lean               |  3 ---
 library/data/rbtree/find.lean                |  3 ---
 library/data/rbtree/insert.lean              |  3 ---
 library/data/rbtree/main.lean                |  3 ---
 library/data/rbtree/min_max.lean             |  3 ---
 library/init/algebra/field.lean              |  2 ++
 library/init/algebra/functions.lean          |  2 +-
 library/init/algebra/group.lean              | 14 +++++++++-----
 library/init/algebra/ring.lean               |  8 ++++++--
 library/init/data/int/basic.lean             |  2 ++
 library/init/data/int/order.lean             | 10 +++++++---
 library/init/data/list/lemmas.lean           |  2 +-
 library/init/data/nat/bitwise.lean           |  2 ++
 library/init/data/nat/lemmas.lean            |  2 ++
 library/init/data/ordering/lemmas.lean       |  4 ++--
 library/init/logic.lean                      | 12 ++++++------
 tests/lean/run/auto_param_in_structures.lean |  2 ++
 tests/lean/run/cpdt.lean                     |  2 +-
 tests/lean/run/psum_wf_rec.lean              |  1 +
 tests/lean/run/u_eq_max_u_v.lean             |  2 ++
 23 files changed, 56 insertions(+), 40 deletions(-)

diff --git a/doc/changes.md b/doc/changes.md
index 8089d849ce..2b7212e971 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -42,6 +42,10 @@ master branch (aka work in progress branch)
 
 *Changes*
 
+- Remove `[simp]` attribute from lemmas `or.assoc`, `or.comm`, `or.left_comm`, `and.assoc`, `and.comm`, `and.left_comm`, `add_assoc`, `add_comm`, `add_left_com`, `mul_assoc`, `mul_comm` and `mul_left_comm`.
+  These lemmas were being used to "sort" arguments of AC operators: and, or, (+) and (*).
+  This was producing unstable proofs. The old behavior can be retrieved by using the commands `local attribute [simp] ...` or `attribute [simp] ...` in the affected files.
+
 - `string` is now a list of unicode scalar values. Moreover, in the VM,
   strings are implemented as an UTF-8 encoded array of bytes.
 
diff --git a/library/data/bitvec.lean b/library/data/bitvec.lean
index 479eb66cbf..e2e3a6286c 100644
--- a/library/data/bitvec.lean
+++ b/library/data/bitvec.lean
@@ -158,6 +158,8 @@ section conversion
   theorem bits_to_nat_to_list {n : ℕ} (x : bitvec n)
   : bitvec.to_nat x = bits_to_nat (vector.to_list x)  := rfl
 
+  local attribute [simp] add_comm add_assoc add_left_comm mul_comm mul_assoc mul_left_comm
+
   theorem to_nat_append {m : ℕ} (xs : bitvec m) (b : bool)
   : bitvec.to_nat (xs ++ₜ b::nil) = bitvec.to_nat xs * 2 + bitvec.to_nat (b::nil) :=
   begin
diff --git a/library/data/rbmap/default.lean b/library/data/rbmap/default.lean
index cb58491751..9b04a6648f 100644
--- a/library/data/rbmap/default.lean
+++ b/library/data/rbmap/default.lean
@@ -127,13 +127,13 @@ begin
     existsi e, cases t; simp [find_entry] at ⊢ h₂,
     { simp [rbtree.find, rbnode.find] at h₂, cases h₂, contradiction },
     { cases h₂ with h₂₁ h₂₂, split,
-      { cases e, apply eqv_keys_of_eqv_entries h₂₁ },
       { have := rbtree.find_eq_find_of_eqv ⟨rbnode.red_node lchild val rchild, p⟩ (eqv_entries k v val.snd),
-        rw [←this], exact h₂₂ } },
+        rw [←this], exact h₂₁ },
+      { cases e, apply eqv_keys_of_eqv_entries h₂₂ } },
     { cases h₂ with h₂₁ h₂₂, split,
-      { cases e, apply eqv_keys_of_eqv_entries h₂₁ },
       { have := rbtree.find_eq_find_of_eqv ⟨rbnode.black_node lchild val rchild, p⟩ (eqv_entries k v val.snd),
-        rw [←this], exact h₂₂ } } },
+        rw [←this], exact h₂₁ },
+      { cases e, apply eqv_keys_of_eqv_entries h₂₂ } } },
   { intro h, cases h with e h,
     cases h with h₁ h₂, cases t; simp [find_entry] at h₁,
     { contradiction },
diff --git a/library/data/rbtree/basic.lean b/library/data/rbtree/basic.lean
index ea851e953f..76a7a3fdf4 100644
--- a/library/data/rbtree/basic.lean
+++ b/library/data/rbtree/basic.lean
@@ -5,9 +5,6 @@ Authors: Leonardo de Moura
 -/
 universe u
 
-/- TODO(Leo): remove after we cleanup stdlib simp lemmas -/
-local attribute [-simp] or.comm or.left_comm or.assoc and.comm and.left_comm and.assoc
-
 namespace tactic
 /- TODO(Leo): move blast_disjs and twice to another file. -/
 
diff --git a/library/data/rbtree/find.lean b/library/data/rbtree/find.lean
index 95444205d5..749e0d2720 100644
--- a/library/data/rbtree/find.lean
+++ b/library/data/rbtree/find.lean
@@ -6,9 +6,6 @@ Authors: Leonardo de Moura
 import data.rbtree.basic
 universe u
 
-/- TODO(Leo): remove after we cleanup stdlib simp lemmas -/
-local attribute [-simp] or.comm or.left_comm or.assoc and.comm and.left_comm and.assoc
-
 namespace rbnode
 variables {α : Type u}
 
diff --git a/library/data/rbtree/insert.lean b/library/data/rbtree/insert.lean
index f71d24ea0b..4e7185b688 100644
--- a/library/data/rbtree/insert.lean
+++ b/library/data/rbtree/insert.lean
@@ -6,9 +6,6 @@ Authors: Leonardo de Moura
 import data.rbtree.find
 universes u v
 
-/- TODO(Leo): remove after we cleanup stdlib simp lemmas -/
-local attribute [-simp] or.comm or.left_comm or.assoc and.comm and.left_comm and.assoc
-
 namespace rbnode
 variables {α : Type u}
 
diff --git a/library/data/rbtree/main.lean b/library/data/rbtree/main.lean
index 62d6d3a957..31e2b1ce8d 100644
--- a/library/data/rbtree/main.lean
+++ b/library/data/rbtree/main.lean
@@ -6,9 +6,6 @@ Authors: Leonardo de Moura
 import data.rbtree.find data.rbtree.insert data.rbtree.min_max
 universes u
 
-/- TODO(Leo): remove after we cleanup stdlib simp lemmas -/
-local attribute [-simp] or.comm or.left_comm or.assoc and.comm and.left_comm and.assoc
-
 namespace rbnode
 variables {α : Type u} {lt : α → α → Prop}
 
diff --git a/library/data/rbtree/min_max.lean b/library/data/rbtree/min_max.lean
index 944e4946da..a99a0e6175 100644
--- a/library/data/rbtree/min_max.lean
+++ b/library/data/rbtree/min_max.lean
@@ -6,9 +6,6 @@ Authors: Leonardo de Moura
 import data.rbtree.basic
 universe u
 
-/- TODO(Leo): remove after we cleanup stdlib simp lemmas -/
-local attribute [-simp] or.comm or.left_comm or.assoc and.comm and.left_comm and.assoc
-
 namespace rbnode
 variables {α : Type u} {lt : α → α → Prop}
 
diff --git a/library/init/algebra/field.lean b/library/init/algebra/field.lean
index 716775eacb..e4e9648587 100644
--- a/library/init/algebra/field.lean
+++ b/library/init/algebra/field.lean
@@ -256,6 +256,8 @@ have a * b ≠ 0, from (division_ring.mul_ne_zero ha hb),
 by rw [add_comm, ← field.div_mul_left ha this, ← field.div_mul_right hb this,
        division_def, division_def, division_def, ← right_distrib]
 
+local attribute [simp] mul_assoc mul_comm mul_left_comm
+
 lemma field.div_mul_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0) (hd : d ≠ 0) :
       (a / b) * (c / d) = (a * c) / (b * d) :=
 begin simp [division_def], rw [mul_inv_eq hd hb, mul_comm d⁻¹] end
diff --git a/library/init/algebra/functions.lean b/library/init/algebra/functions.lean
index 51969023de..64d6a31970 100644
--- a/library/init/algebra/functions.lean
+++ b/library/init/algebra/functions.lean
@@ -438,7 +438,7 @@ sub_lt_of_abs_sub_lt_left (abs_sub a b ▸ h)
 lemma abs_sub_square (a b : α) : abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b :=
 begin
   rw abs_mul_abs_self,
-  simp [left_distrib, right_distrib]
+  simp [left_distrib, right_distrib, add_assoc, add_comm, add_left_comm, mul_comm]
 end
 
 lemma eq_zero_of_mul_self_add_mul_self_eq_zero {x y : α} (h : x * x + y * y = 0) : x = 0 :=
diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean
index 6717661ed5..44d387d839 100644
--- a/library/init/algebra/group.lean
+++ b/library/init/algebra/group.lean
@@ -37,21 +37,23 @@ class group (α : Type u) extends monoid α, has_inv α :=
 
 class comm_group (α : Type u) extends group α, comm_monoid α
 
-@[simp] lemma mul_assoc [semigroup α] : ∀ a b c : α, a * b * c = a * (b * c) :=
+lemma mul_assoc [semigroup α] : ∀ a b c : α, a * b * c = a * (b * c) :=
 semigroup.mul_assoc
 
 instance semigroup_to_is_associative [semigroup α] : is_associative α (*) :=
 ⟨mul_assoc⟩
 
-@[simp] lemma mul_comm [comm_semigroup α] : ∀ a b : α, a * b = b * a :=
+lemma mul_comm [comm_semigroup α] : ∀ a b : α, a * b = b * a :=
 comm_semigroup.mul_comm
 
 instance comm_semigroup_to_is_commutative [comm_semigroup α] : is_commutative α (*) :=
 ⟨mul_comm⟩
 
-@[simp] lemma mul_left_comm [comm_semigroup α] : ∀ a b c : α, a * (b * c) = b * (a * c) :=
+lemma mul_left_comm [comm_semigroup α] : ∀ a b c : α, a * (b * c) = b * (a * c) :=
 left_comm has_mul.mul mul_comm mul_assoc
 
+local attribute [simp] mul_comm mul_assoc mul_left_comm
+
 lemma mul_right_comm [comm_semigroup α] : ∀ a b c : α, a * b * c = a * c * b :=
 right_comm has_mul.mul mul_comm mul_assoc
 
@@ -306,6 +308,8 @@ instance add_semigroup_to_is_eq_associative [add_semigroup α] : is_associative
 instance add_comm_semigroup_to_is_eq_commutative [add_comm_semigroup α] : is_commutative α (+) :=
 ⟨add_comm⟩
 
+local attribute [simp] add_assoc add_comm add_left_comm
+
 def neg_add_self := @add_left_neg
 def add_neg_self := @add_right_neg
 def eq_of_add_eq_add_left := @add_left_cancel
@@ -405,7 +409,7 @@ lemma eq_sub_of_add_eq' [add_comm_group α] {a b c : α} (h : c + a = b) : a = b
 by simp [h.symm]
 
 lemma sub_eq_of_eq_add' [add_comm_group α] {a b c : α} (h : a = b + c) : a - b = c :=
-by simp [h]
+begin simp [h], rw [add_left_comm], simp end
 
 lemma eq_add_of_sub_eq' [add_comm_group α] {a b c : α} (h : a - b = c) : a = b + c :=
 by simp [h.symm]
@@ -420,7 +424,7 @@ lemma add_sub_comm [add_comm_group α] (a b c d : α) : a + b - (c + d) = (a - c
 by simp
 
 lemma sub_eq_sub_add_sub [add_comm_group α] (a b c : α) : a - b = c - b + (a - c) :=
-by simp
+begin simp, rw [add_left_comm c], simp end
 
 lemma neg_neg_sub_neg [add_comm_group α] (a b : α) : - (-a - -b) = a - b :=
 by simp
diff --git a/library/init/algebra/ring.lean b/library/init/algebra/ring.lean
index 3719af8ffa..011a506e75 100644
--- a/library/init/algebra/ring.lean
+++ b/library/init/algebra/ring.lean
@@ -112,6 +112,8 @@ section comm_semiring
   @[simp] theorem dvd_refl : a ∣ a :=
   dvd.intro 1 (by simp)
 
+  local attribute [simp] mul_assoc mul_comm mul_left_comm
+
   theorem dvd_trans {a b c : α} (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c :=
   match h₁, h₂ with
   | ⟨d, (h₃ : b = a * d)⟩, ⟨e, (h₄ : c = b * e)⟩ :=
@@ -220,11 +222,13 @@ instance comm_ring.to_comm_semiring [s : comm_ring α] : comm_semiring α :=
 section comm_ring
   variable [comm_ring α]
 
+  local attribute [simp] add_assoc add_comm add_left_comm mul_comm
+
   lemma mul_self_sub_mul_self_eq (a b : α) : a * a - b * b = (a + b) * (a - b) :=
-  by simp [right_distrib, left_distrib]
+  begin simp [right_distrib, left_distrib], rw [add_comm (-(a*b)), add_left_comm (a*b)], simp end
 
   lemma mul_self_sub_one_eq (a : α) : a * a - 1 = (a + 1) * (a - 1) :=
-  by simp [right_distrib, left_distrib]
+  begin simp [right_distrib, left_distrib], rw [add_left_comm, add_comm (-a), add_left_comm a], simp end
 
   lemma add_mul_self_eq (a b : α) : (a + b) * (a + b) = a*a + 2*a*b + b*b :=
   calc (a + b)*(a + b) = a*a + (1+1)*a*b + b*b : by simp [right_distrib, left_distrib]
diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean
index 2320afe311..8fdd9867a0 100644
--- a/library/init/data/int/basic.lean
+++ b/library/init/data/int/basic.lean
@@ -393,6 +393,8 @@ protected meta def transfer (distrib := tt) : tactic unit :=
 if distrib then `[int.transfer_core, simp [add_mul, mul_add]]
 else `[int.transfer_core, simp]
 
+local attribute [simp] mul_assoc mul_comm mul_left_comm
+
 instance : comm_ring int :=
 { add            := int.add,
   add_assoc      := by int.transfer,
diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean
index 1fb7bbc6ed..4d56b3cae7 100644
--- a/library/init/data/int/order.lean
+++ b/library/init/data/int/order.lean
@@ -175,9 +175,13 @@ protected lemma zero_lt_one : (0 : ℤ) < 1 := trivial
 
 protected lemma lt_iff_le_not_le {a b : ℤ} : a < b ↔ (a ≤ b ∧ ¬ b ≤ a) :=
 begin
-simp [int.lt_iff_le_and_ne], split; intro h; cases h with hneq hab; split,
-{assumption}, {intro hba, apply hneq, apply int.le_antisymm; assumption},
-{intro heq, apply hab, subst heq, apply int.le_refl}, {assumption}
+simp [int.lt_iff_le_and_ne], split; intro h,
+{ cases h with hab hn, split,
+  { assumption },
+  { intro hba, simp [int.le_antisymm hab hba] at *, contradiction } },
+{ cases h with hab hn, split,
+  { assumption },
+  { intro h, simp [*] at * } }
 end
 
 instance : decidable_linear_ordered_comm_ring int :=
diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean
index eea4ba6425..54ba0abb97 100644
--- a/library/init/data/list/lemmas.lean
+++ b/library/init/data/list/lemmas.lean
@@ -105,7 +105,7 @@ lemma eq_or_mem_of_mem_cons {a y : α} {l : list α} : a ∈ y::l → a = y ∨
 assume h, h
 
 @[simp] lemma mem_append {a : α} {s t : list α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t :=
-by induction s; simp *
+by induction s; simp [*, or_assoc]
 
 @[rsimp] lemma mem_append_eq (a : α) (s t : list α) : (a ∈ s ++ t) = (a ∈ s ∨ a ∈ t) :=
 propext mem_append
diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean
index 9d84ee8fba..1098de34ef 100644
--- a/library/init/data/nat/bitwise.lean
+++ b/library/init/data/nat/bitwise.lean
@@ -61,6 +61,8 @@ end
 @[simp] lemma div2_succ (n : ℕ) : div2 (succ n) = cond (bodd n) (succ (div2 n)) (div2 n) :=
 by unfold bodd div2 bodd_div2; cases bodd_div2 n; cases fst; refl
 
+local attribute [simp] add_comm add_assoc add_left_comm mul_comm mul_assoc mul_left_comm
+
 theorem bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 2 * div2 n = n
 | 0        := rfl
 | (succ n) := begin
diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index 8b77c4eea7..dca3f2c74e 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -1359,6 +1359,8 @@ end
 
 /- mod / div / pow -/
 
+local attribute [simp] mul_comm
+
 theorem mod_pow_succ {b : ℕ} (b_pos : b > 0) (w m : ℕ)
 : m % (b^succ w) = b * (m/b % b^w) + m % b :=
 begin
diff --git a/library/init/data/ordering/lemmas.lean b/library/init/data/ordering/lemmas.lean
index 91bc58ad8e..50b7502362 100644
--- a/library/init/data/ordering/lemmas.lean
+++ b/library/init/data/ordering/lemmas.lean
@@ -52,8 +52,8 @@ by simp
 @[simp] lemma cmp_using_eq_gt [is_strict_order α lt] (a b : α) : (cmp_using lt a b = ordering.gt) = lt b a :=
 begin
   simp, apply propext, apply iff.intro,
-  { exact λ h, h.1 },
-  { intro hba, split, assumption, intro hab, exact absurd (trans hab hba) (irrefl a) }
+  { exact λ h, h.2 },
+  { intro hba, split, { intro hab, exact absurd (trans hab hba) (irrefl a) }, { assumption } }
 end
 
 @[simp] lemma cmp_using_eq_eq (a b : α) : (cmp_using lt a b = ordering.eq) = (¬ lt a b ∧ ¬ lt b a) :=
diff --git a/library/init/logic.lean b/library/init/logic.lean
index 678077b3db..163347b128 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -374,19 +374,19 @@ iff.intro
   (assume ⟨ha, hb⟩, ⟨ha, iff.elim_left (h ha) hb⟩)
   (assume ⟨ha, hc⟩, ⟨ha, iff.elim_right (h ha) hc⟩)
 
-@[simp] lemma and.comm : a ∧ b ↔ b ∧ a :=
+lemma and.comm : a ∧ b ↔ b ∧ a :=
 iff.intro and.swap and.swap
 
 lemma and_comm (a b : Prop) : a ∧ b ↔ b ∧ a := and.comm
 
-@[simp] lemma and.assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
+lemma and.assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
 iff.intro
   (assume ⟨⟨ha, hb⟩, hc⟩, ⟨ha, ⟨hb, hc⟩⟩)
   (assume ⟨ha, ⟨hb, hc⟩⟩, ⟨⟨ha, hb⟩, hc⟩)
 
 lemma and_assoc (a b : Prop) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := and.assoc
 
-@[simp] lemma and.left_comm : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) :=
+lemma and.left_comm : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) :=
 iff.trans (iff.symm and.assoc) (iff.trans (and_congr and.comm (iff.refl c)) and.assoc)
 
 lemma and_iff_left {a b : Prop} (hb : b) : (a ∧ b) ↔ a :=
@@ -430,11 +430,11 @@ or.imp id h
 @[congr] lemma or_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∨ b) ↔ (c ∨ d) :=
 iff.intro (or.imp (iff.mp h₁) (iff.mp h₂)) (or.imp (iff.mpr h₁) (iff.mpr h₂))
 
-@[simp] lemma or.comm : a ∨ b ↔ b ∨ a := iff.intro or.swap or.swap
+lemma or.comm : a ∨ b ↔ b ∨ a := iff.intro or.swap or.swap
 
 lemma or_comm (a b : Prop) : a ∨ b ↔ b ∨ a := or.comm
 
-@[simp] lemma or.assoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
+lemma or.assoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
 iff.intro
   (or.rec (or.imp_right or.inl) (λ h, or.inr (or.inr h)))
   (or.rec (λ h, or.inl (or.inl h)) (or.imp_left or.inr))
@@ -442,7 +442,7 @@ iff.intro
 lemma or_assoc (a b : Prop) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
 or.assoc
 
-@[simp] lemma or.left_comm : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) :=
+lemma or.left_comm : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) :=
 iff.trans (iff.symm or.assoc) (iff.trans (or_congr or.comm (iff.refl c)) or.assoc)
 
 theorem or_iff_right_of_imp (ha : a → b) : (a ∨ b) ↔ b :=
diff --git a/tests/lean/run/auto_param_in_structures.lean b/tests/lean/run/auto_param_in_structures.lean
index 2884a4ef4f..d069655f4c 100644
--- a/tests/lean/run/auto_param_in_structures.lean
+++ b/tests/lean/run/auto_param_in_structures.lean
@@ -2,6 +2,8 @@ namespace test
 open tactic
 meta def my_tac : tactic unit := abstract (intros >> `[simp])
 
+local attribute [simp] add_assoc mul_assoc
+
 structure monoid (α : Type) :=
 (op    : α → α → α)
 (assoc : ∀ a b c, op (op a b) c = op a (op b c) . my_tac)
diff --git a/tests/lean/run/cpdt.lean b/tests/lean/run/cpdt.lean
index 38f55ace1a..2c948c3f7e 100644
--- a/tests/lean/run/cpdt.lean
+++ b/tests/lean/run/cpdt.lean
@@ -34,7 +34,7 @@ def reassoc : exp → exp
   | _              := Mult e1' e2'
   end
 
-attribute [simp] mul_add times reassoc eeval
+attribute [simp] mul_add times reassoc eeval mul_comm mul_assoc mul_left_comm
 
 theorem eeval_times (k e) : eeval (times k e) = k * eeval e :=
 by induction e; simp [*]
diff --git a/tests/lean/run/psum_wf_rec.lean b/tests/lean/run/psum_wf_rec.lean
index 05bebd8f21..8e4e40b991 100644
--- a/tests/lean/run/psum_wf_rec.lean
+++ b/tests/lean/run/psum_wf_rec.lean
@@ -6,6 +6,7 @@ def sum_has_sizeof_2 {α β} [has_sizeof α] [has_sizeof β] : has_sizeof (psum
 ⟨psum.alt.sizeof⟩
 
 local attribute [instance] sum_has_sizeof_2
+local attribute [simp] add_comm add_left_comm add_assoc mul_assoc mul_comm mul_left_comm
 
 mutual def f, g
 with f : ℕ → ℕ
diff --git a/tests/lean/run/u_eq_max_u_v.lean b/tests/lean/run/u_eq_max_u_v.lean
index f24e42df5f..e4a07b5d31 100644
--- a/tests/lean/run/u_eq_max_u_v.lean
+++ b/tests/lean/run/u_eq_max_u_v.lean
@@ -26,6 +26,8 @@ attribute [simp] semigroup_morphism.multiplicative
   multiplicative := begin intros, simp [coe_fn] end
 }
 
+local attribute [simp] mul_comm mul_assoc mul_left_comm
+
 @[reducible] definition semigroup_product { α β : Type u } ( s : semigroup α ) ( t: semigroup β ) : semigroup (α × β) := {
   mul := λ p q, (p^.fst * q^.fst, p^.snd * q^.snd),
   mul_assoc := begin