-- Boolean algebras bundled as ordered sets, with the complement compl(P)
-- 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.BooleanAlgebra
import Boolean
import Linear

-- A Boolean algebra is a bounded distributive lattice in which every
-- element has a complement; the complement is read back as compl(P)(a).
-- Only the bounded-lattice projection is an instance, so that Lattice(P)
-- has one derivation from a Boolean hypothesis.
predicate BooleanAlgebra (P : Set) :=
  DistributiveLattice(P) ∧ BoundedLattice(P) ∧
  (∀ a ∈ points(P), ∃ b, IsCompl(P, a, b))

notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis BooleanAlgebra(P) for P.points
notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis BooleanAlgebra(P) for P.points
notation infix 50 "≤" => Le(P, _, _) via hypothesis BooleanAlgebra(P) for P.points

theorem BooleanAlgebra.distributive_of (P : Set)
  requires boolean : BooleanAlgebra(P)
  shows DistributiveLattice(P)
proof
  obtain ⟨distributive, bounded, complemented⟩ := boolean
  exact distributive

instance BooleanAlgebra.bounded_of (P : Set)
  requires boolean : BooleanAlgebra(P)
  shows BoundedLattice(P)
proof
  obtain ⟨distributive, bounded, complemented⟩ := boolean
  exact bounded

theorem BooleanAlgebra.lattice_of (P : Set)
  requires boolean : BooleanAlgebra(P)
  shows Lattice(P)
proof
  exact BoundedLattice.lattice_of with (BooleanAlgebra.bounded_of with boolean)

theorem BooleanAlgebra.exists_isCompl (P a : Set)
  requires boolean : BooleanAlgebra(P)
  requires aIn : a ∈ points(P)
  shows ∃ b, IsCompl(P, a, b)
proof
  obtain ⟨distributive, bounded, complemented⟩ := boolean
  exact complemented with a, aIn

-- Bridges to the unbundled form IsBooleanAlgebra(A, r, bot, top).
instance BooleanAlgebra.unbundled (P : Set)
  requires boolean : BooleanAlgebra(P)
  shows IsBooleanAlgebra(points(P), le(P), bot(P), top(P))
proof
  have distributive := BooleanAlgebra.distributive_of with boolean
  have bounded := BooleanAlgebra.bounded_of with boolean
  have both := BoundedLattice.bounded_distributive with distributive, bounded
  constructor
  . exact both
  . intros a aIn
    obtain ⟨b, compl⟩ := BooleanAlgebra.exists_isCompl with boolean, aIn
    witness b
    exact IsCompl.unbundled with bounded, compl

theorem BooleanAlgebra.mk (A r b t : Set)
  requires boolean : IsBooleanAlgebra(A, r, b, t)
  shows BooleanAlgebra(Order.mk(A, r))
proof
  have boundedU := IsBooleanAlgebra.bounded with boolean
  have bounded := BoundedLattice.mk with boundedU
  have distributive := DistributiveLattice.mk with
      (IsBooleanAlgebra.distributive with boolean)
  have botEq := bot.mk with boundedU
  have topEq := top.mk with boundedU
  refine ⟨distributive, bounded, ?_⟩
  intros a aIn
  rw Order.mk.points at aIn
  obtain ⟨c, compl⟩ := IsBooleanAlgebra.exists_complement with boolean, aIn
  witness c
  have aIn2 : a ∈ points(Order.mk(A, r))
    rw Order.mk.points
    exact aIn
  apply IsCompl.of_complementary with bounded, aIn2
  rw [Order.mk.points, Order.mk.le, botEq, topEq]
  exact compl

defgraph compl (P : Set) (a ∈ points(P)) : points(P) :=
  latticeComplement(points(P), le(P), bot(P), top(P), a)
requires boolean : BooleanAlgebra(P)
proof
  exact latticeComplement.member with
      (BooleanAlgebra.unbundled with boolean), member

