-- Distributive and modular lattices, cancellation, and unique complements
-- 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.Distributive
import Complete

predicate IsDistributiveLattice (A r : Set) :=
  IsLattice(A, r) ∧
  (∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A,
    meet(A, r, x, join(A, r, y, z)) = join(A, r, meet(A, r, x, y), meet(A, r, x, z)))

predicate IsModularLattice (A r : Set) :=
  IsLattice(A, r) ∧
  (∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A, relates(r, y, x) →
    meet(A, r, x, join(A, r, y, z)) = join(A, r, y, meet(A, r, x, z)))

predicate BoundedDistributiveLattice (A r bot top : Set) :=
  IsDistributiveLattice(A, r) ∧ Least(A, r, A, bot) ∧ Greatest(A, r, A, top)

theorem IsDistributiveLattice.lattice (A r : Set)
  requires h : IsDistributiveLattice(A, r)
  shows IsLattice(A, r)
proof
  simp [IsDistributiveLattice]

theorem IsDistributiveLattice.meet_join (A r x y z : Set)
  requires h : IsDistributiveLattice(A, r)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ A
  shows
    meet(A, r, x, join(A, r, y, z)) = join(A, r, meet(A, r, x, y), meet(A, r, x, z))
proof
  rcases h with ⟨lattice, law⟩
  exact law with x, hx, y, hy, z, hz

theorem IsDistributiveLattice.meet_join_right (A r x y z : Set)
  requires h : IsDistributiveLattice(A, r)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ A
  shows
    meet(A, r, join(A, r, x, y), z) = join(A, r, meet(A, r, x, z), meet(A, r, y, z))
proof
  have lattice := IsDistributiveLattice.lattice with h
  have xyA := join.member with lattice, hx, hy
  have outer := meet.commutative with lattice, xyA, hz
  have leftSwap := meet.commutative with lattice, hz, hx
  have rightSwap := meet.commutative with lattice, hz, hy
  have expand := IsDistributiveLattice.meet_join with h, hz, hx, hy
  rw [outer, expand, leftSwap, rightSwap]
  rfl

-- The dual distributive law follows from the first.

theorem IsDistributiveLattice.join_meet (A r x y z : Set)
  requires h : IsDistributiveLattice(A, r)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ A
  shows
    join(A, r, x, meet(A, r, y, z)) = meet(A, r, join(A, r, x, y), join(A, r, x, z))
proof
  have lattice := IsDistributiveLattice.lattice with h
  have xyA := join.member with lattice, hx, hy
  have zxA := meet.member with lattice, hz, hx
  have zyA := meet.member with lattice, hz, hy
  have expand := IsDistributiveLattice.meet_join with h, xyA, hx, hz
  have absorbFirst : meet(A, r, join(A, r, x, y), x) = x
    have swap := meet.commutative with lattice, xyA, hx
    rw swap
    exact meet.absorb with lattice, hx, hy
  have swapSecond := meet.commutative with lattice, xyA, hz
  have expandSecond := IsDistributiveLattice.meet_join with h, hz, hx, hy
  have regroup := join.associative with lattice, hx, zxA, zyA
  have absorbSecond := join.absorb_swap with lattice, hx, hz
  have swapLast := meet.commutative with lattice, hz, hy
  symm
  rw [expand, absorbFirst, swapSecond, expandSecond, ← regroup, absorbSecond,
      swapLast]
  rfl

theorem IsDistributiveLattice.of_join_meet (A r : Set)
  requires lattice : IsLattice(A, r)
  requires law : ∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A,
    join(A, r, x, meet(A, r, y, z)) = meet(A, r, join(A, r, x, y), join(A, r, x, z))
  shows IsDistributiveLattice(A, r)
proof
  constructor
  . exact lattice
  . intros x hx y hy z hz
    have xyA := meet.member with lattice, hx, hy
    have zxA := join.member with lattice, hz, hx
    have zyA := join.member with lattice, hz, hy
    have expand := law with meet(A, r, x, y), xyA, x, hx, z, hz
    have absorbFirst : join(A, r, meet(A, r, x, y), x) = x
      have swap := join.commutative with lattice, xyA, hx
      rw swap
      exact join.absorb with lattice, hx, hy
    have swapSecond := join.commutative with lattice, xyA, hz
    have expandSecond := law with z, hz, x, hx, y, hy
    have regroup := meet.associative with lattice, hx, zxA, zyA
    have absorbSecond := meet.absorb_swap with lattice, hx, hz
    have swapLast := join.commutative with lattice, hz, hy
    symm
    rw [expand, absorbFirst, swapSecond, expandSecond, ← regroup,
        absorbSecond, swapLast]
    rfl

