-- Boolean algebras: complemented distributive bounded lattices
-- 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.Boolean
import Distributive

predicate IsBooleanAlgebra (A r bot top : Set) :=
  BoundedDistributiveLattice(A, r, bot, top) ∧
  (∀ x ∈ A, ∃ y, Complementary(A, r, bot, top, x, y))

theorem IsBooleanAlgebra.bounded_distributive (A r bot top : Set)
  requires h : IsBooleanAlgebra(A, r, bot, top)
  shows BoundedDistributiveLattice(A, r, bot, top)
proof
  simp [IsBooleanAlgebra]

theorem IsBooleanAlgebra.distributive (A r bot top : Set)
  requires h : IsBooleanAlgebra(A, r, bot, top)
  shows IsDistributiveLattice(A, r)
proof
  exact BoundedDistributiveLattice.distributive with
      (IsBooleanAlgebra.bounded_distributive with h)

theorem IsBooleanAlgebra.bounded (A r bot top : Set)
  requires h : IsBooleanAlgebra(A, r, bot, top)
  shows IsBoundedLattice(A, r, bot, top)
proof
  exact BoundedDistributiveLattice.bounded with
      (IsBooleanAlgebra.bounded_distributive with h)

theorem IsBooleanAlgebra.lattice (A r bot top : Set)
  requires h : IsBooleanAlgebra(A, r, bot, top)
  shows IsLattice(A, r)
proof
  exact IsBoundedLattice.lattice with (IsBooleanAlgebra.bounded with h)

theorem IsBooleanAlgebra.exists_complement (A r bot top x : Set)
  requires h : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  shows ∃ y, Complementary(A, r, bot, top, x, y)
proof
  rcases h with ⟨bounded, complemented⟩
  exact complemented with x, hx

-- The complement of an element is its unique complementary element.

defunique latticeComplement (A r bot top x : Set) (y ∈ A) :=
  Complementary(A, r, bot, top, x, y)
requires boolean : IsBooleanAlgebra(A, r, bot, top)
requires hx : x ∈ A
proof
  obtain ⟨y, hy⟩ := IsBooleanAlgebra.exists_complement with boolean, hx
  witness y
  refine ⟨Complementary.member with hy, hy⟩
uniqueness
  intros y yA first z zA second
  have bounded := IsBooleanAlgebra.bounded_distributive with boolean
  exact Complementary.unique with bounded, hx, first, second

