agda-spa/lean/Spa/Lattice/AboveBelow.lean

/-
Port of `Lattice/AboveBelow.agda`: the flat lattice obtained by adjoining a
top and bottom element to an (unordered, decidable-equality) type.

With propositional equality the `_≈_` data type and its equivalence/decidability
proofs disappear (`deriving DecidableEq`). The lattice itself cannot be lifted:
mathlib has no "flat lattice on a discrete type". The `Lattice` instance is
built with `Lattice.mk'`, which — exactly like the Agda module — consumes the
two semilattices (comm/assoc, idempotence derived) plus the absorption laws,
and defines `a ≤ b ↔ a ⊔ b = b` (Agda's `_≼_`).

The Agda module's `Plain x` submodule (the witness `x` seeds the longest chain
`⊥ ≺ [x] ≺ ⊤`) becomes `plainFixedHeight x`; the boundedness proof `isLongest`
is restated through a rank function since chains are mathlib `LTSeries` rather
than a pattern-matchable inductive (the `¬-Chain-⊤`-style case analysis lives
in `rank_strictMono`).
-/
import Spa.Lattice

namespace Spa

/-- Agda: `AboveBelow` with constructors `⊥`, `⊤`, `[_]`. -/
inductive AboveBelow (α : Type*) where
  | bot
  | top
  | mk (x : α)
  deriving DecidableEq

namespace AboveBelow

/-- Agda: the `Showable` instance. -/
instance {α : Type*} [ToString α] : ToString (AboveBelow α) where
  toString
    | bot => "⊥"
    | top => "⊤"
    | mk x => toString x

variable {α : Type*} [DecidableEq α]

instance : Max (AboveBelow α) where
  max
    | bot, x => x
    | top, _ => top
    | mk x, mk y => if x = y then mk x else top
    | mk x, bot => mk x
    | mk _, top => top

instance : Min (AboveBelow α) where
  min
    | bot, _ => bot
    | top, x => x
    | mk x, mk y => if x = y then mk x else bot
    | mk _, bot => bot
    | mk x, top => mk x

/-! Agda: `⊥⊔x≡x`, `⊤⊔x≡⊤`, `x⊔⊥≡x`, `x⊔⊤≡⊤`, and the `[x]⊔[y]` reductions
(`x≈y⇒[x]⊔[y]≡[x]` / `x̷≈y⇒[x]⊔[y]≡⊤` are the two branches of `mk_sup_mk`). -/

@[simp] theorem bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl
@[simp] theorem top_sup (x : AboveBelow α) : top ⊔ x = top := rfl
@[simp] theorem sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl
@[simp] theorem sup_top (x : AboveBelow α) : x ⊔ top = top := by cases x <;> rfl
@[simp] theorem mk_sup_mk (x y : α) :
    (mk x ⊔ mk y : AboveBelow α) = if x = y then mk x else top := rfl

