Should I be using has_dist vs abbreviation metric

Stream: Is there code for X?

[Lars Ericson]

In the following I have an abbreviation metric which says much the same thing as has_dist. Should I be using has_dist here somehow or is this OK? I am trying to define an example metric function prior to defining a metric space that uses it. I feel like I should be able to replace metric X in a function with has_dist X but it doesn't fit exactly:

import data.real.basic
import topology.metric_space.basic

-- Metric: α → α → ℝ

abbreviation metric (α: Type) := α → α → ℝ -- kind of recapitulates has_dist but has_dist α doesn't work as a function type

-- Example 1

abbreviation RealPoint : Type := ℝ × ℝ -- real points

noncomputable def d_taxicab : metric RealPoint := λ x y, (abs (x.1 - y.1)) + (abs (x.2 - y.2))

noncomputable def d_euclid : metric RealPoint := λ x y, real.sqrt ((x.1 - y.1)^2 + (x.2 - y.2)^2)

#check d_taxicab -- d_taxicab : metric RealPoint
#check d_euclid -- d_euclid : metric RealPoint

[Yakov Pechersky]

Providing a has_dist instance for some type, would allow you to say dist and have the function you provided in the has_dist statement be inferred. You will run into issues if you have two separate non-equal has_dist defined for the same type.

Can you give an example (that might not compile) of how you picture using has_dist instead?

[Lars Ericson]

I have

abbreviation metric (α: Type) := α → α → ℝ

and mathlib has

class has_dist (α : Type*) := (dist : α → α → ℝ)

They are declaring the same type for the same purpose.

I am creating a distance function such as

noncomputable def d_L1 : metric ℝ := λ x y, abs (x - y)

This goes into a metric_space such as

noncomputable def MES_L1 : metric_space ℝ :=
{ dist := d_L1,
  dist_self := sorry,
  eq_of_dist_eq_zero := sorry,
  dist_comm := sorry,
  dist_triangle := sorry }

#check MES_L1 -- MES_L1 : metric_space ℝ

It's a very small point but I am just asking whether there is a more mathlib-onic way of declaring d_L1 which uses has_dist so I don't have to create the redundant type abbreviation metric.

[Johan Commelin]

You should not be using abbreviation metric.
You should be using instances of the has_dist typeclass.
You should use those instances via the function dist (which assumes an instance of has_dist as one of its arguments).

[Lars Ericson]

Thank you @Johan Commelin . So the paradigm is to:

• Declare a type of functions which includes my distance function
• Provide that type with a has_dist, like this:

def bounded_continuous_function (α : Type u) (β : Type v) [topological_space α] [metric_space β] :
  Type (max u v) :=
{f : α → β // continuous f ∧ ∃C, ∀x y:α, dist (f x) (f y) ≤ C}

local infixr ` →ᵇ `:25 := bounded_continuous_function

instance : has_dist (α →ᵇ β) :=
⟨λf g, Inf {C | 0 ≤ C ∧ ∀ x : α, dist (f x) (g x) ≤ C}⟩

Can you help me adapt the above example to the case where α = β = ℝ and d= λ x y, abs (x - y), so that the resulting d can be incorporated into the definition of a metric space?

[Lars Ericson]

OK I got it. Section 10.3. Here we go, please correct me if I'm wrong:

import data.real.basic
import topology.metric_space.basic

noncomputable def d_L1 := λ (x y : ℝ), abs (x - y)

noncomputable instance R_has_dist : has_dist ℝ := ⟨ d_L1 ⟩

noncomputable def MES_L1 : metric_space ℝ :=
{ dist := d_L1,
  dist_self := sorry,
  eq_of_dist_eq_zero := sorry,
  dist_comm := sorry,
  dist_triangle := sorry }

#check MES_L1 -- MES_L1 : metric_space ℝ

[Lars Ericson]

Done, revised to avoid instances:

mport data.real.basic
import topology.metric_space.basic

-- Example 1

noncomputable def d_L1 := λ (x y : ℝ), abs (x - y)

noncomputable def R_has_dist_L1 : has_dist ℝ := ⟨ d_L1 ⟩

noncomputable def MES_L1 : metric_space ℝ :=
{ dist := d_L1,
  dist_self := sorry,
  eq_of_dist_eq_zero := sorry,
  dist_comm := sorry,
  dist_triangle := sorry }

#check MES_L1 -- MES_L1 : metric_space ℝ

-- Example 2

noncomputable def d_L2 := λ (x y : ℝ), real.sqrt ((x - y)^2)

noncomputable def R_has_dist_l2 : has_dist ℝ := ⟨ d_L1 ⟩

noncomputable def MES_L2 : metric_space ℝ :=
{ dist := d_L2,
  dist_self := sorry,
  eq_of_dist_eq_zero := sorry,
  dist_comm := sorry,
  dist_triangle := sorry }

#check MES_L2 -- MES_L2 : metric_space ℝ

-- Example 3

abbreviation RealPoint : Type := ℝ × ℝ -- real points

noncomputable def d_taxicab := λ (x y : RealPoint), (abs (x.1 - y.1)) + (abs (x.2 - y.2))

noncomputable def RealPoint_has_dist_taxicab : has_dist RealPoint := ⟨ d_taxicab ⟩

noncomputable def MES_taxicab : metric_space RealPoint :=
{ dist := d_taxicab,
  dist_self := sorry,
  eq_of_dist_eq_zero := sorry,
  dist_comm := sorry,
  dist_triangle := sorry }

#check MES_taxicab -- MES_taxicab : metric_space RealPoint

-- Example 4

noncomputable def d_euclid  := λ (x y : RealPoint), real.sqrt ((x.1 - y.1)^2 + (x.2 - y.2)^2)

noncomputable def RealPoint_has_dist_euclid : has_dist RealPoint := ⟨ d_taxicab ⟩

noncomputable def MES_euclid: metric_space RealPoint :=
{ dist := d_euclid,
  dist_self := sorry,
  eq_of_dist_eq_zero := sorry,
  dist_comm := sorry,
  dist_triangle := sorry }

#check MES_euclid -- MES_taxicab : metric_space RealPoint

[Eric Wieser]

Typo: R_has_dist_l2 : has_dist ℝ := ⟨ d_L1 ⟩ should be R_has_dist_l2 : has_dist ℝ := ⟨ d_L2 ⟩

[Lars Ericson]

Thanks, fixed.