theorem IsDistributiveLattice.join_meet_right (A r x y z : Set)
  requires h : IsDistributiveLattice(A, r)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ A
  shows
    join(A, r, meet(A, r, x, y), z) = meet(A, r, join(A, r, x, z), join(A, r, y, z))
proof
  have lattice := IsDistributiveLattice.lattice with h
  have xyA := meet.member with lattice, hx, hy
  have outer := join.commutative with lattice, xyA, hz
  have leftSwap := join.commutative with lattice, hz, hx
  have rightSwap := join.commutative with lattice, hz, hy
  have expand := IsDistributiveLattice.join_meet with h, hz, hx, hy
  rw [outer, expand, leftSwap, rightSwap]
  rfl

theorem IsDistributiveLattice.converse (A r : Set)
  requires h : IsDistributiveLattice(A, r)
  shows IsDistributiveLattice(A, converse(r, A, A))
proof
  have lattice := IsDistributiveLattice.lattice with h
  constructor
  . exact IsLattice.converse with lattice
  . intros x hx y hy z hz
    have yzA := meet.member with lattice, hy, hz
    have xyA := join.member with lattice, hx, hy
    have xzA := join.member with lattice, hx, hz
    have inner := join.converse with lattice, hy, hz
    have outer := meet.converse with lattice, hx, yzA
    have leftDual := meet.converse with lattice, hx, hy
    have rightDual := meet.converse with lattice, hx, hz
    have joined := join.converse with lattice, xyA, xzA
    rw [inner, outer, leftDual, rightDual, joined]
    exact IsDistributiveLattice.join_meet with h, hx, hy, hz

-- Modularity

theorem IsModularLattice.lattice (A r : Set)
  requires h : IsModularLattice(A, r)
  shows IsLattice(A, r)
proof
  simp [IsModularLattice]

theorem IsModularLattice.law (A r x y z : Set)
  requires h : IsModularLattice(A, r)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ A
  requires hyx : relates(r, y, x)
  shows meet(A, r, x, join(A, r, y, z)) = join(A, r, y, meet(A, r, x, z))
proof
  rcases h with ⟨lattice, law⟩
  exact law with x, hx, y, hy, z, hz, hyx

theorem IsDistributiveLattice.modular (A r : Set)
  requires h : IsDistributiveLattice(A, r)
  shows IsModularLattice(A, r)
proof
  have lattice := IsDistributiveLattice.lattice with h
  constructor
  . exact lattice
  . intros x hx y hy z hz hyx
    have expand := IsDistributiveLattice.meet_join with h, hx, hy, hz
    have below := meet.of_ge with lattice, hx, hy, hyx
    rw [expand, below]
    rfl

-- Cancellation: in a distributive lattice an element is determined by its
-- meet and join with any fixed element.

theorem IsDistributiveLattice.cancel (A r x y z : Set)
  requires h : IsDistributiveLattice(A, r)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ A
  requires meets : meet(A, r, x, y) = meet(A, r, x, z)
  requires joins : join(A, r, x, y) = join(A, r, x, z)
  shows y = z
proof
  have lattice := IsDistributiveLattice.lattice with h
  have startAbsorb := meet.absorb_swap with lattice, hy, hx
  have expand := IsDistributiveLattice.meet_join with h, hy, hx, hz
  have swap := meet.commutative with lattice, hy, hx
  have collect := IsDistributiveLattice.meet_join_right with h, hx, hy, hz
  have endAbsorb := meet.absorb_swap with lattice, hz, hx
  have xzA := join.member with lattice, hx, hz
  have endSwap := meet.commutative with lattice, xzA, hz
  symm at startAbsorb
  symm at collect
  calc
    y = meet(A, r, y, join(A, r, x, y)) := startAbsorb
    _ = meet(A, r, y, join(A, r, x, z)) := by simp [joins]
    _ = join(A, r, meet(A, r, y, x), meet(A, r, y, z)) := expand
    _ = join(A, r, meet(A, r, x, y), meet(A, r, y, z)) := by simp [swap]
    _ = join(A, r, meet(A, r, x, z), meet(A, r, y, z)) := by simp [meets]
    _ = meet(A, r, join(A, r, x, y), z) := collect
    _ = meet(A, r, join(A, r, x, z), z) := by simp [joins]
    _ = meet(A, r, z, join(A, r, x, z)) := endSwap
    _ = z := endAbsorb