-- The complement is written aᶜ, and the bounds ⊥ and ⊤, wherever a
-- hypothesis in scope supplies the Boolean algebra.
notation postfix 90 "ᶜ" => apply(compl(P), _) via hypothesis BooleanAlgebra(P) for P.points
notation constant "⊥" => bot(P) via hypothesis BooleanAlgebra(P) for P.points
notation constant "⊤" => top(P) via hypothesis BooleanAlgebra(P) for P.points

section BooleanLaws
variable (P : Set)
hypothesis boolean : BooleanAlgebra(P)

-- The bundled complement is the unbundled one.
theorem compl.complement (a ∈ points(P))
  shows compl(P)(a) = latticeComplement(points(P), le(P), bot(P), top(P), a)
proof
  exact compl.value with boolean, assumption

instance compl.member (a ∈ points(P))
  shows compl(P)(a) ∈ points(P)
proof
  rw compl.complement
  exact latticeComplement.member with
      (BooleanAlgebra.unbundled with boolean), assumption

theorem compl.isCompl (a ∈ points(P))
  shows IsCompl(P, a, compl(P)(a))
proof
  have complementary := latticeComplement.complementary with
      (BooleanAlgebra.unbundled with boolean), assumption
  rw compl.complement
  exact IsCompl.of_complementary with
      (BooleanAlgebra.bounded_of with boolean), assumption

theorem inf_compl_eq_bot (a ∈ points(P))
  shows a ⊓ aᶜ = ⊥
proof
  rw [inf.meet, compl.complement]
  exact latticeComplement.meet with
      (BooleanAlgebra.unbundled with boolean), assumption

theorem sup_compl_eq_top (a ∈ points(P))
  shows a ⊔ compl(P)(a) = top(P)
proof
  rw [sup.join, compl.complement]
  exact latticeComplement.join with
      (BooleanAlgebra.unbundled with boolean), assumption

theorem compl_inf_eq_bot (a ∈ points(P))
  shows compl(P)(a) ⊓ a = bot(P)
proof
  rw [inf.meet, compl.complement]
  exact latticeComplement.meet_left with
      (BooleanAlgebra.unbundled with boolean), assumption

theorem compl_sup_eq_top (a ∈ points(P))
  shows compl(P)(a) ⊔ a = top(P)
proof
  rw [sup.join, compl.complement]
  exact latticeComplement.join_left with
      (BooleanAlgebra.unbundled with boolean), assumption

theorem IsCompl.compl_eq (b : Set) (a ∈ points(P))
  requires compl : IsCompl(P, a, b)
  shows b = compl(P)(a)
proof
  have complementary := IsCompl.unbundled with
      (BooleanAlgebra.bounded_of with boolean), compl
  rw compl.complement
  exact latticeComplement.of_complementary with
      (BooleanAlgebra.unbundled with boolean), assumption, complementary

theorem compl_compl (a ∈ points(P))
  shows (aᶜ)ᶜ = a
proof
  have complIn : compl(P)(a) ∈ points(P) := compl.member with *
  rw [compl.complement, compl.complement]
  exact latticeComplement.involutive with
      (BooleanAlgebra.unbundled with boolean), assumption

theorem compl_bot
  shows compl(P)(bot(P)) = top(P)
proof
  have botIn : bot(P) ∈ points(P) := bot.member with *
  rw compl.complement
  exact latticeComplement.bottom with (BooleanAlgebra.unbundled with boolean)

theorem compl_top
  shows compl(P)(top(P)) = bot(P)
proof
  have topIn : top(P) ∈ points(P) := top.member with *
  rw compl.complement
  exact latticeComplement.top with (BooleanAlgebra.unbundled with boolean)

theorem compl_injective (a b ∈ points(P))
  requires same : compl(P)(a) = compl(P)(b)
  shows a = b
proof
  rw [compl.complement, compl.complement] at same
  exact latticeComplement.injective with
      (BooleanAlgebra.unbundled with boolean), *

