Refine HMul to specific instance

Stream: new members

[Edmund Lam]

Hi, I am unsure of how to refine a general HMul.hMul to a specific defined instance when proving properties about an instance. I wrote a simple group class as follows:

class Group (G: Type u) where
  identity: G
  mul: G -> G -> G
  mul_assoc: ∀ a b c: G, mul a (mul b c) = mul (mul a b) c
  mul_identity: ∀ a: G, mul identity a = a ∧ mul a identity = a
  mul_inv: ∀ a: G, ∃ a₁: G, mul a a₁ = identity ∧ mul a₁ a = identity

instance : Group Int where
  identity := 0
  mul := Int.add
  mul_assoc := by
    intros a b c
    simp_arith[]
    rw [Int.add_assoc]
  mul_identity := by
    simp_arith[]
  mul_inv := by
    intros a
    exists -a
    simp_arith[]
    rw [Int.add_right_neg, Int.add_left_neg]
    trivial

Everything compiles as expected but I wanted to make Group G extend Mul G so that I can use nice notation

class Group (G: Type u) extends Mul G where
  identity: G
  mul_assoc: ∀ a b c: G, a * (b * c) = (a * b) * c
  mul_identity: ∀ a: G, identity *  a = a ∧ a * identity = a
  mul_inv: ∀ a: G, ∃ a₁: G, a * a₁ = identity ∧ a₁ * a = identity

But simp_arith is no longer able to make progress as it is not sure what to do with the multiplies which have now become @HMul.hMul Int Int Int instHMul b c : Int with@instHMul Int { mul := Int.add } : HMul Int Int Int. How can I tell the solver that HMul is actually Int.add for an integer group on addition?

[Yaël Dillies]

You could do

instance : Mul Int where
  mul := Int.add

@[simp] lemma mul_eq_add (m n : Int) : m * n = Int.add m n := rfl

instance : Group Int where
  identity := 0
  mul_assoc := by
    intros a b c
    simp_arith[]
    rw [Int.add_assoc]
  mul_identity := by
    simp_arith[]
  mul_inv := by
    intros a
    exists -a
    simp_arith[]
    rw [Int.add_right_neg, Int.add_left_neg]
    trivial

[Yaël Dillies]

Though you might want to do your experiments on a type other than Int, which already comes with a (different) Mul instance

[Edmund Lam]

I see, is the specific issue I am having occurring because I am using a type that already has conflicting mul or would I have to generally do this for any group I define?

[Yaël Dillies]

This is something you should be able to figure out for yourself :wink:

[Kyle Miller]

Here's a hint for handling the conflict: instead of making a Group Int instance, make a Group AddInt instance with

def AddInt := Int
def AddInt.mk (n : Int) : AddInt := n

[Edmund Lam]

Even with a new type defined it seems like I still need the lemma, am I totally on the wrong track? I now have

def GInt := Int
def GInt.mk (n: Int) : GInt := n

instance : Mul GInt where
  mul := Int.add

@[simp] theorem mul_add (m n: GInt) : m * n = Int.add m n := rfl

instance : Group GInt where
  identity := GInt.mk 0
  mul_assoc := by
    intros a b c
    repeat rw [mul_add]
    simp[]
    rw [Int.add_assoc]

[Kevin Buzzard]

For some reason you have to fill in the mul field still (I am surprised) (but at least you can now fill it in with what you want it to look like...)

def GInt := Int
def GInt.mk (n: Int) : GInt := n

instance : Mul GInt where
  mul := Int.add

@[simp] theorem mul_add (m n: GInt) : m * n = Int.add m n := rfl

universe u

class Group (G: Type u) where
  identity: G
  mul: G -> G -> G
  mul_assoc: ∀ a b c: G, mul a (mul b c) = mul (mul a b) c
  mul_identity: ∀ a: G, mul identity a = a ∧ mul a identity = a
  mul_inv: ∀ a: G, ∃ a₁: G, mul a a₁ = identity ∧ mul a₁ a = identity

instance : Group GInt where
  mul := (· * ·)
  identity := GInt.mk 0
  mul_assoc := by
    intros a b c
    repeat rw [mul_add]
    simp[]
    rw [Int.add_assoc]
  mul_identity := sorry
  mul_inv := sorry

[Edmund Lam]

I don't have to anymore because I have Group extends Mulwith

class Group (G: Type u) extends Mul G where
  identity: G
  mul_assoc: ∀ a b c: G, a * (b * c) = (a * b) * c
  mul_identity: ∀ a: G, identity *  a = a ∧ a * identity = a
  mul_inv: ∀ a: G, ∃ a₁: G, a * a₁ = identity ∧ a₁ * a = identity

which is where all the issues came from regarding needing mul_add. Still not sure whether that can be gotten rid of...

[Edmund Lam]

As an aside, I don't have the lemma keyword, is this a mathlib specific keyword or something? I can only use theorem.

[Kevin Buzzard]

Lemma: yes this is mathlib-specific because core doesn't like two words for exactly the same thing but mathematicians find it extremely hard to call the thousands of trivialities in mathlib "theorems", so it's cultural more than anything else.

[Aaron Liu]

Edmund Lam said:

As an aside, I don't have the lemma keyword, is this a mathlib specific keyword or something? I can only use theorem.

Yes, it's in file#Tactic/Lemma.

[Kevin Buzzard]

Fortunately the principle that the proofs all the lemmas in mathlib should be strictly shorter than the proofs of all the theorems does not seem to be enforced in that file.

[Edmund Lam]

Cool, thanks!