------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic products of binary relations
------------------------------------------------------------------------

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

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

module Data.Product.Relation.Binary.Lex.NonStrict where

open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Sum using (inj₁; inj₂)
open import Relation.Binary
open import Relation.Binary.Consequences
import Relation.Binary.Construct.NonStrictToStrict as Conv
open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
  using (Pointwise)
import Data.Product.Relation.Binary.Lex.Strict as Strict

module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where

------------------------------------------------------------------------
-- A lexicographic ordering over products

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

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

  ×-reflexive : ∀ _≈₁_ _≤₁_ {_≈₂_} _≤₂_ →
                _≈₂_ ⇒ _≤₂_ →
                (Pointwise _≈₁_ _≈₂_) ⇒ (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-reflexive _≈₁_ _≤₁_ _≤₂_ refl₂ =
    Strict.×-reflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_ refl₂

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

  ×-antisymmetric :
    ∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
    ∀ {_≈₂_ _≤₂_} → Antisymmetric _≈₂_ _≤₂_ →
    Antisymmetric (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-antisymmetric {_≈₁_} {_≤₁_}
                  po₁ {_≤₂_ = _≤₂_} antisym₂ =
    Strict.×-antisymmetric {_<₁_ = Conv._<_ _≈₁_ _≤₁_}
                           ≈-sym₁ irrefl₁ asym₁
                           {_≤₂_ = _≤₂_} antisym₂
    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₂ (Pointwise _≈₁_ _≈₂_)
  ×-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 (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-isPartialOrder {_≈₁_} {_≤₁_} po₁
                     {_≤₂_ = _≤₂_} po₂ = record
    { isPreorder = record
        { isEquivalence = Pointwise.×-isEquivalence
                            (isEquivalence po₁)
                            (isEquivalence po₂)
        ; reflexive     = ×-reflexive _≈₁_ _≤₁_ _≤₂_ (reflexive po₂)
        ; trans         = ×-transitive po₁ {_≤₂_ = _≤₂_} (trans po₂)
        }
    ; antisym = ×-antisymmetric {_≤₁_ = _≤₁_} po₁
                                {_≤₂_ = _≤₂_} (antisym po₂)
    }
    where open IsPartialOrder

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

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

------------------------------------------------------------------------
-- "Bundles" can also be combined.

module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} where

  ×-poset : Poset ℓ₁ ℓ₂ _ → Poset ℓ₃ ℓ₄ _ → Poset _ _ _
  ×-poset p₁ p₂ = record
    { isPartialOrder = ×-isPartialOrder
                         (isPartialOrder p₁) (isPartialOrder p₂)
    } where open Poset

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

  ×-decTotalOrder : DecTotalOrder ℓ₁ ℓ₂ _ → DecTotalOrder ℓ₃ ℓ₄ _ →
                    DecTotalOrder _ _ _
  ×-decTotalOrder t₁ t₂ = record
    { isDecTotalOrder = ×-isDecTotalOrder
        (isDecTotalOrder t₁) (isDecTotalOrder t₂)
    } where open DecTotalOrder

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

_×-isPartialOrder_  = ×-isPartialOrder
{-# WARNING_ON_USAGE _×-isPartialOrder_
"Warning: _×-isPartialOrder_ was deprecated in v0.15.
Please use ×-isPartialOrder instead."
#-}
_×-isDecTotalOrder_ = ×-isDecTotalOrder
{-# WARNING_ON_USAGE _×-isDecTotalOrder_
"Warning: _×-isDecTotalOrder_ was deprecated in v0.15.
Please use ×-isDecTotalOrder instead."
#-}
_×-poset_           = ×-poset
{-# WARNING_ON_USAGE _×-poset_
"Warning: _×-poset_ was deprecated in v0.15.
Please use ×-poset instead."
#-}
_×-totalOrder_      = ×-totalOrder
{-# WARNING_ON_USAGE _×-totalOrder_
"Warning: _×-totalOrder_ was deprecated in v0.15.
Please use ×-totalOrder instead."
#-}
_×-decTotalOrder_   = ×-decTotalOrder
{-# WARNING_ON_USAGE _×-decTotalOrder_
"Warning: _×-decTotalOrder_ was deprecated in v0.15.
Please use ×-decTotalOrder instead."
#-}
×-≈-respects₂       = ×-respects₂
{-# WARNING_ON_USAGE ×-≈-respects₂
"Warning: ×-≈-respects₂ was deprecated in v0.15.
Please use ×-respects₂ instead."
#-}