Class extension and instance/reference

Stream: new members

[Luiz Kazuo Takei]

Suppose I have a class that just extends two other classes:

class TC (α : Type) extends Add α, Mul α

Now I define an object Rn n and make it an instance of Add and Mul:

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

instance : Add (Rn n) where
  add := fun v w : (Rn n) ↦ (fun i ↦ v i + w i)
instance : Mul (Rn n) where
  mul := fun v w : (Rn n) ↦ (fun i ↦ v i * w i)

My understanding is that, from now on, Lean detects that Rn n is an instance of Add, making this work:

example : Add (Rn n) := inferInstance

But, when I check if Lean automatically knows that Rn n is an instance of TC, it doesn't work:

example : TC (Rn n) := inferInstance

I have two questions:

1. The more practical one is: how can I make Lean understand that Rn n is an instance of TC?
2. The more subtle question is: how come Lean doesn't automatically recognize that Rn n is an instance of TC?

[Ruben Van de Velde]

Presumably there's a typo in your last snippet

[Luiz Kazuo Takei]

Thanks @Ruben Van de Velde. Typo fixed!

[Ruben Van de Velde]

I understand it's possible to add instance [Add X] [Mul X] : TC X := TC.mk or similar

[Luiz Kazuo Takei]

Thanks. A related question. Suppose I only declare that Rn n is an instance of Add:

class TC (α : Type) extends Add α, Mul α

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

instance : Add (Rn n) where
  add := fun v w : (Rn n) ↦ (fun i ↦ v i + w i)

and now I want to declare that Rn n is an instance of TC. How can I tell Lean to use the instance of Add so that I can just define Mul?

instance : TC (Rn n) := sorry

[Kenny Lau]

@Luiz Kazuo Takei it is automatic:

import Mathlib

class TC (α : Type) extends Add α, Mul α

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

instance : Add (Rn n) where
  add := fun v w : (Rn n) ↦ (fun i ↦ v i + w i)

instance : TC (Rn n) where
  mul := sorry

[Luiz Kazuo Takei]

Thanks!

[Eric Wieser]

Ruben Van de Velde said:

I understand it's possible to add instance [Add X] [Mul X] : TC X := TC.mk or similar

This indeed works (and is cleaner as attribute [instance] TC.mk), but is usually a bad idea

[Luiz Kazuo Takei]

@Eric Wieser, I am not sure I understand. You're saying it's better to use attribute [instance] TC.mk? Do you mind showing how that would fit in the code? I had never seen this before.

[Eric Wieser]

That spelling is better than Ruben's for minor reasons, but both are not a great idea performance-wise as they make a loop

[Eric Wieser]

As for how to use it, you just add it as a line by itself after your class