Type synonyms

Stream: mathlib4

[Heather Macbeth]

In mathlib4#903, a whole bunch of proofs involving type synonyms (Additive, Multiplicative, OrderDual) are just completely broken. I've fixed them with a bunch of @, but it seems like this really should be debugged; we'll hit it again. Does anyone have time to look at this?

Here's the commit adding a bunch of @, so look at the branch in its state before this.

[Kevin Buzzard]

Is this the same as https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/What.20type.20annotation.20can.20do/near/314660799 ?

[Heather Macbeth]

I think probably not, but it's possible.

[Heather Macbeth]

There were no type synonyms in that one.

[Heather Macbeth]

Interestingly, in the issue here, all the cases are actually a type synonym of a type synonym! Like Multiplicative αᵒᵈ.

[Eric Wieser]

zero := Multiplicative.ofAdd (⊤ : α) should probably be zero := Multiplicative.ofAdd $ toDual (⊤ : α)

[Eric Wieser]

But maybe toDual is not imported yet there

[Yaël Dillies]

If it's not, make it be. It's part of the basic API.

[Eric Wieser]

Sure, but it might be too late if half the order stuff is already ported to mathlib4

[Heather Macbeth]

To check, you're saying that Lean 3 was cleverer, and you could sometimes omit the boilerplate toDual/ofDual; Lean 4 requires this all be there explicitly?

[Eric Wieser]

I'm saying that the code you're porting is somewhat sloppy, and it's possible that writing it in a less sloppy way would be less confusing to Lean 4. It's also entirely possible that my suggestion makes no difference

[Eric Wieser]

I think the @s there are probably ok.

[Eric Wieser]

I'm curious; does @top_add _ (_) work instead of @top_add α _?

[Yaël Dillies]

I would much prefer toDual over the @. It's less sloppy, as you said.

[Yaël Dillies]

Eric Wieser said:

Sure, but it might be too late if half the order stuff is already ported to mathlib4

Not sure what you mean. It's a matter of adding one import.

[Heather Macbeth]

In any case, this doesn't seem to be the issue. Before:

instance [LinearOrderedAddCommMonoidWithTop α] :
    LinearOrderedCommMonoidWithZero (Multiplicative αᵒᵈ) :=
  { Multiplicative.orderedCommMonoid, Multiplicative.linearOrder with
    zero := Multiplicative.ofAdd (⊤ : α)
    zero_mul := top_add -- failed to synthesize instance LinearOrderedAddCommMonoidWithTop (Multiplicative αᵒᵈ)
    <snip> }

After:

instance [LinearOrderedAddCommMonoidWithTop α] :
    LinearOrderedCommMonoidWithZero (Multiplicative αᵒᵈ) :=
  { Multiplicative.orderedCommMonoid, Multiplicative.linearOrder with
    zero := Multiplicative.ofAdd (OrderDual.toDual (⊤ : α))
    zero_mul := top_add -- failed to synthesize instance LinearOrderedAddCommMonoidWithTop (Multiplicative αᵒᵈ)
    <snip> }

[Eric Wieser]

Eric Wieser said:

I'm curious; does @top_add _ (_) work instead of @top_add α _?

How about this suggestion? GitPod is taking a while to build up to WithZero for me

[Heather Macbeth]

Interesting. Yes, that one works. Still worse than Lean 3's simple top_add, of course.

[Eric Wieser]

Then it sounds like this is https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60.28_.29.60.20vs.20.60_.60.20syntax/near/313936557 again

[Heather Macbeth]

Then it seems my comment there was prescient!

Heather Macbeth said:

This might be painful for e.g. OrderDual, MulOpposite.

[Eric Wieser]

I think probably for now we should use the @top_add _ (_) spelling instead of @top_add α _, since that flags that lean4 already knows how to work out all the arguments and it's just being stubborn

[Heather Macbeth]

OK, that seems like a good reason. I'll make the change throughout.

[Heather Macbeth]

Hmm, there are two places in the file where α _ works and _ (_) doesn't. I've pushed the rest of the changes so maybe someone can take a look.

[Eric Wieser]

Can you link to the line where that happened?

[Heather Macbeth]

The only two α _ in the file, one sec ...

[Heather Macbeth]

