------------------------------------------------------------------------
-- Lexicographic products of binary relations
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

-- The definition of lexicographic product used here is suitable if
-- the left-hand relation is a (non-strict) partial order.

module Relation.Binary.Product.NonStrictLex where

open import Data.Product
open import Data.Sum
open import Level
open import Relation.Binary
open import Relation.Binary.Consequences
import Relation.Binary.NonStrictToStrict as Conv
open import Relation.Binary.Product.Pointwise as Pointwise
  using (_×-Rel_)
import Relation.Binary.Product.StrictLex as Strict

private
 module Dummy {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where

  ×-Lex : (_≈₁_ _≤₁_ : Rel A₁ ℓ₁)  (_≤₂_ : Rel A₂ ℓ₂) 
          Rel (A₁ × A₂) _
  ×-Lex _≈₁_ _≤₁_ _≤₂_ = Strict.×-Lex _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_

  -- Some properties which are preserved by ×-Lex (under certain
  -- assumptions).

  ×-reflexive :  _≈₁_ _≤₁_ {_≈₂_} _≤₂_ 
                _≈₂_  _≤₂_  (_≈₁_ ×-Rel _≈₂_)  (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-reflexive _≈₁_ _≤₁_ _≤₂_ refl₂ {x} {y} =
    Strict.×-reflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_ refl₂ {x} {y}

  ×-transitive :  {_≈₁_ _≤₁_}  IsPartialOrder _≈₁_ _≤₁_ 
                  {_≤₂_}  Transitive _≤₂_ 
                 Transitive (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-transitive {_≈₁_ = _≈₁_} {_≤₁_ = _≤₁_} po₁ {_≤₂_ = _≤₂_} trans₂
               {x} {y} {z} =
    Strict.×-transitive
      {_<₁_ = Conv._<_ _≈₁_ _≤₁_}
      isEquivalence (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
      (Conv.trans _ _ po₁)
      {_≤₂_ = _≤₂_} trans₂ {x} {y} {z}
    where open IsPartialOrder po₁

  ×-antisymmetric :
     {_≈₁_ _≤₁_}  IsPartialOrder _≈₁_ _≤₁_ 
     {_≈₂_ _≤₂_}  Antisymmetric _≈₂_ _≤₂_ 
    Antisymmetric (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-antisymmetric {_≈₁_ = _≈₁_} {_≤₁_ = _≤₁_}
                  po₁ {_≤₂_ = _≤₂_} antisym₂ {x} {y} =
    Strict.×-antisymmetric {_<₁_ = Conv._<_ _≈₁_ _≤₁_}
                           ≈-sym₁ irrefl₁ asym₁
                           {_≤₂_ = _≤₂_} antisym₂ {x} {y}
    where
    open IsPartialOrder po₁
    open Eq renaming (refl to ≈-refl₁; sym to ≈-sym₁)

    irrefl₁ : Irreflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
    irrefl₁ = Conv.irrefl _≈₁_ _≤₁_

    asym₁ : Asymmetric (Conv._<_ _≈₁_ _≤₁_)
    asym₁ = trans∧irr⟶asym {_≈_ = _≈₁_}
                           ≈-refl₁ (Conv.trans _ _ po₁) irrefl₁

  ×-≈-respects₂ :
     {_≈₁_ _≤₁_}  IsEquivalence _≈₁_  _≤₁_ Respects₂ _≈₁_ 
     {_≈₂_ _≤₂_ : Rel A₂ ℓ₂}  _≤₂_ Respects₂ _≈₂_ 
    (×-Lex _≈₁_ _≤₁_ _≤₂_) Respects₂ (_≈₁_ ×-Rel _≈₂_)
  ×-≈-respects₂ eq₁ resp₁ resp₂ =
    Strict.×-≈-respects₂ eq₁ (Conv.<-resp-≈ _ _ eq₁ resp₁) resp₂

  ×-decidable :  {_≈₁_ _≤₁_}  Decidable _≈₁_  Decidable _≤₁_ 
                 {_≤₂_}  Decidable _≤₂_ 
                Decidable (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-decidable dec-≈₁ dec-≤₁ dec-≤₂ =
    Strict.×-decidable dec-≈₁ (Conv.decidable _ _ dec-≈₁ dec-≤₁)
                       dec-≤₂

  ×-total :  {_≈₁_ _≤₁_}  Symmetric _≈₁_  Decidable _≈₁_ 
                            Antisymmetric _≈₁_ _≤₁_  Total _≤₁_ 
             {_≤₂_}  Total _≤₂_ 
            Total (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-total {_≈₁_ = _≈₁_} {_≤₁_ = _≤₁_} sym₁ dec₁ antisym₁ total₁
                        {_≤₂_ = _≤₂_} total₂ = total
    where
    tri₁ : Trichotomous _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
    tri₁ = Conv.trichotomous _ _ sym₁ dec₁ antisym₁ total₁

    total : Total (×-Lex _≈₁_ _≤₁_ _≤₂_)
    total x y with tri₁ (proj₁ x) (proj₁ y)
    ... | tri< x₁<y₁ x₁≉y₁ x₁≯y₁ = inj₁ (inj₁ x₁<y₁)
    ... | tri> x₁≮y₁ x₁≉y₁ x₁>y₁ = inj₂ (inj₁ x₁>y₁)
    ... | tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁ with total₂ (proj₂ x) (proj₂ y)
    ...   | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁ , x₂≤y₂))
    ...   | inj₂ x₂≥y₂ = inj₂ (inj₂ (sym₁ x₁≈y₁ , x₂≥y₂))

  -- Some collections of properties which are preserved by ×-Lex
  -- (under certain assumptions).

  _×-isPartialOrder_ :
     {_≈₁_ _≤₁_}  IsPartialOrder _≈₁_ _≤₁_ 
     {_≈₂_ _≤₂_}  IsPartialOrder _≈₂_ _≤₂_ 
    IsPartialOrder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  _×-isPartialOrder_ {_≈₁_ = _≈₁_} {_≤₁_ = _≤₁_} po₁
                     {_≤₂_ = _≤₂_} po₂ = record
    { isPreorder = record
        { isEquivalence = Pointwise._×-isEquivalence_
                            (isEquivalence po₁)
                            (isEquivalence po₂)
        ; reflexive     = λ {x y} 
                          ×-reflexive _≈₁_ _≤₁_ _≤₂_ (reflexive po₂)
                                      {x} {y}
        ; trans         = λ {x y z} 
                          ×-transitive po₁ {_≤₂_ = _≤₂_} (trans po₂)
                                       {x} {y} {z}
        }
    ; antisym = λ {x y} 
                ×-antisymmetric {_≤₁_ = _≤₁_} po₁
                                {_≤₂_ = _≤₂_} (antisym po₂) {x} {y}
    }
    where open IsPartialOrder

  ×-isTotalOrder :
     {_≈₁_ _≤₁_}  Decidable _≈₁_  IsTotalOrder _≈₁_ _≤₁_ 
     {_≈₂_ _≤₂_}  IsTotalOrder _≈₂_ _≤₂_ 
    IsTotalOrder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-isTotalOrder {_≤₁_ = _≤₁_} ≈₁-dec to₁ {_≤₂_ = _≤₂_} to₂ = record
    { isPartialOrder = isPartialOrder to₁ ×-isPartialOrder
                       isPartialOrder to₂
    ; total          = ×-total {_≤₁_ = _≤₁_} (Eq.sym to₁) ≈₁-dec
                                             (antisym to₁) (total to₁)
                               {_≤₂_ = _≤₂_} (total to₂)
    }
    where open IsTotalOrder

  _×-isDecTotalOrder_ :
     {_≈₁_ _≤₁_}  IsDecTotalOrder _≈₁_ _≤₁_ 
     {_≈₂_ _≤₂_}  IsDecTotalOrder _≈₂_ _≤₂_ 
    IsDecTotalOrder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  _×-isDecTotalOrder_ {_≤₁_ = _≤₁_} to₁ {_≤₂_ = _≤₂_} to₂ = record
    { isTotalOrder = ×-isTotalOrder (_≟_ to₁)
                                    (isTotalOrder to₁)
                                    (isTotalOrder to₂)
    ; _≟_          = Pointwise._×-decidable_ (_≟_ to₁) (_≟_ to₂)
    ; _≤?_         = ×-decidable (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
    }
    where open IsDecTotalOrder

open Dummy public

-- "Packages" (e.g. posets) can also be combined.

_×-poset_ :
   {p₁ p₂ p₃ p₄}  Poset p₁ p₂ _  Poset p₃ p₄ _  Poset _ _ _
p₁ ×-poset p₂ = record
  { isPartialOrder = isPartialOrder p₁ ×-isPartialOrder
                     isPartialOrder p₂
  } where open Poset

_×-totalOrder_ :
   {d₁ d₂ t₃ t₄} 
  DecTotalOrder d₁ d₂ _  TotalOrder t₃ t₄ _  TotalOrder _ _ _
t₁ ×-totalOrder t₂ = record
  { isTotalOrder = ×-isTotalOrder T₁._≟_ T₁.isTotalOrder T₂.isTotalOrder
  }
  where
  module T₁ = DecTotalOrder t₁
  module T₂ =    TotalOrder t₂

_×-decTotalOrder_ :
   {d₁ d₂ d₃ d₄} 
  DecTotalOrder d₁ d₂ _  DecTotalOrder d₃ d₄ _  DecTotalOrder _ _ _
t₁ ×-decTotalOrder t₂ = record
  { isDecTotalOrder = isDecTotalOrder t₁ ×-isDecTotalOrder
                      isDecTotalOrder t₂
  } where open DecTotalOrder