------------------------------------------------------------------------
-- The Agda standard library
--
-- Some biased records for lattice-like structures. Such records are
-- often easier to construct, but are suboptimal to use more widely and
-- should be converted to the standard record definitions immediately
-- using the provided conversion functions.
------------------------------------------------------------------------

-- The contents of this module should be accessed via `Algebra.Lattice`,
-- unless you want to parameterise it via the equality relation.

{-# OPTIONS --without-K --safe #-}

open import Algebra.Core
open import Algebra.Consequences.Setoid
open import Data.Product using (proj₁; proj₂)
open import Level using (_⊔_)
open import Relation.Binary using (Rel; Setoid; IsEquivalence)

module Algebra.Lattice.Structures.Biased
  {a } {A : Set a}  -- The underlying set
  (_≈_ : Rel A )    -- The underlying equality relation
  where

open import Algebra.Definitions _≈_
open import Algebra.Lattice.Structures _≈_

private
  variable
      : Op₂ A
    ¬   : Op₁ A
      : A

------------------------------------------------------------------------
-- Lattice

-- An alternative form of `IsLattice` defined in terms of
-- `IsJoinSemilattice` and `IsMeetLattice`. This form may be desirable
-- to use when constructing a lattice object as it requires fewer
-- arguments, but is often a mistake to use as an argument as it
-- contains two, *potentially different*, proofs that the equality
-- relation _≈_ is an equivalence.

record IsLattice₂ (  : Op₂ A) : Set (a  ) where
  field
    isJoinSemilattice : IsJoinSemilattice 
    isMeetSemilattice : IsMeetSemilattice 
    absorptive        : Absorptive  

  module ML = IsMeetSemilattice isMeetSemilattice
  module JL = IsJoinSemilattice isJoinSemilattice

  isLattice₂ : IsLattice  
  isLattice₂ = record
    { isEquivalence = ML.isEquivalence
    ; ∨-comm        = JL.comm
    ; ∨-assoc       = JL.assoc
    ; ∨-cong        = JL.∨-cong
    ; ∧-comm        = ML.comm
    ; ∧-assoc       = ML.assoc
    ; ∧-cong        = ML.∧-cong
    ; absorptive    = absorptive
    }

open IsLattice₂ public using (isLattice₂)

------------------------------------------------------------------------
-- DistributiveLattice

-- A version of distributive lattice that is biased towards the (r)ight
-- distributivity law for (j)oin and (m)eet.
record IsDistributiveLatticeʳʲᵐ (  : Op₂ A) : Set (a  ) where
  field
    isLattice    : IsLattice  
    ∨-distribʳ-∧ :  DistributesOverʳ 

  open IsLattice isLattice public

  setoid : Setoid a 
  setoid = record { isEquivalence = isEquivalence }

  ∨-distrib-∧  = comm+distrʳ⇒distr setoid ∧-cong ∨-comm ∨-distribʳ-∧
  ∧-distribˡ-∨ = distrib+absorbs⇒distribˡ setoid ∧-cong ∧-assoc ∨-comm ∧-absorbs-∨ ∨-absorbs-∧ ∨-distrib-∧
  ∧-distrib-∨  = comm+distrˡ⇒distr setoid ∨-cong ∧-comm ∧-distribˡ-∨

  isDistributiveLatticeʳʲᵐ : IsDistributiveLattice  
  isDistributiveLatticeʳʲᵐ = record
    { isLattice   = isLattice
    ; ∨-distrib-∧ = ∨-distrib-∧
    ; ∧-distrib-∨ = ∧-distrib-∨
    }

open IsDistributiveLatticeʳʲᵐ public using (isDistributiveLatticeʳʲᵐ)

------------------------------------------------------------------------
-- BooleanAlgebra

-- A (r)ight biased version of a boolean algebra.
record IsBooleanAlgebraʳ
         (  : Op₂ A) (¬ : Op₁ A) (  : A) : Set (a  ) where
  field
    isDistributiveLattice : IsDistributiveLattice  
    ∨-complementʳ         : RightInverse  ¬ 
    ∧-complementʳ         : RightInverse  ¬ 
    ¬-cong                : Congruent₁ ¬

  open IsDistributiveLattice isDistributiveLattice public

  setoid : Setoid a 
  setoid = record { isEquivalence = isEquivalence }

  isBooleanAlgebraʳ : IsBooleanAlgebra    ¬  
  isBooleanAlgebraʳ = record
    { isDistributiveLattice = isDistributiveLattice
    ; ∨-complement          = comm+invʳ⇒inv setoid ∨-comm ∨-complementʳ
    ; ∧-complement          = comm+invʳ⇒inv setoid ∧-comm ∧-complementʳ
    ; ¬-cong                = ¬-cong
    }

open IsBooleanAlgebraʳ public using (isBooleanAlgebraʳ)