https://github.com/leanprover-community/mathlib4/blob/cf027a53e0dbd91e30c0361451d0502160f8ea66/Mathlib/Algebra/Order/WithZero.lean#L114
https://github.com/leanprover-community/mathlib4/blob/cf027a53e0dbd91e30c0361451d0502160f8ea66/Mathlib/Algebra/Order/WithZero.lean#L292

[Eric Wieser]

In mathlib3 we also had a different spelling there

[Eric Wieser]

https://github.com/leanprover-community/mathlib/blob/master/src/algebra/order/with_zero.lean#L109

[Heather Macbeth]

Ah, you're right, I introduced both of these during my @-fest.

[Heather Macbeth]

They were also both broken, and also fixable by @, but the error is presumably different.

[Heather Macbeth]

The first one: mathport fun a ↦ (zero_mul a : (0 : α) * a = 0), error

failed to synthesize instance HMul α (Additive αᵒᵈ) ?m.26677

valid replacement is

@zero_mul α _

[Heather Macbeth]

The second: mathport fun a ha ↦ mul_inv_cancel ha, error

type mismatch
  mul_inv_cancel ?m.71933
has type
  @Eq ?m.71275 (?m.71277 * ?m.71277⁻¹) 1 : Prop
but is expected to have type
  @Eq (Additive αᵒᵈ) (a + -a) 0 : Prop

fixed by

@mul_inv_cancel α _

[Eric Wieser]

fun a ↦ zero_mul (Additive.to_mul a) is the less hacky proof of the first one

[Eric Wieser]

(a.to_mul is also not allowed in Lean4 which is a separate problem)

[Heather Macbeth]

Indeed. But the analogue doesn't work for the second!

[Eric Wieser]

fun a ha ↦ mul_inv_cancel (id ha : Additive.toMul a ≠ 0) works for the second

[Heather Macbeth]

Can you confirm that you recommend these versions over the @mul_inv_cancel α _ versions? Again because of

Eric Wieser said:

since that flags that lean4 already knows how to work out all the arguments and it's just being stubborn

? If so I'll make those changes.

[Jireh Loreaux]

Heather, does a different type annotation work for zero_mul? Like 0 * (a : α) = 0 or (0 * a : α) = 0 or (0 : α) * (a : α) = 0?

[Jireh Loreaux]

It seems that Lean is getting confused because * is now actually heterogeneous and it is failing to unify the types appropriately during elaboration.

[Heather Macbeth]

Even putting a type annotation on everything doesn't work:

(zero_mul (a : α) : (0 : α) * (a : α) = (0 : α))

[Sebastian Ullrich]

If a is of a type defeq to α, then the type annotation is a no-op. You would have to use the id trick. Coes between defeq types generally seem like a problematic idea, it would be better to make Additive a structure. But I assume that is not desired in other contexts.

[Eric Wieser]

Can you confirm that you recommend these versions over the @mul_inv_cancel α _ versions?

The @ versions are what Kevin would call "defeq abuse", but they're what we used in mathlib3 so :shrug:. Either spelling is fine

[Eric Wieser]

@Sebastian Ullrich, the goal is not to make a coercion happen, but to force zero_mul to elaborate with the annotated type with no information of the expected type at that point in the expression

[Jireh Loreaux]

Actually Eric, I think Lean knows the expected type here. That's why it's getting it wrong. We are trying to force it to instead use a defeq type, which is why it can be considered defeq abuse.

[Eric Wieser]

We're trying to locally change the expected type

[Eric Wieser]

In Lean3, we could say to Lean "I know you want type B, but I'm going to write (foo : A) and you're going to forget that we're actually trying to produce a B until you're completely done with foo". In Lean 4 some of the elaboration seems to be postponed until we're looking at a goal of B again

[Heather Macbeth]

Here's something that does work in place of fun a ha ↦ mul_inv_cancel ha:

fun a ha ↦ ((id (mul_inv_cancel ha) : _ = (1:α)) : _)

[Heather Macbeth]

Also

fun a ha ↦ (mul_inv_cancel (id ha : _ ≠ (0:α)) : _)

Edit: I guess these are cheating because I provide α explicitly and we're trying to avoid that hint.

[Mario Carneiro]

The (e :) elaborator has a special hack to deal with this postponement issue

[Heather Macbeth]

Yes, that's why it occurred to me that this might work.

[Mario Carneiro]

Let me make a version of (e : ty) that forces no postponing...

