metrics are nonnegative

Stream: Is there code for X?

[Bjørn Kjos-Hanssen]

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]

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

[Bjørn Kjos-Hanssen]

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

[Bjørn Kjos-Hanssen]

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

[Adam Topaz]

Looks like you need an instance of metric_space

[Bjørn Kjos-Hanssen]

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

[Eric Wieser]

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

[Adam Topaz]

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

[Bjørn Kjos-Hanssen]

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]

Ah, you have variables....

[Adam Topaz]

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

[Eric Wieser]

What is the type of m?

[Bjørn Kjos-Hanssen]

real number

[Adam Topaz]

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

[Eric Wieser]

Or you can create a type alias for finset \N

[Adam Topaz]

But I think the proofs needed will still be missing.

[Eric Wieser]

Which folds those proofs into the type

[Adam Topaz]

(deleted)

[Eric Wieser]

That's not what I meant

[Eric Wieser]

m should be part of the type itself

[Adam Topaz]

Or like this:

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

[Eric Wieser]

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

[Eric Wieser]

No point having the proofs as fields there

[Eric Wieser]

Since they're the same for all foo objects

[Adam Topaz]

Those are presumably needed in defining the instance.

[Bjørn Kjos-Hanssen]

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

[Eric Wieser]

Yeah, but put them before the :=

[Bjørn Kjos-Hanssen]

or if m \le M fails

[Adam Topaz]

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

[Adam Topaz]

Yeah, this should work.

[Eric Wieser]

Then metric_space (foo n M hm hM)

[Bjørn Kjos-Hanssen]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Yakov Pechersky]

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]

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]

Then you might prefer to use uniform_space_of_dist instead

[Yakov Pechersky]

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

[Yakov Pechersky]

Because for uniform_space_of_dist you provide the dist explicitly instead of implicitly

[Yakov Pechersky]

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

[Bjørn Kjos-Hanssen]

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

[Adam Topaz]

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

[Yakov Pechersky]

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

[Bjørn Kjos-Hanssen]

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]

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]

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]

and then do someting like myspace.dist_nonneg?

[Yakov Pechersky]

with a hdist : myspace.dist = jaccard_distance_func could work

[Bjørn Kjos-Hanssen]

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