@[simp] theorem bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl
@[simp] theorem top_inf (x : AboveBelow α) : top ⊓ x = x := rfl
@[simp] theorem inf_bot (x : AboveBelow α) : x ⊓ bot = bot := by cases x <;> rfl
@[simp] theorem inf_top (x : AboveBelow α) : x ⊓ top = x := by cases x <;> rfl
@[simp] theorem mk_inf_mk (x y : α) :
    (mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl

/-- Agda: `⊔-comm`. -/
protected theorem sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by
  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
    [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
  split_ifs with h₁ h₂ h₂ <;> simp_all

/-- Agda: `⊔-assoc`. -/
protected theorem sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by
  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
    simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
  split_ifs <;> simp_all

/-- Agda: `⊓-comm`. -/
protected theorem inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by
  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
    [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
  split_ifs with h₁ h₂ h₂ <;> simp_all

/-- Agda: `⊓-assoc`. -/
protected theorem inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by
  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
    simp only [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
  split_ifs <;> simp_all

/-- Agda: `absorb-⊔-⊓`. -/
protected theorem sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by
  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
    simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk,
               bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;>
    try (split_ifs <;> simp_all)

/-- Agda: `absorb-⊓-⊔`. -/
protected theorem inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by
  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
    simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk,
               bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;>
    try (split_ifs <;> simp_all)

/-- Agda: `isLattice` (via the two semilattices + absorption, like the Agda
record; `Lattice.mk'` derives idempotence and sets `a ≤ b ↔ a ⊔ b = b`). -/
instance : Lattice (AboveBelow α) :=
  Lattice.mk' AboveBelow.sup_comm AboveBelow.sup_assoc
    AboveBelow.inf_comm AboveBelow.inf_assoc
    AboveBelow.sup_inf_self AboveBelow.inf_sup_self

theorem le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm

/-- Agda: `⊥≺[x]` (the `≤` part; `⊥` is least). -/
theorem bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a :=
  le_iff.mpr (bot_sup a)

/-- Agda: `[x]≺⊤` (the `≤` part; `⊤` is greatest). -/
theorem le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) :=
  le_iff.mpr (sup_top a)

theorem bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x :=
  lt_of_le_of_ne (bot_le' _) (by simp)

theorem mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
  lt_of_le_of_ne (le_top' _) (by simp)

theorem bot_lt_top : (bot : AboveBelow α) < top :=
  lt_of_le_of_ne (bot_le' _) (by simp)

/-- The order of the flat lattice, by cases (used to discharge the
monotonicity obligations that were `postulate`d in `Analysis/Sign.agda` and
`Analysis/Constant.agda`). -/
theorem le_cases {a b : AboveBelow α} (h : a ≤ b) :
    a = bot ∨ b = top ∨ a = b := by
  have hsup := le_iff.mp h
  rcases a with _ | _ | x <;> rcases b with _ | _ | y
  · exact Or.inl rfl
  · exact Or.inr (Or.inl rfl)
  · exact Or.inl rfl
  · exact absurd hsup (by simp)
  · exact Or.inr (Or.inl rfl)
  · exact absurd hsup (by simp)
  · exact absurd hsup (by simp)
  · exact Or.inr (Or.inl rfl)
  · rw [mk_sup_mk] at hsup
    by_cases hxy : x = y
    · exact Or.inr (Or.inr (by rw [hxy]))
    · rw [if_neg hxy] at hsup
      exact absurd hsup (by simp)

/-- Monotonicity for *strict* operations on flat lattices: if `f` sends `⊥` to
`⊥` (in either argument) and `⊤` to `⊤` (against any non-`⊥` argument), it is
monotone in both arguments — regardless of its values on plain elements.
`Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these
monotonicity facts for their `plus`/`minus`, all of which have this shape. -/
theorem monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
    (f : AboveBelow α → AboveBelow β → AboveBelow γ)
    (hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot)
    (htopl : ∀ y, y ≠ bot → f top y = top)
    (htopr : ∀ x, x ≠ bot → f x top = top) : Monotone₂ f := by
  constructor
  · intro y a b hab
    show f a y ≤ f b y
    rcases le_cases hab with rfl | rfl | rfl
    · rw [hbotl]; exact bot_le' _
    · rcases eq_or_ne y bot with rfl | hy
      · rw [hbotr, hbotr]
      · rw [htopl y hy]; exact le_top' _
    · exact le_rfl
  · intro x a b hab
    show f x a ≤ f x b
    rcases le_cases hab with rfl | rfl | rfl
    · rw [hbotr]; exact bot_le' _
    · rcases eq_or_ne x bot with rfl | hx
      · rw [hbotl, hbotl]
      · rw [htopr x hx]; exact le_top' _
    · exact le_rfl

/-! ### Interpretations of flat lattices

The `⟦⟧-⊔-∨` / `⟦⟧-⊓-∧` proofs of `Analysis/Sign.agda` and
`Analysis/Constant.agda` are the same case analysis; only the meaning of the
plain elements differs. Factored here, they need just `P ⊥ ↦ False`,
`P ⊤ ↦ True`, and (for `⊓`) disjointness of distinct plain elements. -/

section Interp

variable {V : Type*} {P : AboveBelow α → V → Prop}

/-- Agda: `⟦⟧ᵍ-⊔ᵍ-∨` / `⟦⟧ᶜ-⊔ᶜ-∨`, generalized. -/
theorem interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by
  rcases s₁ with _ | _ | x
  · rw [bot_sup]; exact h.resolve_left (hbot v)
  · rw [top_sup]; exact htop v
  · rcases s₂ with _ | _ | y
    · rw [sup_bot]; exact h.resolve_right (hbot v)
    · rw [sup_top]; exact htop v
    · rw [mk_sup_mk]
      split
      · next heq => subst heq; exact h.elim id id
      · exact htop v

/-- Agda: `⟦⟧ᵍ-⊓ᵍ-∧` / `⟦⟧ᶜ-⊓ᶜ-∧`, generalized. -/
theorem interp_inf_of
    (hdisj : ∀ {x y : α}, x ≠ y → ∀ v, ¬(P (mk x) v ∧ P (mk y) v))
    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∧ P s₂ v) : P (s₁ ⊓ s₂) v := by
  rcases s₁ with _ | _ | x
  · rw [bot_inf]; exact h.1
  · rw [top_inf]; exact h.2
  · rcases s₂ with _ | _ | y
    · rw [inf_bot]; exact h.2
    · rw [inf_top]; exact h.1
    · rw [mk_inf_mk]
      split
      · next heq => subst heq; exact h.1
      · next hne => exact absurd h (hdisj hne v)

end Interp

/-- Rank of an element: `⊥ ↦ 0`, `[x] ↦ 1`, `⊤ ↦ 2`. Used to bound chains
(Agda's `isLongest` / `x≺[y]⇒x≡⊥` / `[x]≺y⇒y≡⊤` case analysis lives here). -/
def rank : AboveBelow α → ℕ
  | bot => 0
  | mk _ => 1
  | top => 2

/-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and
`[x]≺y⇒y≡⊤`: the flat middle layer is an antichain). -/
theorem not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
  intro h
  obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h
  have hsup := le_iff.mp hle
  rw [mk_sup_mk] at hsup
  by_cases hxy : x = y
  · rw [if_pos hxy] at hsup
    exact hne hsup
  · rw [if_neg hxy] at hsup
    exact absurd hsup (by simp)

theorem rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
  intro a b hab
  rcases a with _ | _ | x <;> rcases b with _ | _ | y
  · exact absurd hab (lt_irrefl _)
  · simp [rank]
  · simp [rank]
  · exact absurd hab (bot_le' _).not_lt
  · exact absurd hab (lt_irrefl _)
  · exact absurd hab (le_top' _).not_lt
  · exact absurd hab (bot_le' _).not_lt
  · simp [rank]
  · exact absurd hab (not_mk_lt_mk x y)

/-- Agda: `isLongest` — no chain is longer than 2. -/
theorem boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by
  have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono)
  rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h
  have h2 : rank c.last ≤ 2 := by cases c.last <;> simp [rank]
  omega

/-- Agda: `Plain.longestChain`/`Plain.fixedHeight` and
`Plain.isFiniteHeightLattice`/`Plain.finiteHeightLattice` — the witness
(`default`, playing the role of the Agda module parameter `x`) seeds the chain
`⊥ ≺ [x] ≺ ⊤` of length 2. -/
instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where
  bot := bot
  top := top
  height := 2
  longest_chain :=
    { series :=
        ((RelSeries.singleton _ bot).snoc (mk default)
            (by rw [RelSeries.last_singleton]; exact bot_lt_mk default)).snoc top
          (by rw [RelSeries.last_snoc]; exact mk_lt_top default)
      head_series := by simp
      last_series := by simp
      length_series := by simp [RelSeries.snoc, RelSeries.append] }
  chains_bounded := boundedChains

end AboveBelow

end Spa