[Mario Carneiro]

import Lean
open Lean Elab Term
elab "(" e:term ":!" ty:term ")" : term => do
  let ty ← elabType ty
  withSynthesize (mayPostpone := false) <| elabTerm e ty

No one posted an MWE though so I don't have a good test case

[Sebastian Ullrich]

Note that this is missing the coercion insertion code from the standard type annotations. Actually I'm wondering whether that should really be done when expected and given type are non-defeq at reducible level since that is the level coercion resolution works on. Then (a : α) would have generated a coercion and affected resolution at *.

[Sebastian Ullrich]

What exactly is the postponement issue? The expected type shouldn't just get lost during postponement.

[Heather Macbeth]

I'll work on minimizing, but here's a version with imports:

import Mathlib.Algebra.GroupWithZero.Basic
import Mathlib.Algebra.Order.Monoid.WithZero.Defs
import Mathlib.Algebra.Order.Group.Instances
import Mathlib.Algebra.Order.Monoid.TypeTags


class LinearOrderedCommGroupWithZero (α : Type _) extends LinearOrderedCommMonoidWithZero α,
  CommGroupWithZero α

variable [LinearOrderedCommMonoidWithZero α]

instance : LinearOrderedAddCommMonoidWithTop (Additive αᵒᵈ) :=
  { Additive.orderedAddCommMonoid, Additive.linearOrder with
    top := (0 : α)
    top_add' := fun a => zero_mul a -- failed to synthesize instance MulZeroClass (Additive αᵒᵈ)
    le_top := sorry }

It works with fun a => zero_mul (Additive.toMul a).

[Heather Macbeth]

reduced a little more (edit: and more):

import Mathlib.Algebra.GroupWithZero.Defs
import Mathlib.Algebra.Group.TypeTags
import Mathlib.Algebra.Order.Monoid.Defs
import Mathlib.Order.Synonym


instance [h : LE α] : LE (Additive α) := h
instance [h : LT α] : LT (Additive α) := h
instance Additive.partialOrder [h : PartialOrder α] : PartialOrder (Additive α) := h
instance Additive.linearOrder [h : LinearOrder α] : LinearOrder (Additive α) := h

instance Additive.orderedAddCommMonoid [OrderedCommMonoid α] :
    OrderedAddCommMonoid (Additive α) :=
  { Additive.partialOrder, Additive.addCommMonoid with
    add_le_add_left := sorry }


instance [h : Mul α] : Mul αᵒᵈ := h
instance [h : Zero α] : Zero αᵒᵈ := h
instance [h : MulZeroClass α] : MulZeroClass αᵒᵈ := h
instance inst [h : CommMonoid α] : CommMonoid αᵒᵈ := h

instance [LinearOrderedCommMonoid α] : LinearOrderedCommMonoid αᵒᵈ :=
  { OrderDual.instLinearOrderOrderDual α, inst with
    mul_le_mul_left := sorry }

class LinearOrderedCommMonoidWithZero (α : Type) extends LinearOrderedCommMonoid α,
  CommMonoidWithZero α

variable [LinearOrderedCommMonoidWithZero α]

instance : LinearOrderedAddCommMonoidWithTop (Additive αᵒᵈ) :=
  { Additive.orderedAddCommMonoid, Additive.linearOrder with
    top := (0 : α)
    top_add' := fun a => zero_mul (Additive.toMul a)
    le_top := sorry }

[Heather Macbeth]

@Mario Carneiro I think the following should be a MWE for this issue. Can you test it with your proposed no-postponing feature?

class Bot (α : Type) where bot : α
class Top (α : Type) where top : α

notation "⊥" => Bot.bot
notation "⊤" => Top.top

class MulBotClass (α : Type) extends Mul α, Bot α where
  bot_mul : ∀ a : α, ⊥ * a = ⊥

export MulBotClass (bot_mul)

class AddTopClass (α : Type _) extends Add α, Top α where
  top_add : ∀ x : α, ⊤ + x = ⊤

/-- a type synonym -/
def Additive (α : Type) := α

/-- identification with type synonym -/
def Additive.toMul : Additive α → α := id

instance Additive.add [Mul α] : Add (Additive α) := ⟨@Mul.mul α _⟩

