comm_semiring_of_boolean.lean

import algebra.ring.basic

open set

variables {X : Type*} {fil : set X → Prop}

/-- Let `X` be a Type.  Given a predicate `fil : set X → Prop` on subsets of `X`,
the Type `co fil` is the predicate on subsets of `X` that contains all the subsets
of `fil` and is closed under taking finite unions and complements.  It is
implemented with pairwise unions and, for this reason, we include `∅` in `co fil`.
Similar inductive Types could contain one among `{ ∅, univ}` and one among `{∪, ∩}`,
delegating lemmas to prove the others. -/
inductive co (fil : set X → Prop) : set X → Prop
| co_empty : co ∅
| co_fil   : ∀ f : set X, fil f → co f
| co_union    : ∀ {C D : set X}, co C → co D → co (C ∪ D)
| co_compl    : ∀ {C : set X}, co C → co Cᶜ

/--- `clo` is the SubType of `set X` consisting of the subsets spelled out by `co fil`. -/
def clo (fil : set X → Prop) := {s : set X // co fil s}

namespace clo

section boolean_definitions

/-- Equality in the subtype `clo fil` coincides with equality on the subsets. -/
@[simp] lemma eq_iff {a b : clo fil} : a = b ↔ a.1 = b.1 :=
subtype.ext_iff_val

/-- This lemma shows that intersections are implied by the remaining axioms for `clo`.
Should this lemma be named `co.co_in` instead?
`lemma co.co_in : ∀ {C D : set X}, co fil C → co fil D → co fil (C ∩ D) :=` -/
lemma inter {C D : set X} : co fil C → co fil D → co fil (C ∩ D) :=
begin
  intros cC cD,
  rw [← compl_compl (C ∩ D), compl_inter],
  exact co.co_compl (co.co_union (co.co_compl cC) (co.co_compl cD)),
end

/-- Should this lemma be named `co.co_univ` instead?
`lemma co.co_univ : co fil univ :=` -/
lemma univ : co fil univ :=
by rw [← compl_compl univ, compl_univ]; exact co.co_compl co.co_empty

lemma union {s t : set X} : co fil s → co fil t → co fil (s ∪ t) :=
λ cs ct, co.co_union cs ct

instance has_sup : has_sup (clo fil) :=
⟨λ a b, ⟨a.1 ∪ b.1, union a.2 b.2⟩⟩

@[simp] lemma sup_subtype {a b : clo fil} : (a ⊔ b).1 = a.1 ⊔ b.1 := rfl

instance has_inf : has_inf (clo fil) :=
⟨λ a b, ⟨a.1 ∩ b.1, inter a.2 b.2⟩⟩

@[simp] lemma inf_subtype {a b : clo fil} : (a ⊓ b).1 = a.1 ⊓ b.1 := rfl

instance has_top : has_top (clo fil) :=
⟨⟨_, univ ⟩⟩

instance has_bot : has_bot (clo fil) :=
⟨⟨_, co.co_empty ⟩⟩

instance has_compl : has_compl (clo fil) :=
⟨λ a, ⟨_, co.co_compl a.2⟩⟩

instance has_sdiff : has_sdiff (clo fil) :=
⟨λ a b, ⟨a.1 \ b.1, inter a.2 (co.co_compl b.2)⟩⟩

instance has_le : has_le (clo fil) :=
⟨λ a b, a.1 ⊆ b.1⟩

instance has_lt : has_lt (clo fil) :=
⟨λ a b, a ≤ b ∧ ¬ b ≤ a⟩

lemma le_refl : ∀ a : clo fil, a ≤ a :=
λ _ _ c, c

lemma le_trans : ∀ (a b c : clo fil), a ≤ b → b ≤ c → a ≤ c :=
λ _ _ _ ab bc _ xa, bc (ab xa)

lemma lt_iff_le_not_le : ∀ (a b : clo fil), a < b ↔ a ≤ b ∧ ¬b ≤ a :=
λ _ _, iff.refl _

lemma le_antisymm : ∀ (a b : clo fil), a ≤ b → b ≤ a → a = b :=
λ a b ab ba, eq_iff.mpr (le_antisymm ab ba)

instance partial_order : partial_order (clo fil) :=
{ le               := (≤),
  lt               := (<),
  le_refl          := le_refl,
  le_trans         := le_trans,
  lt_iff_le_not_le := lt_iff_le_not_le,
  le_antisymm      := le_antisymm }

lemma le_sup_left : ∀ a b : clo fil, a ≤ (a ⊔ b) :=
λ a b x xa, or.inl xa

lemma le_sup_right : ∀ a b : clo fil, b ≤ (a ⊔ b) :=
λ a b x xa, or.inr xa

lemma sup_le : ∀ (a b c : clo fil), a ≤ c → b ≤ c → a ⊔ b ≤ c :=
λ a b c, @sup_le (set X) _ _ _ _

lemma inf_le_left : ∀ (a b : clo fil), a ⊓ b ≤ a :=
λ _ _ _ ab, ab.1

lemma inf_le_right : ∀ (a b : clo fil), a ⊓ b ≤ b :=
λ _ _ _ ab, ab.2

lemma le_inf : ∀ (a b c : clo fil), a ≤ b → a ≤ c → a ≤ b ⊓ c :=
λ _ _ _ ab ac x xa, ⟨ab xa, ac xa⟩

lemma le_sup_inf : ∀ (x y z : clo fil), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z :=
λ a b c, @le_sup_inf (set X) _ _ _ _

lemma le_top : ∀ (a : clo fil), a ≤ ⊤ :=
λ a x xa, mem_univ _

lemma bot_le : ∀ (a : clo fil), ⊥ ≤ a :=
by rintros a x ⟨⟩

@[simp] lemma compl_coe {a : clo fil} : (aᶜ).1 = (a.1)ᶜ := rfl

lemma inf_compl_le_bot : ∀ (x : clo fil), x ⊓ xᶜ ≤ ⊥ :=
λ a x ⟨xa, xc⟩, xc xa

lemma top_le_sup_compl : ∀ (x : clo fil), ⊤ ≤ x ⊔ xᶜ :=
λ a, @le_of_eq (clo fil) _ _ _ (by simpa)

lemma sdiff_eq : ∀ (x y : clo fil), x \ y = x ⊓ yᶜ :=
λ _ _, rfl

end boolean_definitions

section comm_semiring_definitions

lemma mul_assoc : ∀ (a b c : clo fil), a ⊔ b ⊔ c = a ⊔ (b ⊔ c) :=
λ a b c, eq_iff.mpr sup_assoc

lemma add_assoc : ∀ (a b c : clo fil), a ⊓ b ⊓ c = a ⊓ (b ⊓ c) :=
λ a b c, eq_iff.mpr inf_assoc

lemma zero_add : ∀ (a : clo fil), ⊤ ⊓ a = a :=
λ a, eq_iff.mpr top_inf_eq

lemma add_zero : ∀ (a : clo fil), a ⊓ ⊤ = a :=
λ a, eq_iff.mpr inf_top_eq

lemma add_comm : ∀ (a b : clo fil), a ⊓ b = b ⊓ a :=
λ a b, eq_iff.mpr inf_comm

lemma one_mul : ∀ a : clo fil, ⊥ ⊔ a = a :=
λ a, eq_iff.mpr bot_sup_eq

lemma mul_one : ∀ a : clo fil, a ⊔ ⊥ = a :=
λ a, eq_iff.mpr sup_bot_eq

lemma zero_mul : ∀ a : clo fil, ⊤ ⊔ a = ⊤ :=
λ a, eq_iff.mpr top_sup_eq

lemma mul_zero : ∀ a : clo fil, a ⊔ ⊤ = ⊤ :=
λ a, eq_iff.mpr sup_top_eq

lemma left_distrib : ∀ (a b c : clo fil), a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c) :=
λ a b c, eq_iff.mpr union_inter_distrib_left

