BoolAlg_BoolRing.lean

import Mathlib

namespace TAL

class BoolAlg (P : Type)  extends DistribLattice P, HasCompl P, BoundedOrder P where
  inf_compl_eq_bot (x : P) : x ⊓ xᶜ = ⊥
  sup_compl_eq_top (x : P) : x ⊔ xᶜ = ⊤

class BoolRing (P : Type _ )extends Ring P where
  idempotent (a : P) : a * a = a

namespace BoolAlg

lemma compl_inf_eq_bot [BoolAlg P] (x : P) : xᶜ ⊓ x = ⊥
:= by rw [inf_comm, inf_compl_eq_bot]

lemma compl_sup_eq_top [BoolAlg P] (x : P) : xᶜ ⊔ x = ⊤
:= by rw [sup_comm, sup_compl_eq_top]

lemma compl_top [BoolAlg P] : (⊤ : P)ᶜ = ⊥
:= by rw [<- top_inf_eq ⊤ᶜ, inf_compl_eq_bot]

lemma compl_bot [BoolAlg P] : (⊥ : P)ᶜ = ⊤
:= by rw [<- bot_sup_eq ⊥ᶜ, sup_compl_eq_top]

lemma compl_inf [BoolAlg P] (a b : P) : (a ⊓ b)ᶜ = aᶜ ⊔ bᶜ
:= by
  apply le_antisymm; swap
  · apply sup_le
    · rw [<- inf_top_eq aᶜ, <- compl_sup_eq_top (a ⊓ b)]
      rw [inf_sup_left, <- inf_assoc, compl_inf_eq_bot, bot_inf_eq, sup_bot_eq]
      apply inf_le_right
    · rw [<- inf_top_eq bᶜ, <- compl_sup_eq_top (a ⊓ b)]
      rw [inf_sup_left, inf_comm a b, <- inf_assoc _ b a, compl_inf_eq_bot]
      rw [bot_inf_eq, sup_bot_eq]
      apply inf_le_right
  · rw [<- inf_top_eq (a ⊓ b)ᶜ, <- sup_compl_eq_top a]
    rw [inf_sup_left]
    apply sup_le; swap
    · apply le_trans
      · apply inf_le_right
      · apply le_sup_left
    · rw [<- inf_top_eq ((a ⊓ b)ᶜ ⊓ a), <- sup_compl_eq_top b]
      rw [inf_sup_left, inf_assoc, compl_inf_eq_bot, bot_sup_eq]
      apply le_trans
      · apply inf_le_right
      · apply le_sup_right

