unbundled_classes.lean

/-
Experimenting with unbundled classes.
Author: Jeremy Avigad

Definitions are in the namespace "experiment" to avoid clashing with definitions in init.
-/
namespace experiment

/-
Calculation lemmas for multiplicative notation.
-/

section mul_lemmas
variables {α : Type*}

lemma mul_assoc [has_mul α] [h : is_associative α (*)] : ∀ a b c : α, a * b * c = a * (b * c) :=
h.assoc

lemma mul_comm [has_mul α] [h : is_commutative α (*)] : ∀ a b : α, a * b = b * a :=
h.comm

lemma one_mul [has_mul α] [has_one α] [h : is_left_id α (*) 1] : ∀ a : α, 1 * a = a :=
h.left_id

lemma mul_one [has_mul α] [has_one α] [h : is_right_id α (*) 1] : ∀ a : α, a * 1 = a :=
h.right_id

lemma mul_left_inv [has_mul α] [has_one α] [has_inv α] [h : is_left_inv α (*) has_inv.inv 1] : ∀ a : α, a⁻¹ * a = 1 :=
h.left_inv

-- alternate name
lemma inv_mul [has_mul α] [has_one α] [has_inv α] [h : is_left_inv α (*) has_inv.inv 1] : ∀ a : α, a⁻¹ * a = 1 :=
h.left_inv

lemma mul_inv [has_mul α] [has_one α] [has_inv α] [h : is_right_inv α (*) has_inv.inv 1] : ∀ a : α, a * a⁻¹ = 1 :=
h.right_inv

-- alternate name
lemma mul_right_inv {hm : has_mul α} {ho : has_one α} {hi : has_inv α} [h : is_right_inv α (*) has_inv.inv 1] : ∀ a : α, a * a⁻¹ = 1 :=
h.right_inv

lemma mul_left_cancel [has_mul α] [h : is_left_cancel α (*)] : ∀ {a b c : α}, a * b = a * c → b = c :=
h.left_cancel

lemma mul_right_cancel [has_mul α] [h : is_right_cancel α (*)] : ∀ {a b c : α}, a * b = c * b → a = c :=
h.right_cancel

