Basics of class and instance

Stream: new members

[Luiz Kazuo Takei]

I am trying to understand class and instance and have the following code:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.Ring

namespace TestClass

class AddComm (α : Type) extends Add α where
  add_comm : ∀ (x y : α), x + y = y + x

def Wn (n : ℕ) : Type := Fin n → ℝ

Now I want to show that (Wn n) with the obvious addition is an instance of AddComm and tried this:

instance (n : ℕ) : AddComm (Wn n) where
  add u v := fun i ↦ u i + v i
  add_comm := by
    intro x y
    funext i
    ring

Lean tells me that the ring tactic failed to close the goal. Could someone tell me why?

Also, and probably related to the question above, when I check the Lean InfoView, I see that it does not convert (x + y) i into x i + y i. Why is that?

[Aaron Liu]

typeclass can't see through the definition of Wn

[Aaron Liu]

btw this is docs#AddCommMagma

[Riccardo Brasca]

Are you importing the fact that the reals are a ring?

[Aaron Liu]

yes

[Aaron Liu]

docs#Real.instRing

[Aaron Liu]

well ring needs docs#Real.instCommSemiring

[Kenny Lau]

Luiz Kazuo Takei said:

I see that it does not convert (x + y) i into x i + y i. Why is that?

every time you make a new definition (which includes Wn), you need to include all of the simp lemmas you need to interact with said new object

[Riccardo Brasca]

Ah yes, it's difficult to guess the error with a phone and no infowiew :sweat_smile:. The error is that ring cannot see that (x + y) i = x i + y i automatically

[Riccardo Brasca]

Those are equal by definition, but still two different objects as far as Lean is concerned

[Luiz Kazuo Takei]

Correct me if I am wrong but I think the fact that reals are ring are imported when I say

import Mathlib.Data.Real.Basic

Also, it seems like Lean is having difficulties interpreting (x + y) i. In fact, when I tried this:

instance (n : ℕ) : AddComm (Wn n) where
  add u v := fun i ↦ u i + v i
  add_comm := by
    intro x y
    funext i
    calc
      (x + y) i = x i + y i := by rfl
      _ = y i + x i := by apply add_comm
      _ = (y + x) i := by rfl

I got an error message in the first line of calc. More specifically, it underlines the (x + y) and says that

failed to synthesize
HAdd (Wn n) (Wn n) ?m.48

[Luiz Kazuo Takei]

Ok. I tried the code below and it worked. It seems like if I first declare an instance of Add (only defining addition) and then declare an instance of AddComm (proving it is commutative), then it works.

Why can't I just declare an instance of AddComm (defining addition and proving it is commutative) in one step?

instance (n : ℕ) : Add (Wn n) where
  add u v := fun i ↦ u i + v i

instance (n : ℕ) : AddComm (Wn n) where
  add_comm := by
    intro x y
    funext i
    calc
      (x + y) i = x i + y i := by rfl
      _ = y i + x i := by apply add_comm
      _ = (y + x) i := by rfl

[Riccardo Brasca]

The problem here is that you should define the Add instance before, and then prove that addition is commutative.

import Mathlib.Data.Real.Basic

namespace TestClass

class AddComm (α : Type) extends Add α where
  add_comm : ∀ (x y : α), x + y = y + x

def Wn (n : ℕ) : Type := Fin n → ℝ

instance (n : ℕ) : Add (Wn n) where
  add u v := fun i ↦ u i + v i

instance (n : ℕ) : AddComm (Wn n) where
  add_comm := by
    intro x y
    funext i
    calc
      (x + y) i = x i + y i := by rfl
      _ = y i + x i := by apply add_comm
      _ = (y + x) i := by rfl

end TestClass

[Riccardo Brasca]

This is probably an issue with calc, but I am not 100% sure.

[Riccardo Brasca]

import Mathlib.Data.Real.Basic

namespace TestClass

class AddComm (α : Type) extends Add α where
  add_comm : ∀ (x y : α), x + y = y + x

def Wn (n : ℕ) : Type := Fin n → ℝ

instance (n : ℕ) : AddComm (Wn n) where
  add u v := fun i ↦ u i + v i
  add_comm := by
    intro x y
    funext i
    show x i + y i = y i + x i
    rw [add_comm]

end TestClass

also works.

[Riccardo Brasca]

(The issue with calc is, I think, that it cannot use the expected type to find the HAdd instance. We cannot make it smarter for technical reasons)

[Luiz Kazuo Takei]

Thanks a lot!

[Aaron Liu]

Riccardo Brasca said:

(The issue with calc is, I think, that it cannot use the expected type to find the HAdd instance. We cannot make it smarter for technical reasons)

No this is actually not it

[Aaron Liu]

The issue is not with calc

[Aaron Liu]

if you define the addition and commutativity in one go then the addition hadn't finished being defined at the time you're proving commutativity

[Aaron Liu]

so it's not available to typeclass

[Riccardo Brasca]

Ah OK, I thought it somehow did it, since in the infoview (x + y) i is shown, so something related to Add is found.

[Luiz Kazuo Takei]

Thanks for the input @Aaron Liu but I have a question.

I tried this

class MyAdd (α : Type) where
  add : α → α → α
infixl:70 " ⋄ " => MyAdd.add

class AddComm (α : Type) extends MyAdd α where
  add_comm : ∀ (x y : α), x ⋄ y = y ⋄ x

def Wn (n : ℕ) : Type := Fin n → ℝ

instance (n : ℕ) : AddComm (Wn n) where
  add u v := fun i ↦ u i + v i
  add_comm := by
    intro x y
    funext i
    ring

And now it works. In the Lean InfoView, it doesn't even show (u + v) i when I try to show add_comm. In fact, it already applies the definition and it shows the goal as

∀ (x y : Wn n), (fun i ↦ x i + y i) = fun i ↦ y i + x i

So, if I use Lean's built-in class Add, it doesn't understand the definition. On the other hand, if I use a custom-made MyAdd class, it does. Why?

[Aaron Liu]

That's because when you use Add it goes through HAdd.hAdd