lemma compl_sup [BoolAlg P] (a b : P) : (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ
:= by
  apply le_antisymm
  · apply le_inf
    · rw [<- sup_bot_eq aᶜ, <- compl_inf_eq_bot (a ⊔ b)]
      rw [sup_inf_left, <- sup_assoc, compl_sup_eq_top, top_sup_eq, inf_top_eq]
      apply le_sup_right
    · rw [<- sup_bot_eq bᶜ, <- compl_inf_eq_bot (a ⊔ b)]
      rw [sup_inf_left, sup_comm a b, <- sup_assoc _ b a, compl_sup_eq_top]
      rw [top_sup_eq, inf_top_eq]
      apply le_sup_right
  · rw [<- sup_bot_eq (a ⊔ b)ᶜ, <- inf_compl_eq_bot a, sup_inf_left]
    apply le_inf; swap
    · apply le_trans
      · apply inf_le_left
      · apply le_sup_right
    · rw [<- sup_bot_eq ((a ⊔ b)ᶜ ⊔ a), <- inf_compl_eq_bot b]
      rw [sup_inf_left, sup_assoc, compl_sup_eq_top, top_inf_eq]
      apply le_trans
      · apply inf_le_right
      · apply le_sup_right

lemma compl_compl [BoolAlg P] (x : P) : xᶜᶜ = x
:= by
  conv =>
    arg 1;
    rw [<- inf_top_eq xᶜᶜ, <- sup_compl_eq_top x]
    rw [inf_sup_left, compl_inf_eq_bot, sup_bot_eq]
  conv =>
    arg 2
    rw [<- inf_top_eq x, <- sup_compl_eq_top xᶜ]
    rw [inf_sup_left, inf_compl_eq_bot, bot_sup_eq]
  rw [inf_comm]

instance toRing [BoolAlg P] : Ring P
where
  add a b := (a ⊓ bᶜ) ⊔ (aᶜ ⊓ b)
  sub a b := (a ⊓ bᶜ) ⊔ (aᶜ ⊓ b)
  mul a b := a ⊓ b
  zero := ⊥
  one := ⊤
  neg a := a
  add_comm a b := by
    simp [HAdd.hAdd]
    rw [sup_inf_left, sup_inf_right, sup_compl_eq_top, top_inf_eq]
    rw [sup_inf_right, sup_comm bᶜ b, sup_compl_eq_top, inf_top_eq]
    rw [sup_inf_left, sup_inf_right, sup_compl_eq_top, top_inf_eq]
    rw [sup_inf_right, sup_comm aᶜ a, sup_compl_eq_top, inf_top_eq]
    rw [sup_comm bᶜ, sup_comm b]
  add_assoc a b c := by
    simp [HAdd.hAdd]
    conv =>
      arg 1
      rw [inf_sup_right]
      rw [compl_sup, compl_inf, compl_inf, compl_compl, compl_compl]
      rw [inf_sup_left]
      rw [inf_sup_right _ _ a, compl_inf_eq_bot, bot_sup_eq]
      rw [inf_sup_right _ _ bᶜ, inf_compl_eq_bot, sup_bot_eq]
      rw [inf_sup_right, inf_comm b a, sup_comm (a ⊓ b ⊓ c), <- sup_assoc]
    conv =>
      arg 2
      rw [compl_sup, compl_inf, compl_inf, compl_compl, compl_compl, inf_sup_left]
      rw [inf_sup_right, compl_inf_eq_bot, bot_sup_eq]
      rw [inf_sup_right, inf_compl_eq_bot, sup_bot_eq]
      rw [inf_sup_left, inf_sup_left, sup_assoc, sup_comm]
      rw [<- inf_assoc, <- inf_assoc, <- inf_assoc]
      rw [<- sup_assoc, inf_comm c b, <- inf_assoc a]
  add_zero a := by
    conv => arg 1; arg 2; change ⊥
    simp [HAdd.hAdd]
    rw [compl_bot]; simp
  zero_add a := by
    conv => arg 1; arg 1; change ⊥
    simp [HAdd.hAdd]
    rw [compl_bot]; simp
  mul_assoc a b c := by
    change (a ⊓ b) ⊓ c = a ⊓ (b ⊓ c)
    rw [inf_assoc]
  zero_mul a := by
    change ⊥ ⊓ a = ⊥; simp
  mul_zero a := by
    change a ⊓ ⊥ = ⊥; simp
  one_mul a := by
    change ⊤ ⊓ a = a; simp
  mul_one a := by
    change a ⊓ ⊤ = a; simp
  left_distrib a b c := by
    simp [HAdd.hAdd, HMul.hMul]
    conv =>
      arg 1
      rw [inf_sup_left, <- inf_assoc, <- inf_assoc]
    conv =>
      arg 2
      rw [compl_inf, inf_sup_left]
      rw [inf_comm, <- inf_assoc, compl_inf_eq_bot, bot_inf_eq, bot_sup_eq]
      rw [compl_inf, <- inf_assoc, inf_sup_right, compl_inf_eq_bot, bot_sup_eq]
      rw [inf_comm _ a]
  right_distrib a b c := by
    simp [HAdd.hAdd, HMul.hMul]
    conv =>
      arg 1
      rw [inf_sup_right]
    conv =>
      arg 2
      rw [compl_inf, inf_sup_left]
      rw [inf_assoc a c cᶜ, inf_compl_eq_bot, inf_bot_eq, sup_bot_eq]
      rw [compl_inf, inf_comm b c, <- inf_assoc, inf_sup_right, compl_inf_eq_bot, sup_bot_eq]
      rw [inf_assoc, inf_comm c, inf_assoc, inf_comm c, <- inf_assoc, <- inf_assoc]
  neg_add_cancel x := by
    simp [HAdd.hAdd]
    rw [inf_compl_eq_bot]; rfl
  nsmul n a := by
    letI : Zero P := ⟨⊥⟩
    letI : Add P := ⟨(fun a b => (a ⊓ bᶜ) ⊔ (aᶜ ⊓ b))⟩
    apply nsmulRec n a
  zsmul n a := by
    letI : Zero P := ⟨⊥⟩
    letI : Add P := ⟨(fun a b => (a ⊓ bᶜ) ⊔ (aᶜ ⊓ b))⟩
    letI : Neg P := ⟨fun a => a⟩
    apply  zsmulRec (nsmulRec ) n a

instance toBoolRing [BoolAlg P] : BoolRing P
  where
  idempotent a := by simp [HMul.hMul, Mul.mul]

end BoolAlg

namespace BoolRing

lemma add_self_cancel [BoolRing P] (a : P) : a + a = 0
:= by
  have H := idempotent (a + a)
  rw [mul_add, add_mul, idempotent] at H
  simp at H; rw [H]

instance [BoolRing P] : CommRing P
where
  mul_comm := by
    intro x y
    have H := idempotent (x + y)
    rw [mul_add, add_mul, add_mul, idempotent, idempotent] at H
    rw [add_comm _ y, <- add_assoc, add_assoc x, add_comm _ y, <- add_assoc, add_assoc (x + y)] at H
    rw [add_eq_left] at H
    rw [<- add_self_cancel (x * y)] at H
    rw [add_left_inj] at H
    rw [H]

instance toLattice [BoolRing P ] : Lattice P
where
  inf a b := a * b
  sup a b := a + b + a * b
  le a b := a * b = a
  le_refl a := by
    rw [idempotent]
  le_trans a b c Ha Hb := by
    conv => arg 1; rw [<- Ha, mul_assoc, Hb, Ha]
  le_antisymm a b Ha Hb := by
    conv => arg 1; rw [<- Ha, <- Hb, mul_comm, mul_assoc, idempotent, Hb]
  sup_le a b c Ha Hb := by
    conv =>
      arg 1;
      rw [add_mul, add_mul, Ha, Hb]
      rw [mul_assoc, Hb]
  le_sup_left a b := by
    rw [mul_add, mul_add, <- mul_assoc]
    rw [idempotent, add_assoc, add_self_cancel, add_zero]
  le_sup_right a b := by
    rw [mul_add, mul_add]
    rw [mul_comm a b, <- mul_assoc]
    rw [idempotent, add_comm _ b, add_assoc, add_self_cancel, add_zero]
  le_inf a b c Ha Hb := by
    rw [<- mul_assoc, Ha, Hb]
  inf_le_left a b := by
    rw [mul_comm a b, mul_assoc, idempotent]
  inf_le_right a b := by
    rw [mul_assoc, idempotent]

instance toDistribLattice [BoolRing P] : DistribLattice P
where
  le_sup_inf a b c := by
    simp [min, Lattice.inf]
    simp [max, SemilatticeSup.sup]
    rw [mul_add, mul_add]
    conv =>
      arg 1; arg 1; arg 1
      rw [add_mul, add_mul, idempotent]
      rw [mul_comm a b, mul_assoc, idempotent]
      rw [add_assoc, add_self_cancel, add_zero]
    conv =>
      arg 1; arg 1; arg 2
      rw [add_mul, add_mul]
    conv =>
      arg 1; arg 2
      rw [add_mul, add_mul]
      rw [<- mul_assoc, idempotent]
      rw [<- mul_assoc b, mul_comm b a]
      rw [mul_comm a b, <- mul_assoc, mul_assoc b a a, idempotent, mul_comm b a]
      rw [add_assoc, add_self_cancel, add_zero]
    conv =>
      arg 1
      rw [add_assoc, add_comm _ (a * c)]
      rw [<- add_assoc (a * c), <- add_assoc (a * c), add_self_cancel, zero_add]
      rw [<- add_assoc]
    rw [<- mul_assoc]

instance toBoundedOrder [BoolRing P] : BoundedOrder P
where
  top := 1
  bot := 0
  le_top a := by
    simp only [LE.le]; rw [mul_one]
  bot_le a := by
    simp only [LE.le]; rw [zero_mul]

instance toHasCompl [BoolRing P] : HasCompl P
where
  compl a := 1 + a

instance toBoolAlg [BoolRing P] : BoolAlg P
where
  inf_compl_eq_bot (x : P) : x ⊓ xᶜ = ⊥ := by
    simp [min, SemilatticeInf.inf, Lattice.inf, compl]
    rw [mul_add, mul_one, idempotent, add_self_cancel]
    rfl
  sup_compl_eq_top (x : P) : x ⊔ xᶜ = ⊤ := by
    simp [max, SemilatticeSup.sup, compl]
    rw [mul_add, mul_one, idempotent, add_self_cancel, add_zero]
    rw [add_comm, add_assoc, add_self_cancel, add_zero]
    rfl

end BoolRing

end TAL