From 8fcfe0bbd4a5fe471c1b3769c97117153b786b4f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 27 Dec 2016 16:54:00 -0800
Subject: [PATCH] feat(library/init/algebra/ac): add helper classes for AC

---
 library/init/algebra/ac.lean    | 18 ++++++++++++++++++
 library/init/algebra/group.lean | 14 +++++++++++++-
 2 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 library/init/algebra/ac.lean

diff --git a/library/init/algebra/ac.lean b/library/init/algebra/ac.lean
new file mode 100644
index 0000000000..75644bbe2c
--- /dev/null
+++ b/library/init/algebra/ac.lean
@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.logic
+universe variables u
+
+class is_associative (α : Type u) (r : α → α → Prop) (op : α → α → α) :=
+(assoc : ∀ a b c, r (op (op a b) c) (op a (op b c)))
+
+class is_commutative (α : Type u) (r : α → α → Prop) (op : α → α → α) :=
+(comm : ∀ a b, r (op a b) (op b a))
+
+class is_eq_associative (α : Type u) (op : α → α → α) extends is_associative α eq op
+
+class is_eq_commutative (α : Type u) (op : α → α → α) extends is_commutative α eq op
diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean
index 1bea68d0b4..0d09ec6ae3 100644
--- a/library/init/algebra/group.lean
+++ b/library/init/algebra/group.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 -/
 prelude
-import init.logic init.meta.interactive init.meta.decl_cmds
+import init.logic init.algebra.ac init.meta.interactive init.meta.decl_cmds
 
 /- Make sure instances defined in this file have lower priority than the ones
    defined for concrete structures -/
@@ -38,9 +38,15 @@ class comm_group (α : Type u) extends group α, comm_monoid α
 @[simp] lemma mul_assoc [semigroup α] : ∀ a b c : α, a * b * c = a * (b * c) :=
 semigroup.mul_assoc
 
+instance semigroup_to_is_eq_associative [semigroup α] : is_eq_associative α mul :=
+⟨mul_assoc⟩
+
 @[simp] lemma mul_comm [comm_semigroup α] : ∀ a b : α, a * b = b * a :=
 comm_semigroup.mul_comm
 
+instance comm_semigroup_to_is_eq_commutative [comm_semigroup α] : is_eq_commutative α mul :=
+⟨mul_comm⟩
+
 @[simp] lemma mul_left_comm [comm_semigroup α] : ∀ a b c : α, a * (b * c) = b * (a * c) :=
 left_comm mul mul_comm mul_assoc
 
@@ -278,6 +284,12 @@ run_command transport_to_additive `eq_mul_of_inv_mul_eq `eq_add_of_neg_add_eq
 run_command transport_to_additive `mul_eq_of_eq_inv_mul `add_eq_of_eq_neg_add
 run_command transport_to_additive `mul_eq_of_eq_mul_inv `add_eq_of_eq_add_neg
 
+instance add_semigroup_to_is_eq_associative [add_semigroup α] : is_eq_associative α add :=
+⟨add_assoc⟩
+
+instance add_comm_semigroup_to_is_eq_commutative [add_comm_semigroup α] : is_eq_commutative α add :=
+⟨add_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