Zulip Chat Archive

Stream: Is there code for X?

Topic: Should I be using has_dist vs abbreviation metric


view this post on Zulip Lars Ericson (Dec 07 2020 at 00:58):

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

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 01:05):

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?

view this post on Zulip Lars Ericson (Dec 07 2020 at 03:09):

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.

view this post on Zulip Johan Commelin (Dec 07 2020 at 06:07):

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).

view this post on Zulip Lars Ericson (Dec 07 2020 at 14:08):

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?

view this post on Zulip Lars Ericson (Dec 08 2020 at 04:19):

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 ℝ

view this post on Zulip Lars Ericson (Dec 08 2020 at 13:52):

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

view this post on Zulip Eric Wieser (Dec 08 2020 at 14:08):

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

view this post on Zulip Lars Ericson (Dec 08 2020 at 14:58):

Thanks, fixed.


Last updated: May 16 2021 at 05:21 UTC