instance [MulBotClass α] : AddTopClass (Additive α) :=
  { Additive.add with
    top := (⊥ : α)
    top_add := fun a => bot_mul a } -- failed to synthesize instance MulBotClass (Additive α)

instance [MulBotClass α] : AddTopClass (Additive α) :=
  { Additive.add with
    top := (⊥ : α)
    top_add := fun a => bot_mul (Additive.toMul a) } -- works

[Kevin Buzzard]

It's a bit weird that top := (⊥ : α) works!

top_add := fun a => (id (id (bot_mul (id (a : α))) : (id (⊥ : α)) * (id (a : α)) = (id (⊥ : α)))) } -- failed to synthesize instance MulBotClass (Additive α)

Somehow in Lean 4 you're committed to type Additive α by the time Lean is trying to unify the _ in fun a => _, and no amount of tricks will persuade Lean that a has another type.

[Kevin Buzzard]

    top_add := fun (a : α) => bot_mul a } -- works!

But I don't think that this will solve the general problem.

[Heather Macbeth]

In any case, I oversimplified a bit: the example I posted is susceptible to the @bot_mul _ (_) trick. I think the following should be a real example.

class Bot (α : Type) where bot : α
class Top (α : Type) where top : α

notation "⊥" => Bot.bot
notation "⊤" => Top.top

class MulBotClass (α : Type) extends Mul α, Bot α where
  bot_mul : ∀ a : α, ⊥ * a = ⊥

export MulBotClass (bot_mul)

class Mul₂ (α : Type) extends Mul α

class MulBotClass₂ (α : Type) extends Mul₂ α, MulBotClass α

class AddTopClass₂ (α : Type) extends Add α, Top α where
  top_add : ∀ x : α, ⊤ + x = ⊤

/-- a type synonym -/
def Additive (α : Type) := α

/-- identification with type synonym -/
def Additive.toMul : Additive α → α := id

instance [MulBotClass₂ α] : AddTopClass₂ (Additive α) :=
  { add := @Mul.mul α _
    top := (⊥ : α)
    top_add := bot_mul } -- type mismatch

instance [MulBotClass₂ α] : AddTopClass₂ (Additive α) :=
  { add := @Mul.mul α _
    top := (⊥ : α)
    top_add := @bot_mul _ (_) } -- type mismatch

instance [MulBotClass₂ α] : AddTopClass₂ (Additive α) :=
  { add := @Mul.mul α _
    top := (⊥ : α)
    top_add := fun a => bot_mul a } -- failed to synthesize instance

instance [MulBotClass₂ α] : AddTopClass₂ (Additive α) :=
  { add := @Mul.mul α _
    top := (⊥ : α)
    top_add := fun a => bot_mul (Additive.toMul a) }

[Kevin Buzzard]

Again

    top_add := fun (a : α) => bot_mul a }

also works

[Heather Macbeth]

Here is something specifically that worked in Lean 3 and doesn't work in Lean 4. In Lean 3, translating my example using old_structure_cmd, the following works:

top_add := λ a, (bot_mul a : (⊥ : α) * a = ⊥)

In Lean 4,

top_add := fun a => (bot_mul a : (⊥ : α) * a = ⊥)

fails with two errors,

failed to synthesize instance MulBotClass (Additive α)
failed to synthesize instance HMul α (Additive α) ?m.13158

[Heather Macbeth]

This reminds me of another example I posted. In both cases, in Lean 3 we helped Lean in a tricky situation by providing a type annotation, and that particular type annotation is no longer helpful in Lean 4.

[Heather Macbeth]

And here is a second import-free example, mimicking one of the other errors in the same file.

class Bot (α : Type) where bot : α
class Top (α : Type) where top : α

notation "⊥" => Bot.bot
notation "⊤" => Top.top

class MulBotClass (α : Type) extends Mul α,  Bot α

theorem mul_inv_cancel [MulBotClass α] (a : α) (ha : a ≠ ⊥) : ∃ b : α, a * b = ⊥ := sorry

class Mul₂ (α : Type) extends Mul α

class MulBotClass₂ (α : Type) extends Mul₂ α, MulBotClass α

class AddTopClass₂ (α : Type) extends Add α, Top α where
  add_neg_cancel : ∀ a : α, a ≠ ⊤ → ∃ b, a + b = ⊤

/-- a type synonym -/
def Additive (α : Type) := α

