Skip to content

Relation.Binary.Construct.NaturalOrder.Right

------------------------------------------------------------------------
-- The Agda standard library
--
-- Conversion of binary operators to binary relations via the right
-- natural order.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra.Core using (Opβ‚‚)
open import Data.Product.Base using (_,_; _Γ—_)
open import Data.Sum.Base using (inj₁; injβ‚‚; map)
open import Relation.Binary.Core using (Rel; _β‡’_)
open import Relation.Binary.Bundles
  using (Preorder; Poset; DecPoset; TotalOrder; DecTotalOrder)
open import Relation.Binary.Structures
  using (IsEquivalence; IsPreorder; IsPartialOrder; IsDecPartialOrder
        ; IsTotalOrder; IsDecTotalOrder)
open import Relation.Binary.Definitions
  using (Symmetric; Transitive; Reflexive; Antisymmetric; Total; _RespectsΚ³_
        ; _RespectsΛ‘_; _Respectsβ‚‚_; Decidable)

open import Relation.Nullary.Negation using (Β¬_)
import Relation.Binary.Reasoning.Setoid as β‰ˆ-Reasoning

module Relation.Binary.Construct.NaturalOrder.Right
  {a β„“} {A : Set a} (_β‰ˆ_ : Rel A β„“) (_βˆ™_ : Opβ‚‚ A) where

open import Algebra.Definitions _β‰ˆ_
open import Algebra.Structures _β‰ˆ_
open import Algebra.Lattice.Structures _β‰ˆ_

------------------------------------------------------------------------
-- Definition

infix 4 _≀_

_≀_ : Rel A β„“
x ≀ y = x β‰ˆ (y βˆ™ x)

------------------------------------------------------------------------
-- Relational properties

reflexive : IsMagma _βˆ™_ β†’ Idempotent _βˆ™_ β†’ _β‰ˆ_ β‡’ _≀_
reflexive magma idem {x} {y} xβ‰ˆy = begin
  x     β‰ˆβŸ¨ sym (idem x) ⟩
  x βˆ™ x β‰ˆβŸ¨ βˆ™-cong xβ‰ˆy refl ⟩
  y βˆ™ x ∎
  where open IsMagma magma; open β‰ˆ-Reasoning setoid

refl : Symmetric _β‰ˆ_ β†’ Idempotent _βˆ™_ β†’ Reflexive _≀_
refl sym idem {x} = sym (idem x)

antisym : IsEquivalence _β‰ˆ_ β†’ Commutative _βˆ™_ β†’ Antisymmetric _β‰ˆ_ _≀_
antisym isEq comm {x} {y} x≀y y≀x = begin
  x     β‰ˆβŸ¨  x≀y ⟩
  y βˆ™ x β‰ˆβŸ¨  comm y x ⟩
  x βˆ™ y β‰ˆβŸ¨ y≀x ⟨
  y     ∎
  where open β‰ˆ-Reasoning (record { isEquivalence = isEq })

total : Symmetric _β‰ˆ_ β†’ Transitive _β‰ˆ_ β†’ Selective _βˆ™_ β†’ Commutative _βˆ™_ β†’ Total _≀_
total sym trans sel comm x y =
  map (Ξ» xβˆ™yβ‰ˆx β†’ trans (sym xβˆ™yβ‰ˆx) (comm x y)) sym (sel x y)

trans : IsSemigroup _βˆ™_ β†’ Transitive _≀_
trans semi {x} {y} {z} x≀y y≀z = begin
  x           β‰ˆβŸ¨ x≀y ⟩
  y βˆ™ x       β‰ˆβŸ¨ βˆ™-cong y≀z S.refl ⟩
  (z βˆ™ y) βˆ™ x β‰ˆβŸ¨ assoc z y x ⟩
  z βˆ™ (y βˆ™ x) β‰ˆβŸ¨ βˆ™-cong S.refl (sym x≀y) ⟩
  z βˆ™ x       ∎
  where open module S = IsSemigroup semi; open β‰ˆ-Reasoning S.setoid

respΚ³ : IsMagma _βˆ™_ β†’ _≀_ RespectsΚ³ _β‰ˆ_
respΚ³ magma {x} {y} {z} yβ‰ˆz x≀y = begin
  x     β‰ˆβŸ¨ x≀y ⟩
  y βˆ™ x β‰ˆβŸ¨ βˆ™-cong yβ‰ˆz M.refl ⟩
  z βˆ™ x ∎
  where open module M = IsMagma magma; open β‰ˆ-Reasoning M.setoid

