type synonym trickery not working

Stream: mathlib4

[Heather Macbeth]

In mathlib4#773, there is a porting failure on a lemma deduced for has_inf via the corresponding lemma for has_sup, invoked on the order_dual of the original order. This kind of proof is ubiquitous in the order theory files, so it would be good to find a fix.

Here is a version without imports:

variable (α : Type _)

/-! ### Notation classes for `⊔`, `⊓` -/

class HasSup where
  sup : α → α → α

class HasInf where
  inf : α → α → α

infixl:68 " ⊔ " => HasSup.sup
infixl:69 " ⊓ " => HasInf.inf

/-! ### `OrderDual` and instances -/

def OrderDual : Type _ := α

instance [LE α] : LE (OrderDual α) := ⟨fun x y : α => y ≤ x⟩
instance [HasInf α] : HasSup (OrderDual α) := ⟨((· ⊓ ·) : α → α → α)⟩

/-! ### Example -/

theorem foo [LE α] [HasSup α] {a b c : α} (h : a ≤ b ⊔ c) : a ≤ b := sorry

example [LE α] [HasInf α] {a b c : α} (h : a ⊓ b ≤ c) : a ≤ c :=
  @foo (OrderDual α) _ _ _ a _ h
  -- in lean 3 you don't need the argument `a`, i.e. this works:
  -- @foo (OrderDual α) _ _ _ _ _ h

edit: minimized more

[Heather Macbeth]

The proof @foo (OrderDual α) _ _ _ a _ h I have provided here would have worked without the argument a in Lean 3. That is, in Lean 3 this works:

@foo (OrderDual α) _ _ _ _ _ h

Interestingly, in Lean 3 the following does not work:

foo (OrderDual α) h

so maybe the @ in Lean 3 was causing a change in elaboration order which happened to be convenient for this kind of thing?

[Mario Carneiro]

This sounds like https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/logic.2Eequiv.2Ebasic.20mathlib4.23631/near/311746932

[Heather Macbeth]

Gabriel's fix there was to insert a by exact, but that doesn't seem to work here.

[Scott Morrison]

I think Gabriel's fix in that thread was actually to a different problem. The #mwe that Mario linked to needs a fix in Lean 4 core, as far as I understand, but it hasn't been reported yet.

[Scott Morrison]

Ah, Mario has just reported it! https://github.com/leanprover/lean4/issues/1891

[Heather Macbeth]

Thanks for explaining! I confess I can't tell the relevance of that issue to this one. However, if Mario and Scott now have it in hand, I'm very happy to leave it to you.

[Scott Morrison]

I added a link to your PR to Mario's issue, and we can revisit when it is solved. It doesn't need to hold up this PR.

[Mario Carneiro]

I take it back, on review that's a different issue. I will poke at this one and report it separately

[Mario Carneiro]

The (e :) trick works here

[Mario Carneiro]

example [LE α] [HasInf α] {a b c : α} (h : a ⊓ b ≤ c) : a ≤ c :=
  (foo (α := OrderDual α) h :)

[Heather Macbeth]

Huh! Was there a previous discussion of this trick which you can point me to?

[Mario Carneiro]

this is the lean 4 version of the (e : _) trick from lean 3

[Mario Carneiro]

what it does is hide the expected type while elaborating the subterm, similar to by have := e; exact e

[Heather Macbeth]

I see, thanks. So indeed it was a change in elaboration order. Are we assuming this is a feature, not a bug, from the point of view of the Lean 4 developers?

[Heather Macbeth]

i.e. the side effect of some other useful change?

[Mario Carneiro]

hard to say... hopefully Leo will be able to shed some light on this in lean4#1892

[Mario Carneiro]

I don't think it's about elaboration order per se, but rather there is a missed backtracking opportunity where we tried some solution but it turns out to be wrong and instead of unfolding some stuff and trying again it just gives an error

[Heather Macbeth]

Thanks for finding the further minimization and opening the issue. Is it relevant to mention on your issue that the following variant works in Lean 3 but not Lean 4?

example : a ≤ b := @foo (OrderDual α) _ _ _

[Heather Macbeth]

Actually, even this seems to work in Lean 3:

example : a ≤ b := foo (OrderDual α)