From 4ef7d83445dbab8039f645bf570180da9241358b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Nov 2020 18:58:42 -0800
Subject: [PATCH] test: bundled structures

---
 tests/lean/run/alg.lean  |  2 +-
 tests/lean/run/balg.lean | 92 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 93 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/balg.lean

diff --git a/tests/lean/run/alg.lean b/tests/lean/run/alg.lean
index 61347de425..afc4fa6c40 100644
--- a/tests/lean/run/alg.lean
+++ b/tests/lean/run/alg.lean
@@ -67,4 +67,4 @@ theorem mul_inv_rev [Group α] (a b : α) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
   rw [mul_assoc, ← mul_assoc b, mul_right_inv, one_mul, mul_right_inv]
 
 theorem mul_inv [CommGroup α] (a b : α) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by
-  rewrite [mul_inv_rev, mul_comm]; rfl
+  rw [mul_inv_rev, mul_comm]; rfl
diff --git a/tests/lean/run/balg.lean b/tests/lean/run/balg.lean
new file mode 100644
index 0000000000..62fb44f248
--- /dev/null
+++ b/tests/lean/run/balg.lean
@@ -0,0 +1,92 @@
+universe u
+
+structure Magma where
+  α   : Type u
+  mul : α → α → α
+
+instance : CoeSort Magma (Type u) where
+  coe s := s.α
+
+abbrev mul {M : Magma} (a b : M) : M :=
+  M.mul a b
+
+infix:70 [1] "*" => mul
+
+structure Semigroup extends Magma where
+  mul_assoc (a b c : α) : a * b * c = a * (b * c)
+
+instance : CoeSort Semigroup (Type u) where
+  coe s := s.α
+
+structure CommSemigroup extends Semigroup where
+  mul_comm (a b : α) : a * b = b * a
+
+structure Monoid extends Semigroup where
+  one : α
+  one_mul (a : α) : one * a = a
+  mul_one (a : α) : a * one = a
+
+instance : CoeSort Monoid (Type u) where
+  coe s := s.α
+
+structure CommMonoid extends Monoid where
+  mul_comm (a b : α) : a * b = b * a
+
+instance : Coe CommMonoid CommSemigroup where
+  coe s := {
+      α   := s.α
+      mul := s.mul
+      mul_assoc := s.mul_assoc
+      mul_comm  := s.mul_comm
+    }
+
+structure Group extends Monoid where
+  inv : α → α
+  mul_left_inv (a : α) : (inv a) * a = one
+
+instance : CoeSort Group (Type u) where
+  coe s := s.α
+
+abbrev inv {G : Group} (a : G) : G :=
+  G.inv a
+
+postfix:max "⁻¹" => inv
+
+instance (G : Group) : One (coeSort G.toMagma) where
+  one := G.one
+
+instance (G : Group) : One (G.toMagma.α) where
+  one := G.one
+
+structure CommGroup extends Group where
+  mul_comm (a b : α) : a * b = b * a
+
+instance : CoeSort CommGroup (Type u) where
+  coe s := s.α
+
+theorem inv_mul_cancel_left {G : Group} (a b : G) : a⁻¹ * (a * b) = b := by
+  rw [← G.mul_assoc, G.mul_left_inv, G.one_mul]
+
+theorem toMonoidOneEq {G : Group} : G.toMonoid.one = 1 :=
+  rfl
+
+theorem inv_eq_of_mul_eq_one {G : Group} {a b : G} (h : a * b = 1) : a⁻¹ = b := by
+  rw [← G.mul_one a⁻¹, toMonoidOneEq, ←h, ← G.mul_assoc, G.mul_left_inv, G.one_mul]
+
+theorem inv_inv {G : Group} (a : G) : (a⁻¹)⁻¹ = a :=
+  inv_eq_of_mul_eq_one (G.mul_left_inv a)
+
+theorem mul_right_inv {G : Group} (a : G) : a * a⁻¹ = 1 := by
+  have a⁻¹⁻¹ * a⁻¹ = 1 by rw [G.mul_left_inv]; rfl
+  rw [inv_inv] at this
+  assumption
+
+unif_hint (G : Group) where
+  |- G.toMonoid.one =?= 1
+
+theorem mul_inv_rev {G : Group} (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
+  apply inv_eq_of_mul_eq_one
+  rw [G.mul_assoc, ← G.mul_assoc b, mul_right_inv, G.one_mul, mul_right_inv]
+
+theorem mul_inv {G : CommGroup} (a b : G) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by
+  rw [mul_inv_rev, G.mul_comm]