instance shenanigans

Stream: new members

[Pim Otte]

Context: I'm trying to formalize something where the goal is to stick close to the original text (this concerns theorem 1.34 of this book). Suitability for mathlib is not a consideration.

I would like to state and be able to work with two norms on a space. Now, these are usually worked with as typeclasses, and this is where my issue lies. I figured I would just add the objects as explicit parameters, rather than instance-implicits. However, this means they still get used for instance search within the proof. In the code below this quickly causes issues when it can't infer the fintype of the index because of this mix of instances.

Is there a way I could locally exclude n1/n2/s1/s2 from being used in instance search? Or is there an alternative formulation that allows me to work with two norms in the same context?

import Mathlib.Analysis.RCLike.Basic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs


variable {𝕂 : Type _} {V : Type _} [RCLike 𝕂] [nacg : NormedAddCommGroup V] [ns : NormedSpace 𝕂 V]

open Module

def norm_equiv (norm1 : V → ℝ) (norm2 : V → ℝ) : Prop :=
  ∃ c > 0, ∃ C ≥ c, ∀ x : V, c * norm1 x ≤ norm2 x ∧ norm2 x ≤ C * norm1 x

theorem norm_equiv_of_finite_dimensional
  [h : FiniteDimensional 𝕂 V]
  (n1 : NormedAddCommGroup V)
  (n2 : NormedAddCommGroup V)
  (s1 : @NormedSpace 𝕂 V _ n1.toSeminormedAddCommGroup)
  (s2 : @NormedSpace 𝕂 V _ n2.toSeminormedAddCommGroup) :
  norm_equiv n1.norm n2.norm := by

  let ι := Basis.ofVectorSpaceIndex 𝕂 V
  let basis : Basis ι 𝕂 V := Basis.ofVectorSpace 𝕂 V
  -- haveI : Fintype (Basis.ofVectorSpaceIndex 𝕂 V) := by
    -- infer_instance
    -- exact @FiniteDimensional.fintypeBasisIndex _ _ _ _ _ _ h _
    -- sorry

  let euclidean_norm (v : V) : ℝ :=
    Real.sqrt (∑ i, ‖basis.coord i v‖ ^ 2)

  sorry

[Etienne Marion]

Apart from writing everything with @ to provide instance parameters explicitly I don't see another way, this is kind of anti-lean. What you could do is use another type which is isomorphic but with a different norm, but I guess this will depart from the book.

[Aaron Liu]

why do you have two norms

[Aaron Liu]

I think there was a better way to write this

[Pim Otte]

Because the theorem is to show that different norms are equivalent.

I've thought about it for a bit and I think this might work, but I'd still love something less involved.

import Mathlib.Analysis.RCLike.Basic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs


variable {𝕂 : Type _} {V : Type _} [RCLike 𝕂] [nacg : NormedAddCommGroup V] [ns : NormedSpace 𝕂 V]

open Module

def norm_equiv (norm1 : V → ℝ) (norm2 : V → ℝ) : Prop :=
  ∃ c > 0, ∃ C ≥ c, ∀ x : V, c * norm1 x ≤ norm2 x ∧ norm2 x ≤ C * norm1 x

structure Fa.Norm (𝕂 : Type _) (V : Type _) [RCLike 𝕂] where
  nacg : NormedAddCommGroup V
  ns : @NormedSpace 𝕂 V _ nacg.toSeminormedAddCommGroup

def Fa.Norm.norm (n : Fa.Norm 𝕂 V) : V → ℝ := n.nacg.norm

theorem norm_equiv_of_finite_dimensional
  [h : FiniteDimensional 𝕂 V]
  (norm1 : Fa.Norm 𝕂 V)
  (norm2 : Fa.Norm 𝕂 V) :
  norm_equiv norm1.norm norm2.norm := by
  let ι := Basis.ofVectorSpaceIndex 𝕂 V
  let basis : Basis ι 𝕂 V := Basis.ofVectorSpace 𝕂 V
  let euclidean_norm (v : V) : ℝ :=
    Real.sqrt (∑ i, ‖basis.coord i v‖ ^ 2)

  sorry

[Aaron Liu]

found docs#AddGroupNorm

[Aaron Liu]

I think for a NormedSpace it would be docs#Seminorm

[Kenny Lau]

the way i would do things like this is to spend as little time possible in a situation where I have two typeclasses on the same type, i.e. I might state a lemma with two unbundled norms (i.e. as plain functions) and then do everything there, and then make the main theorem to be just an application of the lemma in as little lines as possible

[Kenny Lau]

you can see an example of this here where this is the only theorem I explicitly use @ and stuff, and in the surrounding theorems I only ever have one instance

[Kenny Lau]

yeah I think the last code you posted is something along these lines.