Class extension example

extends_product.lean

/- The goal of this file is to explain why it's important that using extends in
   command `class foo extends bar` creates a `foo.to_bar` function with an 
   instance implicit parameter.
   
   We will define magmas with law denoted by ◆ and a commutative version.
   Then we want products of such things. The goal is to reuse the work on product
   magmas when defining product commutative magmas, and do so in a completely
   transparent way. -/

-- Defining magmas with some notation is already covered in TPIL

class has_op (α : Type) :=
(op : α → α → α)

local infix `◆`:70 := has_op.op 
/- Side note: 
   Failing to indicate some precedence would make `a ◆ b = b ◆ a` confusing to the 
   parser -/

-- Now move to the commutative version
class comm_magma (α : Type) extends has_op α :=
(op_comm : ∀ a b : α, a ◆ b = b ◆ a)

#print prefix comm_magma
/- Note the line:
   `comm_magma.to_has_op : Π (α : Type) [c : comm_magma α], has_op α`
   where `c` is an instance implicit parameter, ie to be automatically filled 
   in by the type class resolution mechanism -/

-- Now define product magmas with `◆` operation
instance prod.has_op {α β: Type} [has_op α] [has_op β] : has_op (α × β):= 
⟨λ a b, (a.1 ◆ b.1, a.2 ◆ b.2)⟩

#check @prod.has_op
-- `prod.has_op : Π {α β : Type} [_inst_1 : has_op α] [_inst_2 : has_op β], has_op (α × β)`
-- Note both `has_op` arguments are instance implicit

open comm_magma -- to shorten `comm_magma.op_comm` to `op_comm` in the proofs below

-- First try at a product of commutative magma, redoing the work
instance prod.comm_magma {α β: Type} [comm_magma α] [comm_magma β] : 
  comm_magma (α × β):=
{ op := λ a b, (a.1 ◆ b.1, a.2 ◆ b.2),
  op_comm := λ a b, calc 
    a ◆ b = (a.1 ◆ b.1, a.2 ◆ b.2) : rfl
      ... = (b.1 ◆ a.1, b.2 ◆ a.2) : by {rw op_comm a.1, rw op_comm a.2} }

-- the first piece was copy-paste from `prod.has_op`: this is wasteful

-- Try again:
instance prod.comm_magma' {α β: Type} [comm_magma α] [comm_magma β] : 
  comm_magma (α × β):=
{ op_comm := λ a b, calc 
    a ◆ b = (a.1 ◆ b.1, a.2 ◆ b.2) : rfl
      ... = (b.1 ◆ a.1, b.2 ◆ a.2) : by {rw op_comm a.1, rw op_comm a.2},
  ..prod.has_op } 


/- After filling explicitly the `op_comm` field, the `..` syntax is looking 
   for the missing `op` field, which should have type `α × β → α × β → α × β`.
   `prod.has_op` produces a term having a `op` field with such type. But it consumes
   instance implicit arguments with type `has_op α` and `has_op β`. 
   What we directly have from the declared type of `prod.comm_magma'` are 
   `comm_magma α` and `comm_magma b` arguments. This is then chained using the
   automatically generated instance `comm_magma.to_has_op`, since the later has 
   `comm_magma` instance implicit argument. So the automatically generated 
   `comm_magma.to_has_op` and the type class resolution mechanism took care of
   everything for us. 
  
   Side note:
   We also used that α and β are implicit arguments in prod.has_op, otherwise 
   the last line above would have been ..prod.has_op α β (or ..prod.has_op _ _) -/