How to do exercise without le_antisymm?

Stream: new members

[Noble Mushtak (he/him)]

In Section 3.4 of Mathematics in Lean (https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf), there is this exercise:

example : a < b ↔ a ≤ b ∧ a ≠ b

and the book says: "Beyond logical operations, you do not need anything more than le_refl and le_trans." However, the official solution uses le_antisymm. Is there a way to solve this exercise without le_antisymm? Or is this just a typo in the book?

[Derek Rhodes]

This works and is maybe not cheating :). I had to use gt_irrefl to show that a < a is False. But I dug down through the the layers of its definition and found le_refl (or le_rfl) and le_trans. Maybe the same is true for le_antisymm ?

import Mathlib

variable {α : Type*} [PartialOrder α]
variable (a b : α)
-- le_refl and le_trans.
example : a < b ↔ a ≤ b ∧ a ≠ b := by
  rw [lt_iff_le_not_le]
  constructor
  · intro ⟨h₁, h₂⟩
    constructor
    · exact h₁
    · intro h
      apply h₂
      subst h
      exact h₁
  · intro ⟨h₁, h₂⟩
    constructor
    · exact h₁
    · intro h
      apply h₂
      rw [le_iff_lt_or_eq] at *
      obtain ha₁ | hb₁ := h₁
      obtain ha₂ | hb₂ := h
      · exfalso
        have :=
        calc a
          _< b := ha₁
          _< a := ha₂
        apply gt_irrefl a
        exact this
      · exact hb₂.symm
      · exact hb₁

[Daniel Weber]

Noble Mushtak (he/him) said:

In Section 3.4 of Mathematics in Lean (https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf), there is this exercise:

example : a < b ↔ a ≤ b ∧ a ≠ b

and the book says: "Beyond logical operations, you do not need anything more than le_refl and le_trans." However, the official solution uses le_antisymm. Is there a way to solve this exercise without le_antisymm? Or is this just a typo in the book?

I don't think this is possible — le_refl and le_trans are satisfied by preorders (docs#Preorder), but this theorem isn't true for preorders

[Noble Mushtak (he/him)]

@Derek Rhodes Your proof uses le_iff_lt_or_eq, which uses le_antisymm in its definition, so your proof still depends on le_antisymm

@Daniel Weber Makes sense, who should I contact about this error in the book to have it corrected?

[Daniel Weber]

You can make a pull request or open an issue in the github repository: https://github.com/avigad/mathematics_in_lean_source