Subtype coercion leads to error with multiplication

Stream: lean4

[Markus Schmaus]

The following short example leads to an error in #eval:

def two : Subtype fun x : Nat => x = 2 := ⟨2, rfl⟩
def three : Subtype fun x : Nat => x = 3 := ⟨3, rfl⟩

#eval two * three

I would have hoped that two and three would get coerced to Nat and the result would be (6 : Nat). I get that HMul cannot infer the return type and the default instance instHMul doesn't trigger since two and three have different type.

Is there a way to fix this without explicit casting (or .val)? Or is this desired behavior?

[Scott Morrison]

Yes, I think you have an unreasonable hope here. :-)

[Markus Schmaus]

What makes this hope unreasonable?

[Damiano Testa]

You could also hope for an autogenerated

def six : Subtype fun x : Nat => x = 6 := ⟨6, rfl⟩

as a result. :six:

[Damiano Testa]

Btw, you may like this:

import Mathlib.Data.Set.Pointwise.Basic

open Pointwise

example : ({2} * {3} : Set ℕ) = {6} := by simp

[Scott Morrison]

There's nothing you wrote in your code that indicates you want an answer in Nat.

Note that both of the following work:

def two : Subtype fun x : Nat => x = 2 := ⟨2, rfl⟩
def three : Subtype fun x : Nat => x = 3 := ⟨3, rfl⟩

#check (two * three : Nat)
#check (two * three : Int)

[Scott Morrison]

How should Lean know which one you were hoping for?

[Markus Schmaus]

The same is true for 2 * 3 and yet Lean makes the reasonable choice of returning (6 : Nat). I think it would also be reasonable for Lean to eagerly fall back to to underlying type for any Subtype. I wonder if there is a way to make it do so.

[James Gallicchio]

On the other hand, I'm sorta starting to wonder if Nat as the default OfNat might cause more confusion than clarity. For example here the reason it returns Nat in 2 * 3 is that the OfNat instance defaults to Nat, which has nothing to do with *.

[Kyle Miller]

Scott Morrison said:

Yes, I think you have an unreasonable hope here. :-)

I'm not so sure it's unreasonable -- the binop% elaborator could know about Subtype. It could make the assumption that Subtypes never have HMul instances, and so a Subtype argument must be coerced to its underlying type.

[Kyle Miller]

If people do actually add arithmetic operator instances to Subtypes directly (rather than onto a semireducible type synonym), then this is a bad idea.

[Johan Commelin]

Is NNReal a subtype? I think it used to be at some point

[Johan Commelin]

PNat is a subtype.

[Kyle Miller]

Those are type synonyms though -- the instances are being put on NNReal and PNat, rather than on Subtype itself.

[Johan Commelin]

Ooh, ok... I probably misunderstood the reducibility constraints.

[Kyle Miller]

Yeah, I meant to just distinguish a def ... := Subtype ... from an abbrev ... := Subtype ...

[Johan Commelin]

/-!
# The type of nonnegative elements

This file defines instances and prove some properties about the nonnegative elements
`{x : α // 0 ≤ x}` of an arbitrary type `α`.

Currently we only state instances and states some `simp`/`norm_cast` lemmas.

When `α` is `ℝ`, this will give us some properties about `ℝ≥0`.

## Main declarations

* `{x : α // 0 ≤ x}` is a `CanonicallyLinearOrderedAddCommMonoid` if `α` is a `LinearOrderedRing`.

[Johan Commelin]

Output of head -27 Mathlib/Algebra/Order/Nonneg/Ring.lean | tail -14

[Kyle Miller]

Ah, thanks for finding that. Back to the drawing board.

[Johan Commelin]

We could decide that this should also be wrapped behind an honest definition

[Eric Wieser]

Kyle Miller said:

If people do actually add arithmetic operator instances to Subtypes directly (rather than onto a semireducible type synonym), then this is a bad idea.

This is literally the API for every subobject

[Eric Wieser]

docs#Submonoid.toMonoid

[Kyle Miller]

Oh, right -- that's new to Lean 4 though, right? I mean, before in Lean 3 a submonoid as a monoid had a type wrapped up in a coe function, but now the coercions are unfolded. I don't remember, was that coe function reducible for typeclass inference purposes? If not, could we go back to wrapping these subobject -> object coercions in some function to prevent putting instances on Subtype directly?

[Eric Wieser]

I don't remember, was that coe function reducible for typeclass inference purposes?

No, but what mattered is that the it was the same coe_sort function symbol everywhere. I think we could introduced a SetLike.Elem class to use for every subobject if we wanted (or reuse Set.Elem), but that feels like it's pushing back even further against Lean4 deciding to inline coercions

[Mario Carneiro]

I discussed exactly this issue with @Patrick Massot a few weeks ago, my diagnosis was that it was a mistake to use {x // x \in s} directly in the Coe instance and it should instead be wrapped by a @[coe] def toSort function so that you still get the arrow shown by the delaborator