## Stream: Is there code for X?

### Topic: metrics are nonnegative

#### Bjørn Kjos-Hanssen (Dec 03 2020 at 18:21):

I proved that something was a metric_space but now I'm noticing that I was never asked to prove my metric was nonnegative!
Is this a bug?

#### Eric Wieser (Dec 03 2020 at 18:23):

src#dist_nonneg is derived from the triangle equality that you did prove

#### Bjørn Kjos-Hanssen (Dec 03 2020 at 18:24):

Thanks... that's a nice way to set it up

#### Bjørn Kjos-Hanssen (Dec 03 2020 at 19:25):

@Eric Wieser how might I tell dist_nonneg which metric I want to use?

#### Adam Topaz (Dec 03 2020 at 19:27):

Looks like you need an instance of metric_space

#### Bjørn Kjos-Hanssen (Dec 03 2020 at 19:27):

Yes, I have that, but then I'm not sure how to invoke it.

#### Eric Wieser (Dec 03 2020 at 19:27):

In most cases you don't - the way the typeclasses are set up usually means you have exactly one metric per your

#### Adam Topaz (Dec 03 2020 at 19:28):

Did you construct a metric_space instance as a def as opposed to an instance?

#### Bjørn Kjos-Hanssen (Dec 03 2020 at 19:29):

I have this:

section jaccard_numerator
/-- Instantiate finset ℕ as a metric space. -/
instance jaccard_numerator.metric_space (hm : 0 < m) (hM : m ≤ M): metric_space (finset ℕ) := {
-- omitting the details
}
end jaccard_numerator


#### Adam Topaz (Dec 03 2020 at 19:29):

Ah, you have variables....

#### Adam Topaz (Dec 03 2020 at 19:30):

So typeclass inference can't find this instance since it doesn't know how to fill in hm and hM.

#### Eric Wieser (Dec 03 2020 at 19:30):

What is the type of m?

real number

#### Adam Topaz (Dec 03 2020 at 19:30):

You can make this a def, and use @dist_nonneg and put in your definition manually.

#### Eric Wieser (Dec 03 2020 at 19:31):

Or you can create a type alias for finset \N

#### Adam Topaz (Dec 03 2020 at 19:31):

But I think the proofs needed will still be missing.

#### Eric Wieser (Dec 03 2020 at 19:31):

Which folds those proofs into the type

(deleted)

#### Eric Wieser (Dec 03 2020 at 19:33):

That's not what I meant

#### Eric Wieser (Dec 03 2020 at 19:33):

m should be part of the type itself

#### Adam Topaz (Dec 03 2020 at 19:33):

Or like this:

structure foo (m M : ℝ) :=
(α : finset ℕ)
(hm : 0 < m)
(hM : m < M)


#### Eric Wieser (Dec 03 2020 at 19:33):

Otherwise when you do dist x y you have two different ms

#### Eric Wieser (Dec 03 2020 at 19:34):

No point having the proofs as fields there

#### Eric Wieser (Dec 03 2020 at 19:34):

Since they're the same for all foo objects

#### Adam Topaz (Dec 03 2020 at 19:34):

Those are presumably needed in defining the instance.

#### Bjørn Kjos-Hanssen (Dec 03 2020 at 19:34):

Yes, if 0<m fails then it's not a metric space

#### Eric Wieser (Dec 03 2020 at 19:35):

Yeah, but put them before the :=

#### Bjørn Kjos-Hanssen (Dec 03 2020 at 19:35):

or if m \le M fails

#### Adam Topaz (Dec 03 2020 at 19:35):

def foo (m M : ℝ) (hm : 0 < m) (hM : m < M) := finset ℕ


#### Adam Topaz (Dec 03 2020 at 19:36):

Yeah, this should work.

#### Eric Wieser (Dec 03 2020 at 19:36):

Then metric_space (foo n M hm hM)

#### Bjørn Kjos-Hanssen (Dec 03 2020 at 19:37):

Thanks I'll try that... will probably still have some questions

#### Adam Topaz (Dec 03 2020 at 19:37):

def foo {m M : ℝ} (hm : 0 < m) (hM : m < M) := finset ℕ
instance {m M : ℝ} {hm : 0 < m} {hM : m < M} : metric_space (foo hm hM) := sorry


#### Eric Wieser (Dec 03 2020 at 19:39):

Can you combine hm and hM into a statement about docs#Ioo

#### Adam Topaz (Dec 03 2020 at 19:40):

I wish we could write h : 0 < m < M

#### Adam Topaz (Dec 03 2020 at 19:41):

But yes, you can say that $m$ is in the interval $(0,M)$.

#### Adam Topaz (Dec 03 2020 at 19:41):

(even though @Eric Wieser 's link is broken)

#### Yakov Pechersky (Dec 03 2020 at 19:43):

Bjørn Kjos-Hanssen said:

how might I tell dist_nonneg which metric I want to use?

What do you want to use the result of having a proof that jaccard distance is nonnegative for?

#### Bjørn Kjos-Hanssen (Dec 03 2020 at 19:46):

Well it's a numerator of a generalization of Jaccard distance... :) but this numerator I want to use in a proof about the generalization itself, in order to prove eq_of_dist_eq_zero for the latter

#### Yakov Pechersky (Dec 03 2020 at 19:49):

Then you might prefer to use uniform_space_of_dist instead

#### Yakov Pechersky (Dec 03 2020 at 19:51):

And have a helper dist_nonneg to not require a metric_space but just a term of uniform_space

#### Yakov Pechersky (Dec 03 2020 at 19:52):

Because for uniform_space_of_dist you provide the dist explicitly instead of implicitly

#### Yakov Pechersky (Dec 03 2020 at 19:52):

(which I think might be useful for @Lars Ericson as well...?)

#### Bjørn Kjos-Hanssen (Dec 03 2020 at 19:55):

But will that be a weaker result, then? If I just prove it's a uniform_space instead of a metric space?

#### Adam Topaz (Dec 03 2020 at 19:55):

I think @Yakov Pechersky is saying to put the dist as a variable in the lemma.

#### Yakov Pechersky (Dec 03 2020 at 19:56):

You're trying to prove statements about __this__ particular distance function, not spaces that have this distance function, right?

#### Bjørn Kjos-Hanssen (Dec 03 2020 at 19:58):

Right, I'm working with no additional "space" structure beside the distance function... except that the domain is fixed to be finset \N

#### Yakov Pechersky (Dec 03 2020 at 20:04):

There's several ways of getting out the unbundled result from the metric_space bundled structure. Can you share your larger problem statement?

#### Bjørn Kjos-Hanssen (Dec 03 2020 at 20:06):

I can share but maybe I should ask first if you mean something like this:

theorem eq_of_jn_eq_zero (myspace : metric_space (finset ℕ)) (hm: 0 < m)  --- omitting the rest


#### Bjørn Kjos-Hanssen (Dec 03 2020 at 20:07):

and then do someting like myspace.dist_nonneg?

#### Yakov Pechersky (Dec 03 2020 at 20:11):

with a hdist : myspace.dist = jaccard_distance_func could work

#### Bjørn Kjos-Hanssen (Dec 03 2020 at 23:44):

Anyway, I was able to get what was needed by just using @Eric Wieser 's original pointer to dist_nonneg and replicating that proof

Last updated: May 19 2021 at 03:22 UTC