lemma right_distrib : ∀ (a b c : clo fil), (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) :=
λ a b c, eq_iff.mpr inter_union_distrib_right

lemma mul_comm : ∀ (a b : clo fil), a ⊔ b = b ⊔ a :=
λ a b, eq_iff.mpr (union_comm _ _)

end comm_semiring_definitions

end clo

open clo

def boo (fil : set X → Prop) : boolean_algebra (clo fil) :=
{sup := (⊔),
  le_sup_left := le_sup_left,
  le_sup_right := le_sup_right,
  sup_le := sup_le,
  inf := (⊓),
  inf_le_left := inf_le_left,
  inf_le_right := inf_le_right,
  le_inf := le_inf,
  le_sup_inf := le_sup_inf,
  top := ⊤,
  le_top := le_top,
  bot := ⊥,
  bot_le := bot_le,
  compl := (clo.has_compl).1,
  sdiff := (\),
  inf_compl_le_bot := inf_compl_le_bot,
  top_le_sup_compl := top_le_sup_compl,
  sdiff_eq := sdiff_eq,
  ..clo.partial_order,
}

def bosemi : comm_semiring (clo fil) :=
{ add := (⊓),
  add_assoc := add_assoc,
  zero := (⊤),
  zero_add := zero_add,
  add_zero := add_zero,
  add_comm := add_comm,
  mul := (⊔),
  mul_assoc := mul_assoc,
  one := (⊥),
  one_mul := one_mul,
  mul_one := mul_one,
  zero_mul := zero_mul,
  mul_zero := mul_zero,
  left_distrib := left_distrib,
  right_distrib := right_distrib,
  mul_comm := mul_comm}