Zulip Chat Archive

Stream: mathlib4

Topic: Mathlib.Order.ConditionallyCompleteLattice.Basic


Riccardo Brasca (Dec 23 2022 at 14:19):

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 (Dec 23 2022 at 14:51):

did we rename the fields in docs4#LinearOrder?

Adam Topaz (Dec 23 2022 at 14:51):

docs4#LinearOrder

Eric Wieser (Dec 23 2022 at 14:51):

No, we didn't

Eric Wieser (Dec 23 2022 at 14:52):

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 (Dec 23 2022 at 14:53):

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

Adam Topaz (Dec 23 2022 at 14:54):

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 (Dec 23 2022 at 14:59):

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 (Dec 23 2022 at 14:59):

Yeah it seems that stuff is just for simps

Eric Wieser (Dec 23 2022 at 15:02):

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 (Dec 23 2022 at 17:13):

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 (Dec 23 2022 at 17:18):

In mathlib3 the proof is provided with an autoparam

Eric Wieser (Dec 23 2022 at 17:18):

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

Eric Wieser (Dec 23 2022 at 17:19):

Yeah, here

Eric Wieser (Dec 23 2022 at 17:20):

The autoparam in Lean4 is different and evidently less powerful

Eric Wieser (Dec 23 2022 at 17:21):

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

Eric Wieser (Dec 23 2022 at 17:23):

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

Riccardo Brasca (Dec 23 2022 at 17:23):

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

Riccardo Brasca (Dec 23 2022 at 17:24):

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

Eric Wieser (Dec 23 2022 at 18:07):

Prove them in the instance to match mathlib3

Eric Wieser (Dec 23 2022 at 18:07):

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


Last updated: Dec 20 2023 at 11:08 UTC