Zulip Chat Archive

Stream: mathlib4

Topic: LinearOrder in mathlib3/4


Kevin Buzzard (Oct 21 2022 at 17:40):

Lean 3:

instance : linear_order bool :=
{ le := λ a b, a = ff  b = tt,
  le_refl := dec_trivial,
  le_trans := dec_trivial,
  le_antisymm := dec_trivial,
  le_total := dec_trivial,
  decidable_le := infer_instance,
  decidable_eq := infer_instance,
  max := bor,
  max_def := by { funext x y, revert x y, exact dec_trivial },
  min := band,
  min_def := by { funext x y, revert x y, exact dec_trivial } }

Lean 4:

instance : LinearOrder Bool where
  le := fun a b => a = false  b = true
  le_refl := by unfold LE.le; decide
  le_trans := by unfold LE.le; decide
  le_antisymm := by unfold LE.le Preorder.toLE; decide
  le_total := by unfold LE.le Preorder.toLE PartialOrder.toPreorder; decide
  decidable_le := by unfold LE.le Preorder.toLE PartialOrder.toPreorder; exact inferInstance
  decidable_eq := inferInstance
  lt_iff_le_not_le := λ _ _ => Iff.rfl

Three differences:
1) Fields of structures are not seen through with decide, whereas they were with dec_trivial (and because structures extend other structures one has to unfold more and more as we go on)
2) lt_iff_not_le had . order_laws_tac in mathlib3. Does this tactic exist in mathlib4?
3) max and min are bundled into the definition in mathlib3, not in mathlib4.

Should I worry about any of these?

David Renshaw (Oct 21 2022 at 17:44):

(3) is https://github.com/leanprover-community/mathlib4/issues/369

David Renshaw (Oct 21 2022 at 17:55):

(added a comment there to elaborate a bit)

Mario Carneiro (Oct 21 2022 at 20:56):

IIRC order_laws_tac is an extremely simple tactic, something like intros; refl. So := by intros; rfl is a reasonable replacement

Mario Carneiro (Oct 21 2022 at 20:57):

(In lean 3 there was the restriction that auto params had to be just a name, which names a global definition containing the actual tactic, so even really trivial tactics had to be wrapped up like this. In lean 4 this process is automatic)

Mario Carneiro (Oct 21 2022 at 20:58):

although I guess mathport can do this alignment too

David Renshaw (Oct 21 2022 at 21:02):

https://github.com/leanprover-community/lean/blob/fc13c8c72a15dab71a2c2b31410c2cadc3526bd7/library/init/meta/tactic.lean#L1879

David Renshaw (Oct 21 2022 at 21:02):

meta def order_laws_tac := whnf_target >> intros >> to_expr ``(iff.refl _) >>= exact

David Renshaw (Oct 21 2022 at 21:03):

I can't tell whether that's actually equivalent to intros; rfl.

Mario Carneiro (Oct 21 2022 at 21:37):

that's intros; exact iff.rfl

David Renshaw (Oct 21 2022 at 21:39):

If I try to put that in the class Preorder declaration in mathlib4, I get

invalid auto tactic, identifier is not allowed

Scott Morrison (Nov 06 2022 at 08:44):

I've added the := by intros; rfl to Preorder as part of mathlib4#534, where @kbuzzard needed it.

Scott Morrison (Nov 06 2022 at 08:57):

Regarding Kevin's point 1) above, here is a standalone example.

In Lean 3, we can:

class P (α : Type*) extends has_le α :=
(h :  a : α, a  a)

@[simp]
theorem forall_bool {p : bool  Prop} : ( b, p b)  p false  p true :=
  λ h, by simp [h], λ h₁, h₂ b, by cases b; assumption

instance {p : bool  Prop} [ b, decidable (p b)] : decidable ( b, p b) :=
  decidable_of_decidable_of_iff infer_instance forall_bool.symm

instance : P bool :=
{ le := λ a b, a = false  b = true,
  h := dec_trivial, } -- No unfolding necessary.

while in Lean 4:

class P (α : Type u) extends LE α :=
(h :  a : α, a  a)

@[simp]
theorem forall_bool {p : Bool  Prop} : ( b, p b)  p false  p true :=
  fun h => by simp [h], fun h₁, h₂ b => by cases b <;> assumption

instance {p : Bool  Prop} [ b, Decidable (p b)] : Decidable ( b, p b) :=
  decidable_of_decidable_of_iff forall_bool.symm

instance : P Bool where
  le := fun a b => a = false  b = true
  h := by unfold LE.le; decide -- how do we do this without the unfold?

Scott Morrison (Nov 07 2022 at 03:42):

I've merged the PR, leaving a link to this discussion.


Last updated: Dec 20 2023 at 11:08 UTC