------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic ordering of lists
------------------------------------------------------------------------

-- The definition of lexicographic ordering used here is suitable if
-- the argument order is a (non-strict) partial order. The
-- lexicographic ordering itself can be either strict or non-strict,
-- depending on the value of a parameter.

module Relation.Binary.List.NonStrictLex where

open import Data.Empty
open import Function
open import Data.Unit using (⊤; tt)
open import Data.Product
open import Data.List
open import Level
open import Relation.Nullary
open import Relation.Binary

import Relation.Binary.NonStrictToStrict as Conv
import Relation.Binary.List.StrictLex as Strict

open import Relation.Binary.List.Pointwise as Pointwise using ([])

module _ {A : Set} where

  Lex : (P : Set) → (_≈_ _≤_ : Rel A zero) → Rel (List A) zero
  Lex P _≈_ _≤_ = Strict.Lex P _≈_ (Conv._<_ _≈_ _≤_)

  -- Strict lexicographic ordering.

  Lex-< : (_≈_ _≤_ : Rel A zero) → Rel (List A) zero
  Lex-< = Lex ⊥

  -- Non-strict lexicographic ordering.

  Lex-≤ : (_≈_ _≤_ : Rel A zero) → Rel (List A) zero
  Lex-≤ = Lex ⊤

  ------------------------------------------------------------------------
  -- Properties

  ≤-reflexive : ∀ _≈_ _≤_ → Pointwise.Rel _≈_ ⇒ Lex-≤ _≈_ _≤_
  ≤-reflexive _≈_ _≤_ = Strict.≤-reflexive _≈_ (Conv._<_ _≈_ _≤_)

  <-irreflexive : ∀ {_≈_ _≤_} →
                  Irreflexive (Pointwise.Rel _≈_) (Lex-< _≈_ _≤_)
  <-irreflexive {_≈_} {_≤_} =
    Strict.<-irreflexive {_<_ = Conv._<_ _≈_ _≤_} (Conv.irrefl _≈_ _≤_)

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

  antisymmetric : ∀ {P _≈_ _≤_} →
                  Symmetric _≈_ → Antisymmetric _≈_ _≤_ →
                  Antisymmetric (Pointwise.Rel _≈_) (Lex P _≈_ _≤_)
  antisymmetric {_≈_ = _≈_} {_≤_} sym antisym =
    Strict.antisymmetric sym (Conv.irrefl _≈_ _≤_)
                         (Conv.antisym⟶asym _≈_ _ antisym)

  <-asymmetric : ∀ {_≈_ _≤_} →
                 IsEquivalence _≈_ → _≤_ Respects₂ _≈_ →
                 Antisymmetric _≈_ _≤_ → Asymmetric (Lex-< _≈_ _≤_)
  <-asymmetric {_≈_} eq resp antisym  =
    Strict.<-asymmetric sym (Conv.<-resp-≈ _ _ eq resp)
                        (Conv.antisym⟶asym _≈_ _ antisym)
    where open IsEquivalence eq

  respects₂ : ∀ {P _≈_ _≤_} →
              IsEquivalence _≈_ → _≤_ Respects₂ _≈_ →
              Lex P _≈_ _≤_ Respects₂ Pointwise.Rel _≈_
  respects₂ eq resp = Strict.respects₂ eq (Conv.<-resp-≈ _ _ eq resp)

  decidable : ∀ {P _≈_ _≤_} →
              Dec P → Decidable _≈_ → Decidable _≤_ →
              Decidable (Lex P _≈_ _≤_)
  decidable dec-P dec-≈ dec-≤ =
    Strict.decidable dec-P dec-≈ (Conv.decidable _ _ dec-≈ dec-≤)

  <-decidable :
    ∀ {_≈_ _≤_} →
    Decidable _≈_ → Decidable _≤_ → Decidable (Lex-< _≈_ _≤_)
  <-decidable = decidable (no id)

  ≤-decidable :
    ∀ {_≈_ _≤_} →
    Decidable _≈_ → Decidable _≤_ → Decidable (Lex-≤ _≈_ _≤_)
  ≤-decidable = decidable (yes tt)

  ≤-total : ∀ {_≈_ _≤_} → Symmetric _≈_ → Decidable _≈_ →
            Antisymmetric _≈_ _≤_ → Total _≤_ →
            Total (Lex-≤ _≈_ _≤_)
  ≤-total sym dec-≈ antisym tot =
    Strict.≤-total sym (Conv.trichotomous _ _ sym dec-≈ antisym tot)

  <-compare : ∀ {_≈_ _≤_} → Symmetric _≈_ → Decidable _≈_ →
              Antisymmetric _≈_ _≤_ → Total _≤_ →
              Trichotomous (Pointwise.Rel _≈_) (Lex-< _≈_ _≤_)
  <-compare sym dec-≈ antisym tot =
    Strict.<-compare sym (Conv.trichotomous _ _ sym dec-≈ antisym tot)

  -- Some collections of properties which are preserved by Lex-≤ or
  -- Lex-<.

  ≤-isPreorder : ∀ {_≈_ _≤_} →
                 IsPartialOrder _≈_ _≤_ →
                 IsPreorder (Pointwise.Rel _≈_) (Lex-≤ _≈_ _≤_)
  ≤-isPreorder po =
    Strict.≤-isPreorder
       isEquivalence (Conv.trans _ _ po)
       (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
   where open IsPartialOrder po

  ≤-isPartialOrder : ∀ {_≈_ _≤_} →
                     IsPartialOrder _≈_ _≤_ →
                     IsPartialOrder (Pointwise.Rel _≈_) (Lex-≤ _≈_ _≤_)
  ≤-isPartialOrder po =
    Strict.≤-isPartialOrder
      (Conv.isPartialOrder⟶isStrictPartialOrder _ _ po)

  ≤-isTotalOrder : ∀ {_≈_ _≤_} →
                   Decidable _≈_ → IsTotalOrder _≈_ _≤_ →
                   IsTotalOrder (Pointwise.Rel _≈_) (Lex-≤ _≈_ _≤_)
  ≤-isTotalOrder dec tot =
    Strict.≤-isTotalOrder
      (Conv.isTotalOrder⟶isStrictTotalOrder _ _ dec tot)

  ≤-isDecTotalOrder :
    ∀ {_≈_ _≤_} →
    IsDecTotalOrder _≈_ _≤_ →
    IsDecTotalOrder (Pointwise.Rel _≈_) (Lex-≤ _≈_ _≤_)
  ≤-isDecTotalOrder dtot =
    Strict.≤-isDecTotalOrder
      (Conv.isDecTotalOrder⟶isStrictTotalOrder _ _ dtot)

  <-isStrictPartialOrder : ∀ {_≈_ _≤_} →
    IsPartialOrder _≈_ _≤_ →
    IsStrictPartialOrder (Pointwise.Rel _≈_) (Lex-< _≈_ _≤_)
  <-isStrictPartialOrder po =
    Strict.<-isStrictPartialOrder
      (Conv.isPartialOrder⟶isStrictPartialOrder _ _ po)

  <-isStrictTotalOrder : ∀ {_≈_ _≤_} →
    Decidable _≈_ → IsTotalOrder _≈_ _≤_ →
    IsStrictTotalOrder (Pointwise.Rel _≈_) (Lex-< _≈_ _≤_)
  <-isStrictTotalOrder dec tot =
    Strict.<-isStrictTotalOrder
      (Conv.isTotalOrder⟶isStrictTotalOrder _ _ dec tot)

-- "Packages" (e.g. preorders) can also be handled.

≤-preorder : Poset _ _ _ → Preorder _ _ _
≤-preorder po = record
  { isPreorder = ≤-isPreorder isPartialOrder
  } where open Poset po

≤-partialOrder : Poset _ _ _ → Poset _ _ _
≤-partialOrder po = record
  { isPartialOrder = ≤-isPartialOrder isPartialOrder
  } where open Poset po

≤-decTotalOrder : DecTotalOrder _ _ _ → DecTotalOrder _ _ _
≤-decTotalOrder dtot = record
  { isDecTotalOrder = ≤-isDecTotalOrder isDecTotalOrder
  } where open DecTotalOrder dtot

<-strictPartialOrder : Poset _ _ _ → StrictPartialOrder _ _ _
<-strictPartialOrder po = record
  { isStrictPartialOrder = <-isStrictPartialOrder isPartialOrder
  } where open Poset po

<-strictTotalOrder : DecTotalOrder _ _ _ → StrictTotalOrder _ _ _
<-strictTotalOrder dtot = record
  { isStrictTotalOrder = <-isStrictTotalOrder _≟_ isTotalOrder
  } where open IsDecTotalOrder (DecTotalOrder.isDecTotalOrder dtot)