import Builtin

import public Builtin

import Algebra.Equivalence

import public Algebra.Equivalence
import public Algebra.Monoid

--
-- Values
--

--
-- Relation
--

--
-- Operations
--

public export
[BooleanDisjMagma] Magma Boolean where
  False <> False = False
  _     <> _     = True

public export

disj False False = False
disj _     _     = True

disj = (<>) @{BooleanDisjMagma}
proofDisjLeftIdentity : (a : Boolean) -> False `disj` a = a
proofDisjLeftIdentity False = Refl
proofDisjLeftIdentity True  = Refl
proofDisjRightIdentity : (a : Boolean) -> a `disj` False = a
proofDisjRightIdentity False = Refl
proofDisjRightIdentity True  = Refl

proofDisjLeftIdentity : (a : Boolean) -> False `disj` a = a
proofDisjLeftIdentity False = Refl
proofDisjLeftIdentity True  = Refl

public export
[BooleanDisjSemigroup] Semigroup Boolean using BooleanDisjMagma where
  proofAssociativity False b c =
    rewrite proofDisjLeftIdentity b in
    rewrite proofDisjLeftIdentity (b `disj` c) in
    Refl
  proofAssociativity True b c = Refl

proofDisjRightIdentity : (a : Boolean) -> a `disj` False = a
proofDisjRightIdentity False = Refl
proofDisjRightIdentity True  = Refl

public export
[BooleanDisjMonoid] Monoid Boolean using BooleanDisjSemigroup where
  id = False
  proofLeftIdentity = proofDisjLeftIdentity
  proofRightIdentity = proofDisjRightIdentity

proofDisjAssociative : (a, b, c : Boolean) -> a `disj` (b `disj` c) = (a `disj` b) `disj` c
proofDisjAssociative False b c =
  rewrite proofDisjLeftIdentity b in
  rewrite proofDisjLeftIdentity (b `disj` c) in
  Refl
proofDisjAssociative True b c = Refl

public export
[BooleanConjMagma] Magma Boolean where
  True <> True = True
  _    <> _    = False

conj True True = True
conj _    _    = False

conj = (<>) @{BooleanConjMagma}
proofConjLeftIdentity : (a : Boolean) -> True `conj` a = a
proofConjLeftIdentity False = Refl
proofConjLeftIdentity True  = Refl
proofConjRightIdentity : (a : Boolean) -> a `conj` True = a
proofConjRightIdentity False = Refl
proofConjRightIdentity True  = Refl

proofConjLeftIdentity : (a : Boolean) -> True `conj` a = a
proofConjLeftIdentity False = Refl
proofConjLeftIdentity True  = Refl

public export
[BooleanConjSemigroup] Semigroup Boolean using BooleanConjMagma where
  proofAssociativity False b c = Refl
  proofAssociativity True b c =
    rewrite proofConjLeftIdentity b in
    rewrite proofConjLeftIdentity (b `conj` c) in
    Refl

proofConjRightIdentity : (a : Boolean) -> a `conj` True = a
proofConjRightIdentity False = Refl
proofConjRightIdentity True  = Refl

public export
[BooleanConjMonoid] Monoid Boolean using BooleanConjSemigroup where
  id = True
  proofLeftIdentity  = proofConjLeftIdentity
  proofRightIdentity = proofConjRightIdentity

  Refl
proofConjAssociative : (a, b, c : Boolean) -> a `conj` (b `conj` c) = (a `conj` b) `conj` c
proofConjAssociative False b c = Refl
proofConjAssociative True b c =
  rewrite proofConjLeftIdentity b in
  rewrite proofConjLeftIdentity (b `conj` c) in