theorem compl_sup (a b ∈ points(P))
  shows compl(P)(a ⊔ b) = compl(P)(a) ⊓ compl(P)(b)
proof
  have supIn : a ⊔ b ∈ points(P) := sup.member with *
  have complA : compl(P)(a) ∈ points(P) := compl.member with *
  have complB : compl(P)(b) ∈ points(P) := compl.member with *
  simp [sup.join, inf.meet, compl.complement]
  exact latticeComplement.join_eq with
      (BooleanAlgebra.unbundled with boolean), *

theorem compl_inf (a b ∈ points(P))
  shows compl(P)(a ⊓ b) = compl(P)(a) ⊔ compl(P)(b)
proof
  have infIn : a ⊓ b ∈ points(P) := inf.member with *
  have complA : compl(P)(a) ∈ points(P) := compl.member with *
  have complB : compl(P)(b) ∈ points(P) := compl.member with *
  simp [sup.join, inf.meet, compl.complement]
  exact latticeComplement.meet_eq with
      (BooleanAlgebra.unbundled with boolean), *

theorem le_compl_iff_inf_eq_bot (a b ∈ points(P))
  shows a ≤ compl(P)(b) ↔ a ⊓ b = bot(P)
proof
  rw [inf.meet, compl.complement]
  have characterization := latticeComplement.le_iff_meet_bottom at points(P),
      le(P), bot(P), top(P), a, b with (BooleanAlgebra.unbundled with boolean),
      assumption, assumption
  constructor
  . intro h
    exact characterization.forward with (Le.relates with h)
  . intro h
    exact Le.of_relates with (characterization.backward with h)

theorem compl_le_compl (a b ∈ points(P))
  requires hab : a ≤ b
  shows compl(P)(b) ≤ compl(P)(a)
proof
  rw [compl.complement, compl.complement]
  unfold Le
  exact latticeComplement.antitone with (BooleanAlgebra.unbundled with boolean),
      assumption, assumption, (Le.relates with hab)

theorem compl_le_compl_iff_le (a b ∈ points(P))
  shows compl(P)(b) ≤ compl(P)(a) ↔ a ≤ b
proof
  rw [compl.complement, compl.complement]
  have characterization := latticeComplement.le_iff at points(P), le(P),
      bot(P), top(P), a, b with (BooleanAlgebra.unbundled with boolean),
      assumption, assumption
  constructor
  . intro h
    exact Le.of_relates with (characterization.backward with (Le.relates with h))
  . intro h
    exact Le.of_relates with (characterization.forward with (Le.relates with h))

end BooleanLaws

-- The powerset of a set is a Boolean algebra whose complement is the
-- relative complement.
instance powersetLattice.boolean (X : Set)
  shows BooleanAlgebra(powersetLattice(X))
proof
  unfold powersetLattice
  exact BooleanAlgebra.mk with (powersetOrder.boolean at X)

section PowersetBoolean
variable (X : Set)
hypothesis boolean : BooleanAlgebra(powersetLattice(X))

theorem powersetLattice.compl (B ∈ 𝒫(X))
  shows compl(powersetLattice(X))(B) = X ∖ B
proof
  have complete : CompleteLattice(powersetLattice(X)) := powersetLattice.complete at X
  have BIn : B ∈ points(powersetLattice(X)) := powersetLattice.member at X, B with
      *
  have botEq := powersetLattice.bot with complete
  have topEq := powersetLattice.top with complete
  rw [compl.complement, powersetLattice.points, powersetLattice.le, botEq, topEq]
  exact powersetOrder.complement_value with *

end PowersetBoolean

-- The Boolean rewrite set: double complements, the complements of the
-- bounds, and the meet and join of an element with its complement.
tactic boolean_simp := simp [compl_compl, compl_bot, compl_top, inf_compl_eq_bot, sup_compl_eq_top, compl_inf_eq_bot, compl_sup_eq_top]