\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Semiring
\import Function.Meta
\import Meta
\import Order.BooleanAlgebra
\import Order.HeytingAlgebra
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta

\class BooleanRing \extends PseudoCRing, BottomDistributiveLattice {
  | isBooleanRing {x : E} : x * x = x
  | <= => BooleanRing.<=
  | <=-refl => isBooleanRing
  | <=-transitive xy=x yz=y => pmap (`* _) (inv xy=x) *> *-assoc *> pmap (_ *) yz=y *> xy=x
  | <=-antisymmetric xy=x yx=y => inv xy=x *> *-comm *> yx=y
  | meet => *
  | meet-left => *-comm *> inv *-assoc *> pmap (`* _) isBooleanRing
  | meet-right => *-assoc *> pmap (_ *) isBooleanRing
  | meet-univ zx=z zy=z => inv *-assoc *> pmap (`* _) zx=z *> zy=z
  | join x y => x + y + x * y
  | join-left => ldistr *> pmap2 (+) ldistr (inv *-assoc) *> +-assoc *> pmap2 (+) isBooleanRing (pmap (_ + __ * _) isBooleanRing *> sum2 isBooleanRing) *> zro-right
  | join-right => ldistr *> pmap2 (__ + _ * __) ldistr *-comm *> +-comm *> inv +-assoc *> pmap2 (+) (pmap (`+ _) (inv *-assoc *> pmap (`* _) isBooleanRing) *> sum2 isBooleanRing) isBooleanRing *> zro-left
  | join-univ xz=x yz=y => rdistr *> pmap2 (+) (rdistr *> pmap2 (+) xz=x yz=y) (*-assoc *> pmap (_ *) yz=y)
  | bottom => 
  | bottom-univ => zro_*-left
  | ldistr>= => pmap (_ *) (inv $ ldistr *> pmap2 (+) ldistr (pmap (`* _) (inv isBooleanRing) *> *-assoc *> pmap (_ *) (inv *-assoc *> pmap (`* _) *-comm *> *-assoc) *> inv *-assoc)) *> isBooleanRing

  \default *-comm {x} {y} => inv zro-left *> pmap (`+ _) (cancel-right y $ zro-left *> cancel-left x (inv isBooleanRing *> ldistr *> pmap2 (+) rdistr rdistr *> pmap2 (__ + _ + (_ + __)) isBooleanRing isBooleanRing *> +-assoc) *> inv +-assoc) *> +-assoc *> pmap (_ +) (sum2 isBooleanRing) *> zro-right

  \lemma double=0 {x : E} : x + x = 
    => sum2 isBooleanRing

  \lemma negative=id {x : E} : negative x = x
    => cancel-left x $ negative-right *> inv double=0

  \lemma +_join {x y : E} (xy=0 : x * y = ) : x + y = x ∨ y
    => inv zro-right *> pmap (_ +) (inv xy=0)

  \func diff (x y : E) => x + x * y

  \lemma diff_<= {x y : E} : diff x y <= x
    => rdistr *> pmap2 (+) isBooleanRing (*-comm *> inv *-assoc *> pmap (`* y) isBooleanRing)

  \lemma diff_* {x y : E} : diff x y * y = 
    => rdistr *> pmap (_ +) (*-assoc *> pmap (x *) isBooleanRing) *> double=0

  \lemma diff-univ {x y z : E} (p : x <= y) (q : x * z = ) : x <= diff y z
    => ldistr *> pmap2 (+) p (pmap (x *) *-comm *> inv *-assoc *> pmap (`* y) q *> zro_*-left) *> zro-right

  \lemma diff-mono {x y x' y' : E} (p : x <= x') (q : y' <= y) : diff x y <= diff x' y'
    => diff-univ (diff_<= <=∘ p) $ <=-antisymmetric (meet-monotone <=-refl q <=∘ =_<= diff_*) bottom-univ

  \lemma diff_*_diff {x y : E} : diff x y * diff y x = 
    => <=-antisymmetric (meet-monotone <=-refl diff_<= <=∘ =_<= diff_*) bottom-univ

  \lemma +_diff {x y : E} : x + y = diff x y ∨ diff y x
    => inv zro-right *> pmap2 (+) (inv $ +-assoc *> pmap (x +) (+-comm *> +-assoc *> pmap (y +) (pmap (_ +) *-comm *> double=0) *> zro-right)) (inv diff_*_diff)

  \lemma split_<= {x y : E} (p : y <= x) : x = diff x y ∨ y
    => inv $ +-assoc *> +-assoc *> pmap (x +) (inv +-assoc *> pmap2 (+) (pmap (_ +) (<=-antisymmetric (meet-univ p <=-refl) meet-right) *> double=0) diff_* *> zro-right) *> zro-right

  \lemma split {x y : E} : x = diff x y ∨ x * y
    => split_<= meet-left *> pmap (`∨ _) (pmap (x +) (inv *-assoc *> pmap (`* y) isBooleanRing))

  \lemma diff-trans {x y z : E} : diff x z <= diff x y ∨ diff y z
    => =_<= split <=∘ join-monotone (diff-mono diff_<= <=-refl) (diff-univ meet-right $ *-assoc *> pmap (_ *) *-comm *> inv *-assoc *> pmap (`* y) diff_* *> zro_*-left)

  \lemma diff_BigJoin {l : Array E} {x : E} : diff (BigJoin l) x = BigJoin \lam j => diff (l j) x \elim l
    | nil => equation.bRing
    | a :: l => equation.bRing *> pmap (_ ∨) diff_BigJoin
} \where {
  \private \lemma sum2 {R : PseudoRing} (br : \Pi {x : R} -> x * x = x) {x : R} : x + x = 
    => inv $ R.cancel-left (x + x) $ zro-right *> inv br *> ldistr *> pmap2 (+) rdistr rdistr *> pmap2 (+) (pmap2 (+) br br) (pmap2 (+) br br)

  \type \infix  <= {R : Semigroup} (x y : R) => x * y = x
}

\class UnitalBooleanRing \extends BooleanRing, CRing, BooleanAlgebra
  | top => 
  | top-univ => ide-right
  | compl a => a + 
  | compl-meet => zro_*-right *> inv (ldistr *> pmap2 (+) isBooleanRing ide-right *> double=0)
  | compl-join => unfold $ ide-left *> pmap2 (+) (inv +-assoc *> pmap (`+ ) double=0 *> zro-left) (ldistr *> pmap2 (+) isBooleanRing ide-right *> double=0) *> zro-right
  \where {
    \open MeetSemilattice
    \open JoinSemilattice

    \use \coerce fromBooleanAlgebra (R : BooleanAlgebra) : UnitalBooleanRing R \cowith
      | zro => R.bottom
      | + a b => a ∧ compl b ∨ b ∧ compl a
      | zro-left => <=-antisymmetric (join-univ (meet-left <=∘ bottom-univ) meet-left) $ meet-univ <=-refl (top-univ <=∘ compl-join <=∘ join-univ bottom-univ <=-refl) <=∘ join-right
      | +-assoc => rewrite (R.compl_symm-diff,R.compl_symm-diff,R.meet-ldistr,R.meet-rdistr,R.meet-ldistr,R.meet-rdistr) $ <=-antisymmetric
          (join-univ (join-univ (meet-assoc =<= join-right <=∘ join-left) ((meet-assoc *> pmap (_ ∧) meet-comm *> inv meet-assoc) =<= join-left <=∘ join-right)) (join-univ (meet-comm =<= meet-assoc =<= join-left <=∘ join-left) ((pmap (_ ∧) meet-comm *> inv meet-assoc) =<= join-right <=∘ join-right)))
          (join-univ (join-univ ((inv meet-assoc *> meet-comm) =<= join-left <=∘ join-right) (inv meet-assoc =<= join-left <=∘ join-left)) (join-univ ((meet-assoc *> pmap (_ ∧) meet-comm *> inv meet-assoc) =<= join-right <=∘ join-left) ((meet-assoc *> pmap (_ ∧) meet-comm) =<= join-right <=∘ join-right)))
      | +-comm => join-comm
      | * => ∧
      | *-assoc => meet-assoc
      | ldistr => R.meet-ldistr *> pmap2 (∨)
          (later $ rewrite R.compl_meet $ inv $ R.meet-ldistr *> pmap2 (∨) (<=-antisymmetric (meet-monotone meet-left <=-refl <=∘ compl-meet) bottom-univ) meet-assoc *> R.bottom-left)
          (later $ rewrite R.compl_meet $ inv $ R.meet-ldistr *> pmap2 (∨) (<=-antisymmetric (meet-monotone meet-left <=-refl <=∘ compl-meet) bottom-univ) meet-assoc *> R.bottom-left)
      | negative x => x
      | negative-left => unfold $ <=-antisymmetric (join-univ compl-meet compl-meet) bottom-univ
      | ide => top
      | ide-left => R.top-left
      | *-comm => meet-comm
      | isBooleanRing => meet-idemp
  }

\instance HeytingBooleanRing (R : HeytingAlebra) : UnitalBooleanRing (NegatedElem R)
  => UnitalBooleanRing.fromBooleanAlgebra (HeytingBooleanAlgebra R)