LinearOrder in mathlib3/4

Stream: mathlib4

[Kevin Buzzard]

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]

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

[David Renshaw]

(added a comment there to elaborate a bit)

[Mario Carneiro]

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

[Mario Carneiro]

(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]

although I guess mathport can do this alignment too

[David Renshaw]

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

[David Renshaw]

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

[David Renshaw]

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

[Mario Carneiro]

that's intros; exact iff.rfl

[David Renshaw]

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

invalid auto tactic, identifier is not allowed

[Scott Morrison]

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

[Scott Morrison]

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]

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