Zulip Chat Archive

Stream: Is there code for X?

Topic: metrics are nonnegative


view this post on Zulip 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?

view this post on Zulip Eric Wieser (Dec 03 2020 at 18:23):

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

view this post on Zulip Bjørn Kjos-Hanssen (Dec 03 2020 at 18:24):

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

view this post on Zulip Bjørn Kjos-Hanssen (Dec 03 2020 at 19:25):

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

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:27):

Looks like you need an instance of metric_space

view this post on Zulip Bjørn Kjos-Hanssen (Dec 03 2020 at 19:27):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:28):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:29):

Ah, you have variables....

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Dec 03 2020 at 19:30):

What is the type of m?

view this post on Zulip Bjørn Kjos-Hanssen (Dec 03 2020 at 19:30):

real number

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:30):

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

view this post on Zulip Eric Wieser (Dec 03 2020 at 19:31):

Or you can create a type alias for finset \N

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:31):

But I think the proofs needed will still be missing.

view this post on Zulip Eric Wieser (Dec 03 2020 at 19:31):

Which folds those proofs into the type

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:33):

(deleted)

view this post on Zulip Eric Wieser (Dec 03 2020 at 19:33):

That's not what I meant

view this post on Zulip Eric Wieser (Dec 03 2020 at 19:33):

m should be part of the type itself

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:33):

Or like this:

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

view this post on Zulip Eric Wieser (Dec 03 2020 at 19:33):

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

view this post on Zulip Eric Wieser (Dec 03 2020 at 19:34):

No point having the proofs as fields there

view this post on Zulip Eric Wieser (Dec 03 2020 at 19:34):

Since they're the same for all foo objects

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:34):

Those are presumably needed in defining the instance.

view this post on Zulip Bjørn Kjos-Hanssen (Dec 03 2020 at 19:34):

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

view this post on Zulip Eric Wieser (Dec 03 2020 at 19:35):

Yeah, but put them before the :=

view this post on Zulip Bjørn Kjos-Hanssen (Dec 03 2020 at 19:35):

or if m \le M fails

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:35):

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

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:36):

Yeah, this should work.

view this post on Zulip Eric Wieser (Dec 03 2020 at 19:36):

Then metric_space (foo n M hm hM)

view this post on Zulip Bjørn Kjos-Hanssen (Dec 03 2020 at 19:37):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 03 2020 at 19:39):

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

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:40):

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

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:41):

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

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:41):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Dec 03 2020 at 19:49):

Then you might prefer to use uniform_space_of_dist instead

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Dec 03 2020 at 19:52):

Because for uniform_space_of_dist you provide the dist explicitly instead of implicitly

view this post on Zulip Yakov Pechersky (Dec 03 2020 at 19:52):

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

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Dec 03 2020 at 19:55):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Bjørn Kjos-Hanssen (Dec 03 2020 at 20:07):

and then do someting like myspace.dist_nonneg?

view this post on Zulip Yakov Pechersky (Dec 03 2020 at 20:11):

with a hdist : myspace.dist = jaccard_distance_func could work

view this post on Zulip 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