respΛ‘ : IsMagma _βˆ™_ β†’ _≀_ RespectsΛ‘ _β‰ˆ_
respΛ‘ magma {x} {y} {z} yβ‰ˆz y≀x = begin
  z     β‰ˆβŸ¨ sym yβ‰ˆz ⟩
  y     β‰ˆβŸ¨ y≀x ⟩
  x βˆ™ y β‰ˆβŸ¨ βˆ™-cong M.refl yβ‰ˆz ⟩
  x βˆ™ z ∎
  where open module M = IsMagma magma; open β‰ˆ-Reasoning M.setoid

respβ‚‚ : IsMagma _βˆ™_ β†’  _≀_ Respectsβ‚‚ _β‰ˆ_
respβ‚‚ magma = respΚ³ magma , respΛ‘ magma

dec : Decidable _β‰ˆ_ β†’ Decidable _≀_
dec _β‰Ÿ_ x y = x β‰Ÿ (y βˆ™ x)

------------------------------------------------------------------------
-- Structures

isPreorder : IsBand _βˆ™_ β†’ IsPreorder _β‰ˆ_ _≀_
isPreorder band = record
  { isEquivalence = isEquivalence
  ; reflexive     = reflexive isMagma idem
  ; trans         = trans isSemigroup
  }
  where open IsBand band hiding (reflexive; trans)

isPartialOrder : IsSemilattice _βˆ™_ β†’ IsPartialOrder _β‰ˆ_ _≀_
isPartialOrder semilattice = record
  { isPreorder = isPreorder isBand
  ; antisym    = antisym isEquivalence comm
  }
  where open IsSemilattice semilattice

isDecPartialOrder : IsSemilattice _βˆ™_ β†’ Decidable _β‰ˆ_ β†’
                    IsDecPartialOrder _β‰ˆ_ _≀_
isDecPartialOrder semilattice _β‰Ÿ_ = record
  { isPartialOrder = isPartialOrder semilattice
  ; _β‰Ÿ_            = _β‰Ÿ_
  ; _≀?_           = dec _β‰Ÿ_
  }

isTotalOrder : IsSemilattice _βˆ™_ β†’ Selective _βˆ™_ β†’ IsTotalOrder _β‰ˆ_ _≀_
isTotalOrder latt sel  = record
  { isPartialOrder = isPartialOrder latt
  ; total          = total sym S.trans sel comm
  }
  where open module S = IsSemilattice latt

isDecTotalOrder : IsSemilattice _βˆ™_ β†’ Selective _βˆ™_ β†’
                  Decidable _β‰ˆ_ β†’ IsDecTotalOrder _β‰ˆ_ _≀_
isDecTotalOrder latt sel _β‰Ÿ_ = record
  { isTotalOrder = isTotalOrder latt sel
  ; _β‰Ÿ_          = _β‰Ÿ_
  ; _≀?_         = dec _β‰Ÿ_
  }

------------------------------------------------------------------------
-- Bundles

preorder : IsBand _βˆ™_ β†’ Preorder a β„“ β„“
preorder band = record
  { isPreorder = isPreorder band
  }

poset : IsSemilattice _βˆ™_ β†’ Poset a β„“ β„“
poset latt = record
  { isPartialOrder = isPartialOrder latt
  }

decPoset : IsSemilattice _βˆ™_ β†’ Decidable _β‰ˆ_ β†’ DecPoset a β„“ β„“
decPoset latt dec = record
  { isDecPartialOrder = isDecPartialOrder latt dec
  }

totalOrder : IsSemilattice _βˆ™_ β†’ Selective _βˆ™_ β†’ TotalOrder a β„“ β„“
totalOrder latt sel = record
  { isTotalOrder = isTotalOrder latt sel
  }

decTotalOrder : IsSemilattice _βˆ™_ β†’ Selective _βˆ™_ β†’
                Decidable _β‰ˆ_ β†’ DecTotalOrder a β„“ β„“
decTotalOrder latt sel dec = record
  { isDecTotalOrder = isDecTotalOrder latt sel dec
  }