Mathlib.Order.ConditionallyCompleteLattice.Basic

Stream: mathlib4

[Riccardo Brasca]

In Mathlib.Order.ConditionallyCompleteLattice.Basic there is

class ConditionallyCompleteLinearOrder (α : Type _) extends ConditionallyCompleteLattice α,
  "./././Mathport/Syntax/Translate/Command.lean:407:11: unsupported: advanced extends in structure"

where the mathlib3 class is

class conditionally_complete_linear_order (α : Type*)
  extends conditionally_complete_lattice α, linear_order α renaming max → sup min → inf

I guess the issue is with renaming, but I don't know. How are we supposed to write this in Lean4?

[Eric Wieser]

did we rename the fields in docs4#LinearOrder?

[Adam Topaz]

docs4#LinearOrder

[Eric Wieser]

No, we didn't

[Eric Wieser]

The solution here is to pick one class to extend, and copy across the fields (except sup/max and min/inf) for the other

[Eric Wieser]

And then add an instance manually that sets min := inf or vice versa

[Adam Topaz]

There is some renaming infrastructure here, but I don't know ow enough about this to say whether it applies here
https://github.com/leanprover-community/mathlib4/blob/ddf4802e9a3a09b881d512b5a9bc7276920da7aa/Mathlib/Tactic/Simps/Basic.lean

[Eric Wieser]

I don't think that's relevant here. The renaming keyword in Lean 3 was a mechanism to automatically do pretty much exactly the manual process I described above

[Adam Topaz]

Yeah it seems that stuff is just for simps

[Eric Wieser]

I suppose it would be reasonable to file a feature request against Lean for

structure Foo where
  x : Nat

structure Bar where
  y : Nat

structure Baz extends Foo, Bar renaming Foo.x Bar.y -> z

which would generate code similar to

structure Foo where
  x : Nat

structure Bar where
  y : Nat

structure Baz where
  z : Nat

def Baz.toFoo (self : Baz) : Foo := { x := self.z }
def Baz.toBar (self : Baz) : Bar := { y := self.z }

[Riccardo Brasca]

There is still one thing I don't understand. I am writing

class ConditionallyCompleteLinearOrder (α : Type _) extends ConditionallyCompleteLattice α where
  le_total (a b : α) : a ≤ b ∨ b ≤ a
  decidable_le : DecidableRel (. ≤ . : α → α → Prop)
  decidable_eq : DecidableEq α := @decidableEq_of_decidableLE _ _ decidable_le
  decidable_lt : DecidableRel (. < . : α → α → Prop) :=
    @decidableLT_of_decidableLE _ _ decidable_le

(these are the fields of linear_order that don't mention min/max). Then we want

instance (α : Type _) [ConditionallyCompleteLinearOrder α] : LinearOrder α :=
{ ‹ConditionallyCompleteLinearOrder α› with
  max := HasSup.sup, min := HasInf.inf, min_def := sorry, max_def := sorry }

I know how to fill the sorry, but I don't understand what happens in mathlib3: there is no sign of the proof, so I think renaming is adding them explicitly to the definition of ConditionallyCompleteLinearOrder even if they're automatic in this particular situation? In this case are they spelled using inf/sup?

[Eric Wieser]

In mathlib3 the proof is provided with an autoparam

[Eric Wieser]

either src#conditionally_complete_linear_order or src#linear_order should contain the answer

[Eric Wieser]

Yeah, here

[Eric Wieser]

The autoparam in Lean4 is different and evidently less powerful

[Eric Wieser]

Oh, the actual answer is that in Mathlib3 , the min_def and max_def fields remain there, but restarted with sup/inf

[Eric Wieser]

Which is usually good enough, because you usually already have a linear_order instance lying around that you can populate them with

[Riccardo Brasca]

OK, that's reasonable, since I think it's just a coincidence that here they're automatic.

[Riccardo Brasca]

What's the best approach here? Adding them even if they're automatic or prove them in the instance?

[Eric Wieser]

Prove them in the instance to match mathlib3

[Eric Wieser]

The downside is that you won't be able to use foo.linearOrder with because the with keyword doesn't know about the renames