What's this typeclass?

Stream: maths

[Wrenna Robson]

Let's say I have a type, probably a monoid, and it has a cast/coercion to the reals which is order-preserving, respects addition, and which maps only zero to zero.
What's a short way of describing this?
For example, the relation that the natural embedding of the naturals or the rationals into the reals has this property

[Yaël Dillies]

My guess is variables {F α : Type*} [ordered_add_comm_monoid α] [order_add_monoid_hom_class F α ℝ] (f : F) (hf : function.injective f)

[Jireh Loreaux]

(deleted)

[Jireh Loreaux]

Oh wait, nevermind.

[Riccardo Brasca]

If you want to set up the API for one specific coercion (say it is "canonical" in some sense), then the trick is to use the right norm_cast attributes

[Wrenna Robson]

I'm defining something and I happened to be defining it on nat, but I'm not really using many actual properties of nat.

[Wrenna Robson]

To be honest it might be the case that nat and int and rat and real are the only ones I really care about.

[Wrenna Robson]

(But it would still be nice to have a typeclass that more or less boils down to nat_or_int_or_rat_or_real...)

[Jireh Loreaux]

That would be a weird type class. What do you want it for?

[Wrenna Robson]

I was defining "nat metrics", natural-valued metrics, and I was trying to work out if I could generalise what I was doing

[Jireh Loreaux]

okay, but why would you need that type class you described?

[Kevin Buzzard]

inb4 hamming codes

[Wrenna Robson]

actually for hamming codes nat is sufficient

[Wrenna Robson]

basically I was trying to work out what other types could be said to be "reasonable" codomains for a metric

[Wrenna Robson]

slash dist-variant

[Kevin Buzzard]

Any subset of the nonnegative reals?

[Mario Carneiro]

in that case, it doesn't seem to be much of an advantage to not just say it's nonneg reals

[Jireh Loreaux]

presumably you want it to be closed under addition so you can state the triangle inequality.

[Wrenna Robson]

Yes.

[Wrenna Robson]

@Mario Carneiro there are specific useful properties that you get from being careful about the nat-valued-ness

[Mario Carneiro]

especially if you are saying that this set naturally injects into the reals

[Wrenna Robson]

some of which you can see in https://leanprover-community.github.io/mathlib_docs/information_theory/hamming.html

[Mario Carneiro]

there are other reasonable notions of metric that go beyond the reals but if it's a subset then I don't see the point

[Jireh Loreaux]

I think you can capture this another way. Why don't you just have a structure that extends metric that says the values are all coercions of nats? Then you can prove all the properties you want "from being careful about the nat-valued ones"

[Mario Carneiro]

sure, hamming_dist is a nat, but that's already everything you need to know

[Wrenna Robson]

@Jireh Loreaux that's exactly what I've done

[Mario Carneiro]

the dist you get out of the structure is a real but that's fine since you still have hamming_dist in the restricted case

[Wrenna Robson]

Aye, I have all this.

[Mario Carneiro]

if you want to be generic about it then you don't know it's a nat anymore but rather some subset of the reals and the benefits are lost

[Kevin Buzzard]

Jireh Loreaux said:

presumably you want it to be closed under addition so you can state the triangle inequality.

You don't need it to be closed under addition because you can do the addition in the reals I guess.

[Jireh Loreaux]

Yeah, at the time I thought we were talking about actually ℕ (or whatever) valued dist functions, as opposed to ℝ-valued ones where the range is included in the range of the coercion.

[Wrenna Robson]

Aye, but in a sense you want all the lemmas that only come from the metric axioms "for free". Currently hamming_dist has a bunch of lemmas that duplicate a lot of dist lemmas - that's fine enough, but if someone defined some other natural-valued or rational-valued metric for some other information-theoretic application... you wouldn't want to prove them all again, it would be a waste.

[Mario Carneiro]

you do get them "for free" though, as a result of instantiating the real-valued metric_space using \u (my_dist x y) as the metric

[Wrenna Robson]

@Jireh Loreaux oh to be fair I have implemented it as ℕ-valued dist functions, but I suppose one could do it in other ways.

[Wrenna Robson]

Mario Carneiro said:

you do get them "for free" though, as a result of instantiating the real-valued metric_space using \u (my_dist x y) as the metric

Mmm, but that means reasoning about them can be a pain because you end up doing a lot of coercing around.

[Wrenna Robson]

I think that's why Eric advised me to write the hamming file in the way that I did.

[Mario Carneiro]

is this one of those examples where we are generalizing from one example?

[Wrenna Robson]

Yes.

[Wrenna Robson]

I'm perfectly happy to just stay in my one-example box.

[Mario Carneiro]

please don't

[Wrenna Robson]

But sometimes when I do that people then say "this isn't general enough".

[Mario Carneiro]

I suggest leaving that to the refactor junkies once there are at least 3 examples

[Wrenna Robson]

Yeah it is just annoying when it blocks me from doing stuff.

[Wrenna Robson]

As in, when it jams up PRs.

[Wrenna Robson]

I've found if I don't hit the right level of generality I spend a lot longer on stuff.

[Mario Carneiro]

I think you should try not to write code that is "trivially generalizable", but if generalization makes the code significantly structurally different then it's fine to put it off until the next example shows up to motivate it better

[Mario Carneiro]

a typeclass that generalizes over nat,int,rat coes is what I would call a significant structural refactor of the hamming_dist code

[Wrenna Robson]

Alright.

[Yaël Dillies]

Mario Carneiro said:

I suggest leaving that to the refactor junkies once there are at least 3 examples

Is that me? :rofl: