------------------------------------------------------------------------
-- A bunch of properties
------------------------------------------------------------------------

module Data.Bool.Properties where

open import Data.Bool as Bool
open import Data.Fin
open import Data.Function
open import Algebra
open import Algebra.Structures
import Algebra.RingSolver.Simple as Solver
import Algebra.RingSolver.AlmostCommutativeRing as ACR
open import Relation.Nullary using (_⇔_)
open import Relation.Binary.PropositionalEquality
  hiding (proof-irrelevance)
open ≡-Reasoning
import Algebra.FunctionProperties as P; open P _≡_
open import Data.Product
open import Data.Sum
open import Data.Empty

------------------------------------------------------------------------
-- Duality

-- Can we take advantage of duality in some (nice) way?

------------------------------------------------------------------------
-- (Bool, ∨, ∧, false, true) forms a commutative semiring

private

  ∨-assoc : Associative _∨_
  ∨-assoc true  y z = refl
  ∨-assoc false y z = refl

  ∧-assoc : Associative _∧_
  ∧-assoc true  y z = refl
  ∧-assoc false y z = refl

  ∨-comm : Commutative _∨_
  ∨-comm true  true  = refl
  ∨-comm true  false = refl
  ∨-comm false true  = refl
  ∨-comm false false = refl

  ∧-comm : Commutative _∧_
  ∧-comm true  true  = refl
  ∧-comm true  false = refl
  ∧-comm false true  = refl
  ∧-comm false false = refl

  ∨-identity : Identity false _∨_
  ∨-identity =  _  refl) ,  x  ∨-comm x false)

  ∧-identity : Identity true _∧_
  ∧-identity =  _  refl) ,  x  ∧-comm x true)

  zero-∧ : Zero false _∧_
  zero-∧ =  _  refl) ,  x  ∧-comm x false)

  distrib-∧-∨ : _∧_ DistributesOver _∨_
  distrib-∧-∨ = distˡ , distʳ
    where
    distˡ : _∧_ DistributesOverˡ _∨_
    distˡ true  y z = refl
    distˡ false y z = refl

    distʳ : _∧_ DistributesOverʳ _∨_
    distʳ x y z =
                      begin
       (y  z)  x
                      ≡⟨ ∧-comm (y  z) x 
       x  (y  z)
                      ≡⟨ distˡ x y z 
       x  y  x  z
                      ≡⟨ cong₂ _∨_ (∧-comm x y) (∧-comm x z) 
       y  x  z  x
                      

isCommutativeSemiring-∨-∧
  : IsCommutativeSemiring _≡_ _∨_ _∧_ false true
isCommutativeSemiring-∨-∧ = record
  { isSemiring = record
    { isSemiringWithoutAnnihilatingZero = record
      { +-isCommutativeMonoid = record
        { isMonoid = record
          { isSemigroup = record
            { isEquivalence = isEquivalence
            ; assoc         = ∨-assoc
            ; ∙-cong        = cong₂ _∨_
            }
          ; identity = ∨-identity
          }
        ; comm = ∨-comm
        }
      ; *-isMonoid = record
        { isSemigroup = record
          { isEquivalence = isEquivalence
          ; assoc         = ∧-assoc
          ; ∙-cong        = cong₂ _∧_
          }
        ; identity = ∧-identity
        }
      ; distrib = distrib-∧-∨
      }
    ; zero = zero-∧
    }
  ; *-comm = ∧-comm
  }

commutativeSemiring-∨-∧ : CommutativeSemiring
commutativeSemiring-∨-∧ = record
  { _+_                   = _∨_
  ; _*_                   = _∧_
  ; 0#                    = false
  ; 1#                    = true
  ; isCommutativeSemiring = isCommutativeSemiring-∨-∧
  }

module RingSolver =
  Solver (ACR.fromCommutativeSemiring commutativeSemiring-∨-∧)

------------------------------------------------------------------------
-- (Bool, ∧, ∨, true, false) forms a commutative semiring

private

  zero-∨ : Zero true _∨_
  zero-∨ =  _  refl) ,  x  ∨-comm x true)

  distrib-∨-∧ : _∨_ DistributesOver _∧_
  distrib-∨-∧ = distˡ , distʳ
    where
    distˡ : _∨_ DistributesOverˡ _∧_
    distˡ true  y z = refl
    distˡ false y z = refl

    distʳ : _∨_ DistributesOverʳ _∧_
    distʳ x y z =
                          begin
       (y  z)  x
                          ≡⟨ ∨-comm (y  z) x 
       x  (y  z)
                          ≡⟨ distˡ x y z 
       (x  y)  (x  z)
                          ≡⟨ cong₂ _∧_ (∨-comm x y) (∨-comm x z) 
       (y  x)  (z  x)
                          

isCommutativeSemiring-∧-∨
  : IsCommutativeSemiring _≡_ _∧_ _∨_ true false
isCommutativeSemiring-∧-∨ = record
  { isSemiring = record
    { isSemiringWithoutAnnihilatingZero = record
      { +-isCommutativeMonoid = record
        { isMonoid = record
          { isSemigroup = record
            { isEquivalence = isEquivalence
            ; assoc         = ∧-assoc
            ; ∙-cong        = cong₂ _∧_
            }
          ; identity = ∧-identity
          }
        ; comm = ∧-comm
        }
      ; *-isMonoid = record
        { isSemigroup = record
          { isEquivalence = isEquivalence
          ; assoc         = ∨-assoc
          ; ∙-cong        = cong₂ _∨_
          }
        ; identity = ∨-identity
        }
      ; distrib = distrib-∨-∧
      }
    ; zero = zero-∨
    }
  ; *-comm = ∨-comm
  }

commutativeSemiring-∧-∨ : CommutativeSemiring
commutativeSemiring-∧-∨ = record
  { _+_                   = _∧_
  ; _*_                   = _∨_
  ; 0#                    = true
  ; 1#                    = false
  ; isCommutativeSemiring = isCommutativeSemiring-∧-∨
  }

------------------------------------------------------------------------
-- (Bool, ∨, ∧, not, true, false) is a boolean algebra

private

  absorptive : Absorptive _∨_ _∧_
  absorptive = abs-∨-∧ , abs-∧-∨
    where
    abs-∨-∧ : _∨_ Absorbs _∧_
    abs-∨-∧ true  y = refl
    abs-∨-∧ false y = refl

    abs-∧-∨ : _∧_ Absorbs _∨_
    abs-∧-∨ true  y = refl
    abs-∧-∨ false y = refl

  not-∧-inverse : Inverse false not _∧_
  not-∧-inverse =
    ¬x∧x≡⊥ ,  x  ∧-comm x (not x)  trans  ¬x∧x≡⊥ x)
    where
    ¬x∧x≡⊥ : LeftInverse false not _∧_
    ¬x∧x≡⊥ false = refl
    ¬x∧x≡⊥ true  = refl

  not-∨-inverse : Inverse true not _∨_
  not-∨-inverse =
    ¬x∨x≡⊤ ,  x  ∨-comm x (not x)  trans  ¬x∨x≡⊤ x)
    where
    ¬x∨x≡⊤ : LeftInverse true not _∨_
    ¬x∨x≡⊤ false = refl
    ¬x∨x≡⊤ true  = refl

isBooleanAlgebra : IsBooleanAlgebra _≡_ _∨_ _∧_ not true false
isBooleanAlgebra = record
  { isDistributiveLattice = record
      { isLattice = record
          { isEquivalence = isEquivalence
          ; ∨-comm        = ∨-comm
          ; ∨-assoc       = ∨-assoc
          ; ∨-cong        = cong₂ _∨_
          ; ∧-comm        = ∧-comm
          ; ∧-assoc       = ∧-assoc
          ; ∧-cong        = cong₂ _∧_
          ; absorptive    = absorptive
          }
      ; ∨-∧-distribʳ = proj₂ distrib-∨-∧
      }
  ; ∨-complementʳ = proj₂ not-∨-inverse
  ; ∧-complementʳ = proj₂ not-∧-inverse
  ; ¬-cong        = cong not
  }

booleanAlgebra : BooleanAlgebra
booleanAlgebra = record
  { _∨_              = _∨_
  ; _∧_              = _∧_
  ; ¬_               = not
  ;                 = true
  ;                 = false
  ; isBooleanAlgebra = isBooleanAlgebra
  }

------------------------------------------------------------------------
-- (Bool, xor, ∧, id, false, true) forms a commutative ring

private

  xor-is-ok :  x y  x xor y  (x  y)  not (x  y)
  xor-is-ok true  y = refl
  xor-is-ok false y = sym $ proj₂ ∧-identity _

commutativeRing-xor-∧ : CommutativeRing
commutativeRing-xor-∧ = commutativeRing
  where
  import Algebra.Props.BooleanAlgebra as BA
  open BA booleanAlgebra
  open XorRing _xor_ xor-is-ok

module XorRingSolver =
  Solver (ACR.fromCommutativeRing commutativeRing-xor-∧)

------------------------------------------------------------------------
-- Miscellaneous other properties

not-involutive : Involutive not
not-involutive true  = refl
not-involutive false = refl

not-¬ :  {x y}  x  y  x  not y
not-¬ {true}  refl ()
not-¬ {false} refl ()

¬-not :  {x y}  x  y  x  not y
¬-not {true}  {true}  x≢y = ⊥-elim (x≢y refl)
¬-not {true}  {false} _   = refl
¬-not {false} {true}  _   = refl
¬-not {false} {false} x≢y = ⊥-elim (x≢y refl)

⇔→≡ : {b₁ b₂ b : Bool}  b₁  b  b₂  b  b₁  b₂
⇔→≡ {true } {true }         hyp = refl
⇔→≡ {true } {false} {true } hyp = sym (proj₁ hyp refl)
⇔→≡ {true } {false} {false} hyp = proj₂ hyp refl
⇔→≡ {false} {true } {true } hyp = proj₂ hyp refl
⇔→≡ {false} {true } {false} hyp = sym (proj₁ hyp refl)
⇔→≡ {false} {false}         hyp = refl

T-≡ :  {b}  T b  b  true
T-≡ {false} = ((λ ())     , λ ())
T-≡ {true}  = (const refl , const _)

T-∧ :  {b₁ b₂}  T (b₁  b₂)  (T b₁ × T b₂)
T-∧ {true}  {true}  = (const (_ , _) , const _)
T-∧ {true}  {false} = ((λ ()) , proj₂)
T-∧ {false} {_}     = ((λ ()) , proj₁)

T-∨ :  {b₁ b₂}  T (b₁  b₂)  (T b₁  T b₂)
T-∨ {true}  {b₂}    = (inj₁ , const _)
T-∨ {false} {true}  = (inj₂ , const _)
T-∨ {false} {false} = (inj₁ , [ id , id ])

proof-irrelevance :  {b} (p q : T b)  p  q
proof-irrelevance {true}  _  _  = refl
proof-irrelevance {false} () ()