theorem latticeComplement.member (A r bot top x : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  shows latticeComplement(A, r, bot, top, x) ∈ A
proof
  have selected := latticeComplement.selected with boolean, hx
  exact selected.left

theorem latticeComplement.complementary (A r bot top x : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  shows Complementary(A, r, bot, top, x, latticeComplement(A, r, bot, top, x))
proof
  have selected := latticeComplement.selected with boolean, hx
  exact selected.right

theorem latticeComplement.meet (A r bot top x : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  shows meet(A, r, x, latticeComplement(A, r, bot, top, x)) = bot
proof
  exact Complementary.meet with (latticeComplement.complementary with boolean,
      hx)

theorem latticeComplement.join (A r bot top x : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  shows join(A, r, x, latticeComplement(A, r, bot, top, x)) = top
proof
  exact Complementary.join with (latticeComplement.complementary with boolean,
      hx)

theorem latticeComplement.meet_left (A r bot top x : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  shows meet(A, r, latticeComplement(A, r, bot, top, x), x) = bot
proof
  have lattice := IsBooleanAlgebra.lattice with boolean
  have swap := meet.commutative with lattice,
      (latticeComplement.member with boolean, hx), hx
  rw swap
  exact latticeComplement.meet with boolean, hx

theorem latticeComplement.join_left (A r bot top x : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  shows join(A, r, latticeComplement(A, r, bot, top, x), x) = top
proof
  have lattice := IsBooleanAlgebra.lattice with boolean
  have swap := join.commutative with lattice,
      (latticeComplement.member with boolean, hx), hx
  rw swap
  exact latticeComplement.join with boolean, hx

theorem latticeComplement.of_complementary (A r bot top x y : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  requires h : Complementary(A, r, bot, top, x, y)
  shows y = latticeComplement(A, r, bot, top, x)
proof
  have bounded := IsBooleanAlgebra.bounded_distributive with boolean
  have selected := latticeComplement.complementary with boolean, hx
  exact Complementary.unique with bounded, hx, h, selected

theorem latticeComplement.involutive (A r bot top x : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  shows
    latticeComplement(A, r, bot, top, latticeComplement(A, r, bot, top, x)) = x
proof
  have bounded := IsBooleanAlgebra.bounded with boolean
  have complementA := latticeComplement.member with boolean, hx
  have selected := latticeComplement.complementary with boolean, hx
  have symmetric := Complementary.symmetric with bounded, hx, selected
  symm
  exact latticeComplement.of_complementary with boolean, complementA, symmetric

theorem latticeComplement.bottom (A r bot top : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  shows latticeComplement(A, r, bot, top, bot) = top
proof
  have bounded := IsBooleanAlgebra.bounded with boolean
  have botA := IsBoundedLattice.bottom_member with bounded
  symm
  exact latticeComplement.of_complementary with boolean, botA,
      (Complementary.bottom_top with bounded)

theorem latticeComplement.top (A r bot top : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  shows latticeComplement(A, r, bot, top, top) = bot
proof
  have bounded := IsBooleanAlgebra.bounded with boolean
  have topA := IsBoundedLattice.top_member with bounded
  symm
  exact latticeComplement.of_complementary with boolean, topA,
      (Complementary.top_bottom with bounded)

theorem latticeComplement.injective (A r bot top x y : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires same :
    latticeComplement(A, r, bot, top, x) = latticeComplement(A, r, bot, top, y)
  shows x = y
proof
  have twiceX := latticeComplement.involutive with boolean, hx
  have twiceY := latticeComplement.involutive with boolean, hy
  rw ← twiceX
  rw ← twiceY
  rw same
  rfl

-- De Morgan's laws

theorem latticeComplement.join_eq (A r bot top x y : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows latticeComplement(A, r, bot, top, join(A, r, x, y)) =
    meet(A, r, latticeComplement(A, r, bot, top, x), latticeComplement(A, r, bot, top, y))
proof
  have distributive := IsBooleanAlgebra.distributive with boolean
  have bounded := IsBooleanAlgebra.bounded with boolean
  have lattice := IsBooleanAlgebra.lattice with boolean
  have xA := latticeComplement.member with boolean, hx
  have yA := latticeComplement.member with boolean, hy
  have joinA := join.member with lattice, hx, hy
  have meetA := meet.member with lattice, xA, yA
  have meetBottom : meet(A, r, join(A, r, x, y), meet(A, r,
      latticeComplement(A, r, bot, top, x), latticeComplement(A, r, bot, top,
      y))) = bot
    have expand := IsDistributiveLattice.meet_join_right with distributive, hx,
        hy, meetA
    have regroupX := meet.associative with lattice, hx, xA, yA
    have swapInner := meet.commutative with lattice, xA, yA
    have regroupY := meet.associative with lattice, hy, yA, xA
    have cancelX := latticeComplement.meet with boolean, hx
    have cancelY := latticeComplement.meet with boolean, hy
    have absorbX := meet.bottom_left with bounded, yA
    have absorbY := meet.bottom_left with bounded, xA
    have botA := IsBoundedLattice.bottom_member with bounded
    rw [expand, ← regroupX, cancelX, absorbX, swapInner, ← regroupY, cancelY,
        absorbY]
    exact join.idempotent with lattice, botA
  have joinTop : join(A, r, join(A, r, x, y), meet(A, r, latticeComplement(A,
      r, bot, top, x), latticeComplement(A, r, bot, top, y))) = top
    have expand := IsDistributiveLattice.join_meet with distributive, joinA, xA,
        yA
    have swapOuter := join.commutative with lattice, hx, hy
    have regroupX := join.associative with lattice, hy, hx, xA
    have cancelX := latticeComplement.join with boolean, hx
    have absorbX := join.top_right with bounded, hy
    have regroupY := join.associative with lattice, hx, hy, yA
    have cancelY := latticeComplement.join with boolean, hy
    have absorbY := join.top_right with bounded, hx
    have topA := IsBoundedLattice.top_member with bounded
    rw expand
    rw [regroupY, cancelY, absorbY]
    rw [swapOuter, regroupX, cancelX, absorbX]
    exact meet.idempotent with lattice, topA
  have complementary : Complementary(A, r, bot, top, join(A, r, x, y), meet(A,
      r, latticeComplement(A, r, bot, top, x), latticeComplement(A, r, bot,
      top, y)))
    refine ⟨meetA, meetBottom, joinTop⟩
  symm
  exact latticeComplement.of_complementary with boolean, joinA, complementary

theorem latticeComplement.meet_eq (A r bot top x y : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows latticeComplement(A, r, bot, top, meet(A, r, x, y)) =
    join(A, r, latticeComplement(A, r, bot, top, x), latticeComplement(A, r, bot, top, y))
proof
  have lattice := IsBooleanAlgebra.lattice with boolean
  have xA := latticeComplement.member with boolean, hx
  have yA := latticeComplement.member with boolean, hy
  have joinA := join.member with lattice, xA, yA
  have deMorgan := latticeComplement.join_eq with boolean, xA, yA
  have twiceX := latticeComplement.involutive with boolean, hx
  have twiceY := latticeComplement.involutive with boolean, hy
  rw [twiceX, twiceY] at deMorgan
  rw ← deMorgan
  exact latticeComplement.involutive with boolean, joinA

-- Order and complements

theorem latticeComplement.le_iff_meet_bottom (A r bot top a b : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires ha : a ∈ A
  requires hb : b ∈ A
  shows
    relates(r, a, latticeComplement(A, r, bot, top, b)) ↔ meet(A, r, a, b) = bot
proof
  have distributive := IsBooleanAlgebra.distributive with boolean
  have bounded := IsBooleanAlgebra.bounded with boolean
  have lattice := IsBooleanAlgebra.lattice with boolean
  have reflexive := IsLattice.reflexive with lattice
  have bA := latticeComplement.member with boolean, hb
  have abA := meet.member with lattice, ha, hb
  constructor
  . intro below
    have bounded2 := meet.monotone with lattice, ha, hb, bA, hb, below,
        (reflexive with b, hb)
    have cancel := latticeComplement.meet_left with boolean, hb
    rw cancel at bounded2
    exact IsBoundedLattice.le_bottom_iff.forward with bounded, abA, bounded2
  . intro disjoint
    have unit := meet.top_right with bounded, ha
    have cover := latticeComplement.join with boolean, hb
    have expand := IsDistributiveLattice.meet_join with distributive, ha, hb, bA
    have abBotA := meet.member with lattice, ha, bA
    have absorb := join.bottom_left with bounded, abBotA
    symm at absorb
    symm at expand
    have equation : meet(A, r, a, latticeComplement(A, r, bot, top, b)) = a
      calc
        meet(A, r, a, latticeComplement(A, r, bot, top, b)) = join(A, r, bot, meet(A, r, a, latticeComplement(A, r, bot, top, b))) :=
          absorb
        _ = join(A, r, meet(A, r, a, b), meet(A, r, a, latticeComplement(A, r, bot, top, b))) :=
          by simp [disjoint]
        _ = meet(A, r, a, join(A, r, b, latticeComplement(A, r, bot, top, b))) := expand
        _ = meet(A, r, a, top) := by simp [cover]
        _ = a := unit
    exact meet.eq_left_iff.backward with lattice, ha, bA, equation

theorem latticeComplement.antitone (A r bot top x y : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hxy : relates(r, x, y)
  shows
    relates(r, latticeComplement(A, r, bot, top, y), latticeComplement(A, r, bot, top, x))
proof
  have bounded := IsBooleanAlgebra.bounded with boolean
  have lattice := IsBooleanAlgebra.lattice with boolean
  have reflexive := IsLattice.reflexive with lattice
  have yA := latticeComplement.member with boolean, hy
  have yxA := meet.member with lattice, yA, hx
  have below := meet.monotone with lattice, yA, hx, yA, hy,
      (reflexive with latticeComplement(A, r, bot, top, y), yA), hxy
  have cancel := latticeComplement.meet_left with boolean, hy
  rw cancel at below
  have disjoint := IsBoundedLattice.le_bottom_iff.forward with bounded, yxA,
    below
  exact latticeComplement.le_iff_meet_bottom.backward with boolean, yA, hx,
      disjoint

theorem latticeComplement.le_iff (A r bot top x y : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows relates(r, x, y) ↔
    relates(r, latticeComplement(A, r, bot, top, y), latticeComplement(A, r, bot, top, x))
proof
  constructor
  . intro hxy
    exact latticeComplement.antitone with boolean, hx, hy, hxy
  . intro reversed
    have xA := latticeComplement.member with boolean, hx
    have yA := latticeComplement.member with boolean, hy
    have twice := latticeComplement.antitone with boolean, yA, xA, reversed
    have twiceX := latticeComplement.involutive with boolean, hx
    have twiceY := latticeComplement.involutive with boolean, hy
    rw [twiceX, twiceY] at twice
    exact twice

theorem IsBooleanAlgebra.converse (A r bot top : Set)
  requires boolean : IsBooleanAlgebra(A, r, bot, top)
  shows IsBooleanAlgebra(A, converse(r, A, A), top, bot)
proof
  have bounded := IsBooleanAlgebra.bounded with boolean
  have distributive := IsBooleanAlgebra.bounded_distributive with boolean
  constructor
  . exact BoundedDistributiveLattice.converse with distributive
  . intros x hx
    have selected := latticeComplement.complementary with boolean, hx
    refine ⟨latticeComplement(A, r, bot, top, x),
        (Complementary.converse with bounded, hx, selected)⟩

-- The powerset of X is a Boolean algebra whose complements are relative
-- complements in X.

theorem powersetOrder.complementary (X B : Set)
  requires hB : B ∈ 𝒫(X)
  shows Complementary(𝒫(X), powersetOrder(X), ∅, X, B, X ∖ B)
proof
  have BX := powerset.membership_iff.forward with hB
  have differenceIn : X ∖ B ∈ 𝒫(X) :=
    powerset.membership_iff.backward with (difference.subset_left at X, B)
  have meetValue := powersetOrder.meet with hB, differenceIn
  have joinValue := powersetOrder.join with hB, differenceIn
  refine ⟨differenceIn, ?_, ?_⟩
  . rw meetValue
    have swap := intersection.commutative at B, X ∖ B
    rw swap
    exact difference.intersection_eq at X, B
  . rw joinValue
    exact difference.union2_of_subset with BX

theorem powersetOrder.boolean (X : Set)
  shows IsBooleanAlgebra(𝒫(X), powersetOrder(X), ∅, X)
proof
  constructor
  . exact powersetOrder.bounded_distributive at X
  . intros B hB
    refine ⟨X ∖ B, powersetOrder.complementary with hB⟩

theorem powersetOrder.complement_value (X B : Set)
  requires hB : B ∈ 𝒫(X)
  shows latticeComplement(𝒫(X), powersetOrder(X), ∅, X, B) = X ∖ B
proof
  have boolean := powersetOrder.boolean at X
  symm
  exact latticeComplement.of_complementary with boolean, hB,
      (powersetOrder.complementary with hB)