Heterogenous LE?

Stream: Is there code for X?

[Alex Zani]

Is there a heterogenous version of LE? (One that takes elements from two different types)

[Kevin Buzzard]

Such a thing couldn't satisfy any of the usual axioms for LE because they won't typecheck. Are you asking if there's a notation typeclass with type A -> B -> Prop? What exactly are you looking for?

[Kevin Buzzard]

AFAIK the question "docs#Mul is to docs#HMul as docs#LE is to ??" doesn't have an answer in core Lean at least (but all these are are notation typeclasses).

[Alex Zani]

Kevin Buzzard said:

Such a thing couldn't satisfy any of the usual axioms for LE because they won't typecheck. Are you asking if there's a notation typeclass with type A -> B -> Prop? What exactly are you looking for?

Yes, I am looking for a notation typeclass.

Specifically I want to be able to do a <= b where a and b are instances of two different subtypes of the same type.

[Alex Zani]

I guess to avoid the XY problem, I am defining orders (preorders, partial orders, etc) as part of a pedagogical exercise and I've settled on using subtypes to represent suborders. So it would be nice if I could still talk about comparisons of elements of various subsets.

[Yaël Dillies]

Have you considered coercing the elements to the original order before comparing them? Something like

import Mathlib

example {a : {x : Nat // Even x}} {b : {x : Nat // Odd x}} : a.val \le b.val := sorry

[Kyle Miller]

I've wondered about whether arithmetic binary operators and relations should automatically cast subtypes to the base type. This seems to occasionally come up as an issue, right? And if you want to have a subtype with arithmetic operations, you may as well create a custom structure, to avoid accidentally putting the operations globally on Subtype itself.

[Alex Zani]

Kyle Miller said:

I've wondered about whether arithmetic binary operators and relations should automatically cast subtypes to the base type. This seems to occasionally come up as an issue, right? And if you want to have a subtype with arithmetic operations, you may as well create a custom structure, to avoid accidentally putting the operations globally on Subtype itself.

I don't think that works for operators because what's the output type?

[Kyle Miller]

E.g. if you have

variable {a : {x : Nat // Even x}} {b : {x : Nat // Odd x}}
#check a + b

what I'm proposing is that this elaborates to (a.val + b.val : Nat).

[Kyle Miller]

(The broader context is that arithmetic operators/relations have a special elaborator that computes a type that everything coerces to, then inserts coercions where necessary. I tweak this elaborator every once in a while, and this is something I've had in the back of my head, since I only ever see subtypes cause problems for it.)

[Weiyi Wang]

I personally find implicit coercion of subtypes already confusing sometimes. I don't think I would like it if we add another special elaborator rule. I would need to constantly check InfoView to ensure it goes to the right type I expect

[Kyle Miller]

For arithmetic though, do you ever expect it to stay in the Subtype @Weiyi Wang? Right now arithmetic sometimes triggers the coercion but not always, and having a clean rule that it will always coerce seems easier to reason about. The observation here is that it's questionable adding any arithmetic typeclass instances to Subtype.

[Alex Zani]

I think I would sometimes want to stay in the subtype. As long as I can override the behavior so I can stay in N/2 for instance, that's fine.

[Weiyi Wang]

Hmm, I don't know. How does this behave if I have a b : s where s : Subgroup G? I think I want a * b to stay in the subgroup. Does s count as a subtype?

[Kyle Miller]

Somehow I thought the Subgroup coercion used a custom type rather than giving Subtype itself a Mul instance. I think there's some talk elsewhere about making SetLike coercions use a custom type, but in any case Subgroup kills the idea for now.

[Yury G. Kudryashov]

In the other thread, @Eric Wieser suggests that we block simp's unwanted behavior by using simprocs instead of introducing a new type.

[Yury G. Kudryashov]

#mathlib4 > Coercion of SetLike to Type*

[Alex Zani]

Kyle Miller said:

Somehow I thought the Subgroup coercion used a custom type rather than giving Subtype itself a Mul instance. I think there's some talk elsewhere about making SetLike coercions use a custom type, but in any case Subgroup kills the idea for now.

Should I be using Set or SetLike as the basis for my orders then?