/-- identification with type synonym -/
def Additive.toMul : Additive α → α := id

instance [MulBotClass₂ α] : AddTopClass₂ (Additive α) :=
  { add := @Mul.mul α _
    top := (⊥ : α)
    add_neg_cancel := mul_inv_cancel } -- type mismatch

instance [MulBotClass₂ α] : AddTopClass₂ (Additive α) :=
  { add := @Mul.mul α _
    top := (⊥ : α)
    add_neg_cancel := @mul_inv_cancel _ (_) } -- type mismatch

instance [MulBotClass₂ α] : AddTopClass₂ (Additive α) :=
  { add := @Mul.mul α _
    top := (⊥ : α)
    add_neg_cancel := fun a ha => mul_inv_cancel _ (id ha : Additive.toMul a ≠ ⊥) } -- works

[Heather Macbeth]

The working proof

add_neg_cancel := fun a ha => mul_inv_cancel _ (id ha : Additive.toMul a ≠ ⊥)

at the end was suggested by Eric above. But in Lean 3,

add_neg_cancel := mul_inv_cancel

works!

[Kevin Buzzard]

    add_neg_cancel := @mul_inv_cancel α _ } -- works

but I agree it's not as good as the Lean 3 version!

[Eric Wieser]

I think it's worth remember that a lot of these spellings which work in Lean3 are things that are golfed to oblivion because no-one cares about them being readable or easy for the compiler. It's annoying to have to fix them in the port, but I don't think it's any great loss to lean4 for not supporting the type of nonsense we've historically written for these proofs

[Eric Wieser]

At the extreme, this probably means that in many places where we currently write @some_lemma (order_dual X) _ _ _ we'd be forced to write something more like fun x => some_lemma (to_dual x) etc.

[Yakov Pechersky]

I think that more reliance on "transfer" across homs could reduce boilerplate even more, instead of having to give these mirage-proofs

[Yaël Dillies]

My dream is still for a to_additive-like tactic to handle them all.

[Yaël Dillies]

All this defeq abuse is doing could be done by a script working on the proof term from the original proof.

[Eric Wieser]

Note there are some cases where the type alias is under an internal binder where it really is useful that the types are defeq; I think these come up in some quotient things that probably haven't been reached by the port yet

[Yaël Dillies]

Yes, it will be really hard to hygienise all type synonyms if we don't have automation to do so. Given the pain we've seen in this stream over type synonyms these past weeks, I foresee that we'll be forced to write the automation sooner than later.

[Heather Macbeth]

I'm still curious to see whether @Mario Carneiro's proposed new Lean feature would solve these.

[Heather Macbeth]

Eric Wieser said:

At the extreme, this probably means that in many places where we currently write @some_lemma (order_dual X) _ _ _ we'd be forced to write something more like fun x => some_lemma (to_dual x) etc.

This gets awkward when all the x : X in some_lemma are implicit (because there are hypotheses involving them which are explicit). That was the case here.

[Mario Carneiro]

It's not a proposed new feature, it's a simple macro which was given

[Mario Carneiro]

I am not exactly sure where to slot it into the example from your last ping

[Mario Carneiro]

but this works:

instance [MulBotClass α] : AddTopClass (Additive α) :=
  { Additive.add with
    top := (⊥ : α)
    top_add := fun a => bot_mul (α := α) a }

[Mario Carneiro]

bot_mul (by exact a : α) also works

[Mario Carneiro]

bot_mul (a :! α) does not work, since it seems the postponing is being done from outside the scope of the :!

[Heather Macbeth]

It's certainly nice that Lean 4 provides this other spelling bot_mul (α := α) of @bot_mul α _. That was actually how I was originally solving these failures, but Eric pointed out that with this spelling, in some cases we are giving more help to Lean 4 (the α) than it needed in Lean 3. My second import-free example was one of these cases, and I think we still haven't found a Lean 4 proof there that doesn't contain the hint about α or at least about passing between a type and its additivization.

My first import-free example, the one you were looking at here, was solved in Lean 3 with an elaborate type annotation,

top_add := λ a, (bot_mul a : (⊥ : α) * a = ⊥)

It's certainly not necessary that we get this ugly proof working in Lean 4; bot_mul (α := α) is strictly nicer in my opinion. But I would have thought that this was exactly the use case of your :! macro and it's surprising to me that it doesn't work here.