@[simp] lemma mul_left_comm [has_mul α] [h : is_associative α (*)] [h' : is_commutative α (*)] : ∀ a b c : α, a * (b * c) = b * (a * c) :=
left_comm (*) h'.comm h.assoc

lemma mul_right_comm [has_mul α] [h : is_associative α (*)] [h' : is_commutative α (*)]  : ∀ a b c : α, a * b * c = a * c * b :=
right_comm (*) h'.comm h.assoc

lemma mul_left_cancel_iff [has_mul α] [is_left_cancel α (*)] {a b c : α} : a * b = a * c ↔ b = c :=
⟨mul_left_cancel, by intro h; rw h⟩

lemma mul_right_cancel_iff [has_mul α] [is_right_cancel α (*)] {a b c : α} : b * a = c * a ↔ b = c :=
⟨mul_right_cancel, by intro h; rw h⟩

end mul_lemmas

/- additive versions -/

section add_lemmas
variable {α : Type*}

@[simp] lemma add_assoc [has_add α] [h : is_associative α (+)] : ∀ a b c : α, a + b + c = a + (b + c) :=
h.assoc

@[simp] lemma add_comm [has_add α] [h : is_commutative α (+)] : ∀ a b : α, a + b = b + a :=
h.comm

@[simp] lemma zero_add [has_add α] [has_zero α] [h : is_left_id α (+) 0] : ∀ a : α, 0 + a = a :=
h.left_id

@[simp] lemma add_zero [has_add α] [has_zero α] [h : is_right_id α (+) 0] : ∀ a : α, a + 0 = a :=
h.right_id

@[simp] lemma add_left_neg [has_add α] [has_zero α] [has_neg α] [h : is_left_inv α (+) has_neg.neg 0] : ∀ a : α, -a  + a = 0 :=
h.left_inv

-- alternate name
lemma neg_add [has_add α] [has_zero α] [has_neg α] [h : is_left_inv α (+) has_neg.neg 0] : ∀ a : α, -a  + a = 0 :=
h.left_inv

@[simp] lemma add_neg [has_add α] [has_zero α] [has_neg α] [h : is_right_inv α (+) has_neg.neg 0] : ∀ a : α, a + -a = 0 :=
h.right_inv

-- alternate name
lemma add_right_neg {hm : has_add α} {ho : has_zero α} {hi : has_neg α} [h : is_right_inv α (+) has_neg.neg 0] : ∀ a : α, a + -a = 0 :=
h.right_inv

lemma add_left_cancel [has_add α] [h : is_left_cancel α (+)] : ∀ {a b c : α}, a + b = a + c → b = c :=
h.left_cancel

lemma add_right_cancel [has_add α] [h : is_right_cancel α (+)] : ∀ {a b c : α}, a + b = c + b → a = c :=
h.right_cancel

@[simp] lemma add_left_comm [has_add α] [h : is_associative α (+)] [h' : is_commutative α (+)] : ∀ a b c : α, a + (b + c) = b + (a + c) :=
left_comm (+) h'.comm h.assoc

lemma add_right_comm [has_add α] [h : is_associative α (+)] [h' : is_commutative α (+)]  : ∀ a b c : α, a + b + c = a + c + b :=
right_comm (+) h'.comm h.assoc

lemma add_left_cancel_iff [has_add α] [is_left_cancel α (+)] {a b c : α} : a + b = a + c ↔ b = c :=
⟨add_left_cancel, by intro h; rw h⟩

lemma add_right_cancel_iff [has_add α] [is_right_cancel α (+)] {a b c : α} : b + a = c + a ↔ b = c :=
⟨add_right_cancel, by intro h; rw h⟩

end add_lemmas

/-
First, let's try coding groups in a very unbundled way. We can then use the class to support
calculations with multiplicative notation, additive notation, and even (with some extra work) no
notation at all.
-/

class is_group (α : Type*) (op : α → α → α) (i : α) (inv : α → α) extends
  is_associative α op,
  is_left_id α op i,
  is_right_id α op i,
  is_left_inv α op inv i,
  is_right_inv α op inv i

-- multiplicative calculation
section examples
variables {α : Type*} [has_mul α] [has_one α] [has_inv α]
variables [is_group α (*) 1 has_inv.inv]

example (x : α) : x * 1 = x := mul_one _

example (x y : α) : x * y * y⁻¹ * x⁻¹ = 1 :=
by rw [mul_assoc x, mul_inv, mul_one, mul_inv]

variable [is_commutative α (*)]

example (x y : α) : x * y * x⁻¹ * y⁻¹ = 1 :=
by rw [mul_comm x, mul_assoc y, mul_inv, mul_one, mul_inv]

end examples

-- additive calculation
section examples
variables {α : Type*} [has_add α] [has_zero α] [has_neg α]
variables [is_group α (+) 0 has_neg.neg]

example (x : α) : x + 0 = x := add_zero _

example (x y : α) : x + y + -y + -x = 0 :=
by rw [add_assoc x, add_neg, add_zero, add_neg]

variable [is_commutative α (+)]

example (x y : α) : x + y + -x + -y = 0 :=
by rw [add_comm x, add_assoc y, add_neg, add_zero, add_neg]

end examples

-- generic calculation
section examples
variables {α : Type*} (op : α → α → α) (i : α) (inv : α → α)
variables [h : is_group α op i inv]
include h

local notation `id`  := i
local infix    ` ∘ ` := op
local postfix  `⁻¹`  := inv

local notation `op_assoc` := is_associative.assoc (∘)
local notation `op_inv`   := is_right_inv.right_inv (∘)
local notation `op_id`    := is_right_id.right_id (∘)

example (x : α) : x ∘ id = x := op_id _

example (x y : α) : x ∘ y ∘ y⁻¹ ∘ x⁻¹ = id :=
by rw [op_assoc x, op_inv, op_id, op_inv]

variable [is_commutative α (∘)]

local notation `op_comm` := is_commutative.comm (∘)

example (x y : α) : x ∘ y ∘ x⁻¹ ∘ y⁻¹ = id :=
by rw [op_comm x, op_assoc y, op_inv, op_id, op_inv]

end examples

/-
Now, suppose for some reason we want to bundle the structure and bundle the axioms, but leave the
type as a parameter. We can still use the unbundled theorems.

Note: I don't see why we might want to do this. To do group theory, we probably want to go straight
to the fully bundled version.
-/

class group_struc (α : Type*) extends has_mul α, has_one α, has_inv α
class is_group_struc (α : Type*) [group_struc α] extends is_group α (*) 1 has_inv.inv

class add_group_struc (α : Type*) extends has_add α, has_zero α, has_neg α
class is_add_group_struc (α : Type*) [add_group_struc α] extends has_add α, has_zero α, has_neg α

section examples
variables {α : Type*} [group_struc α] [is_group_struc α]

-- there are exactly the same as before!

example (x : α) : x * 1 = x := mul_one _

example (x y : α) : x * y * y⁻¹ * x⁻¹ = 1 :=
by rw [mul_assoc x, mul_inv, mul_one, mul_inv]

variable [is_commutative α (*)]

example (x y : α) : x * y * x⁻¹ * y⁻¹ = 1 :=
by rw [mul_comm x, mul_assoc y, mul_inv, mul_one, mul_inv]

end examples

/-
Fully bundled groups.
-/

class Group :=
(carrier  : Type*)
(struc    : group_struc carrier)
(is_group : is_group_struc carrier)

instance has_coe_to_sort : has_coe_to_sort Group := ⟨_, @Group.carrier⟩

instance (G : Group) : group_struc G := G.struc
instance (G : Group) : is_group_struc G := G.is_group

section examples
variable (G : Group)

-- there are exactly the same as before!

example (x : G) : x * 1 = x := mul_one _

example (x y : G) : x * y * y⁻¹ * x⁻¹ = 1 :=
by rw [mul_assoc x, mul_inv, mul_one, mul_inv]

variable [is_commutative G (*)]

example (x y : G) : x * y * x⁻¹ * y⁻¹ = 1 :=
by rw [mul_comm x, mul_assoc y, mul_inv, mul_one, mul_inv]

end examples

end experiment