-- Bounded distributive lattices and the uniqueness of complements

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

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

theorem BoundedDistributiveLattice.bounded (A r bot top : Set)
  requires h : BoundedDistributiveLattice(A, r, bot, top)
  shows IsBoundedLattice(A, r, bot, top)
proof
  rcases h with ⟨distributive, least, greatest⟩
  have lattice := IsDistributiveLattice.lattice with distributive
  exact IsBoundedLattice.of_bounds with lattice, least, greatest

theorem BoundedDistributiveLattice.of_bounds (A r bot top : Set)
  requires distributive : IsDistributiveLattice(A, r)
  requires bounded : IsBoundedLattice(A, r, bot, top)
  shows BoundedDistributiveLattice(A, r, bot, top)
proof
  refine ⟨distributive, IsBoundedLattice.least with bounded,
      IsBoundedLattice.greatest with bounded⟩

theorem BoundedDistributiveLattice.converse (A r bot top : Set)
  requires h : BoundedDistributiveLattice(A, r, bot, top)
  shows BoundedDistributiveLattice(A, converse(r, A, A), top, bot)
proof
  have distributive := BoundedDistributiveLattice.distributive with h
  have bounded := BoundedDistributiveLattice.bounded with h
  exact BoundedDistributiveLattice.of_bounds with
      (IsDistributiveLattice.converse with distributive), (IsBoundedLattice.converse with bounded)

theorem Complementary.unique (A r bot top x y z : Set)
  requires h : BoundedDistributiveLattice(A, r, bot, top)
  requires hx : x ∈ A
  requires hy : Complementary(A, r, bot, top, x, y)
  requires hz : Complementary(A, r, bot, top, x, z)
  shows y = z
proof
  have distributive := BoundedDistributiveLattice.distributive with h
  have yA := Complementary.member with hy
  have zA := Complementary.member with hz
  have meetY := Complementary.meet with hy
  have meetZ := Complementary.meet with hz
  have joinY := Complementary.join with hy
  have joinZ := Complementary.join with hz
  have meets : meet(A, r, x, y) = meet(A, r, x, z)
    rw [meetY, meetZ]
    rfl
  have joins : join(A, r, x, y) = join(A, r, x, z)
    rw [joinY, joinZ]
    rfl
  exact IsDistributiveLattice.cancel with distributive, hx, yA, zA, meets, joins

-- The powerset lattice is distributive.

theorem powersetOrder.distributive (X : Set)
  shows IsDistributiveLattice(𝒫(X), powersetOrder(X))
proof
  constructor
  . exact powersetOrder.lattice at X
  . intros B hB C hC D hD
    have CX := powerset.membership_iff.forward with hC
    have DX := powerset.membership_iff.forward with hD
    have BX := powerset.membership_iff.forward with hB
    have unionIn : C ∪ D ∈ 𝒫(X) :=
      powerset.membership_iff.backward with (union2.subset with CX, DX)
    have leftIn : B ∩ C ∈ 𝒫(X) :=
      powerset.membership_iff.backward with (Subset.transitive with (intersection.subset_left at B, C), BX)
    have rightIn : B ∩ D ∈ 𝒫(X) :=
      powerset.membership_iff.backward with (Subset.transitive with (intersection.subset_left at B, D), BX)
    have innerJoin := powersetOrder.join with hC, hD
    have outerMeet := powersetOrder.meet with hB, unionIn
    have leftMeet := powersetOrder.meet with hB, hC
    have rightMeet := powersetOrder.meet with hB, hD
    have outerJoin := powersetOrder.join with leftIn, rightIn
    rw [innerJoin, outerMeet, leftMeet, rightMeet, outerJoin]
    exact intersection.union2_distrib at B, C, D

theorem powersetOrder.bounded_distributive (X : Set)
  shows BoundedDistributiveLattice(𝒫(X), powersetOrder(X), ∅, X)
proof
  exact BoundedDistributiveLattice.of_bounds with
      (powersetOrder.distributive at X), (powersetOrder.bounded at X)