Mathlib.Order.Copy

Stream: mathlib4

[Riccardo Brasca]

I am porting Mathlib.Order.Copy. In mathlib3 there is

def bounded_order.copy {h : has_le α} {h' : has_le α} (c : @bounded_order α h')
  (top : α) (eq_top : top = @bounded_order.top α _ c)
  (bot : α) (eq_bot : bot = @bounded_order.bot α _ c)
  (le_eq : ∀ (x y : α), ((@has_le.le α h) x y) ↔ x ≤ y) :
  @bounded_order α h :=
begin
  refine { top := top, bot := bot, .. },
  all_goals { abstract { subst_vars, casesI c, simp_rw le_eq, assumption } }
end

Let's forget that abstract is not ported, this is not a problem.

First of all @BoundedOrder.top α _ c does not exist, I changed it to (@BoundedOrder.toOrderTop α _ c).top, I don't know if there is a shorter version.

Secondly, if I try something like (that more or less follows the mathlib3 proof)

  refine'
    { top := top,
      bot := bot,
      le_top := sorry,
      bot_le := sorry }

I get the error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  h'
inferred
  h

so it seems Lean4 is not smart enough to understand it is supposed to use h, but Lean3 was. A working proof is

def BoundedOrder.copy {h : LE α} {h' : LE α} (c : @BoundedOrder α h') (t : α)
    (eq_top : top = (@BoundedOrder.toOrderTop α _ c).top) (bot : α)
    (eq_bot : bot = (@BoundedOrder.toOrderBot α _ c).bot)
    (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @BoundedOrder α h :=
  @BoundedOrder.mk α h (@OrderTop.mk α h { top := top } (fun a ↦ by simp [eq_top, le_eq]))
    (@OrderBot.mk α h { bot := bot } (fun a ↦ by simp [eq_bot, le_eq]))

Is there a nicer way?

[Riccardo Brasca]

Something that also works is

def BoundedOrder.copy {h : LE α} {h' : LE α} (c : @BoundedOrder α h') (t : α)
    (eq_top : top = (by infer_instance : Top α).top) (bot : α)
    (eq_bot : bot = (by infer_instance : Bot α).bot)
    (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @BoundedOrder α h

I am a little surprised that infer_instance finds Top α, since c is not in square brackets...

[Kevin Buzzard]

The square bracket thing is just for other functions using your function, it doesn't affect how your function elaborates. If it's before the colon and a typeclass it goes in the instance cache regardless of what brackets you use. This is the same in lean 3 and it surprised me when I discovered it too!

[Riccardo Brasca]

Good to know!

[Eric Wieser]

This has come up repeatedly, https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60.28_.29.60.20vs.20.60_.60.20syntax is related

[Eric Wieser]

As I understand it, It's not Lean4 is not smart enough; it's that it's decided that the spelling you wanted to use isn't allowed any more

[Eric Wieser]

The solution is to use @bounded_order.mk with (_) in place of the typeclass arguments

[Eric Wieser]

That is, you can replace h with (_) in the proof