-- Linear orders as distributive lattices, bundled
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Lattice.Linear
import LinearLattice
import DistribLattice

-- A linear order is a lattice: the join of two elements is the larger and
-- the meet the smaller, and the lattice is distributive.
theorem LinearOrder.lattice_of (P : Set)
  requires linear : LinearOrder(P)
  shows Lattice(P)
proof
  unfold Join.Lattice
  exact IsLinearOrder.lattice with (LinearOrder.unbundled with linear)

instance LinearOrder.distributive_of (P : Set)
  requires linear : LinearOrder(P)
  shows DistributiveLattice(P)
proof
  unfold DistribLattice.DistributiveLattice
  exact IsLinearOrder.distributive with (LinearOrder.unbundled with linear)

theorem LinearOrder.modular_of (P : Set)
  requires linear : LinearOrder(P)
  shows ModularLattice(P)
proof
  unfold DistribLattice.ModularLattice
  exact IsLinearOrder.modular with (LinearOrder.unbundled with linear)

notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis LinearOrder(P) for P.points
notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis LinearOrder(P) for P.points

theorem LinearOrder.dual (P : Set)
  requires linear : LinearOrder(P)
  shows LinearOrder(dual(P))
proof
  unfold dual
  apply LinearOrder.mk
  exact IsLinearOrder.converse with (LinearOrder.unbundled with linear)

section LinearLaws
variable (P : Set)
hypothesis linear : LinearOrder(P)

theorem sup_eq_left_or_right (a b ∈ points(P))
  shows a ⊔ b = a ∨ a ⊔ b = b
proof
  rw sup.join
  exact IsLinearOrder.join_cases with *

theorem inf_eq_left_or_right (a b ∈ points(P))
  shows a ⊓ b = a ∨ a ⊓ b = b
proof
  rw inf.meet
  exact IsLinearOrder.meet_cases with *

theorem sup_mem_pair (a b ∈ points(P))
  shows a ⊔ b ∈ {a, b}
proof
  rw sup.join
  exact IsLinearOrder.join_member_pair with *

theorem inf_mem_pair (a b ∈ points(P))
  shows a ⊓ b ∈ {a, b}
proof
  rw inf.meet
  exact IsLinearOrder.meet_member_pair with *

end LinearLaws