IMPAN demo: classes

classes.lean

import demo.structures

/-! # Classes

Define a class (e.g. `monoid`)
and define an instance (e.g. product monoid).

-/

namespace impan

variables (M N : Type)

-- the unit element on a product
instance prod.has_one [has_one M] [has_one N] :
  has_one (M ⊠ N) :=
{ one := ⟨1,1⟩ }

-- the multiplication on a product
instance prod.has_mul [has_mul M] [has_mul N] :
  has_mul (M ⊠ N) :=
{ mul := _ }

@[simp]
lemma one_fst [has_one M] [has_one N] :
  (1 : M ⊠ N).fst = 1 :=
_

@[simp]
lemma one_snd [has_one M] [has_one N] :
  (1 : M ⊠ N).snd = 1 :=
_

@[simp]
lemma mul_fst [has_mul M] [has_mul N]
  (x y : M ⊠ N) :
  (x * y : M ⊠ N).fst = _ :=
_

@[simp]
lemma mul_snd [has_mul M] [has_mul N]
  (x y : M ⊠ N) :
  (x * y : M ⊠ N).snd = _ :=
_


class monoid (M : Type)
  extends has_one M, has_mul M :=
(one_mul : ∀ m : M, 1 * m = m)
-- (mul_one : _)
-- (mul_assoc : _)

export monoid (one_mul) -- add the rest

attribute [simp] one_mul -- add the rest

instance (M N : Type)
  [monoid M] [monoid N] :
  monoid (M ⊠ N) :=
{ one := 1,
  mul := (*),
  /- fix the errors -/ }

end impan