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

-- The definitions of lexicographic ordering used here are suitable if
-- the argument order is a strict partial order.

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

module Data.List.Relation.Binary.Lex.Strict where

open import Data.Empty using (⊥)
open import Data.Unit.Base using (⊤; tt)
open import Function.Base using (_∘_; id)
open import Data.Product.Base using (_,_)
open import Data.Sum.Base using (inj₁; inj₂)
open import Data.List.Base using (List; []; _∷_)
open import Level using (_⊔_)
open import Relation.Nullary using (yes; no; ¬_)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Bundles
  using (StrictPartialOrder; StrictTotalOrder; Preorder; Poset; DecPoset; DecTotalOrder)
open import Relation.Binary.Structures
  using (IsEquivalence; IsStrictPartialOrder; IsStrictTotalOrder; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder)
open import Relation.Binary.Definitions
  using (Irreflexive; Symmetric; _Respects₂_; Total; Asymmetric; Antisymmetric; Transitive; Trichotomous; Decidable; tri≈; tri<; tri>)
open import Relation.Binary.Consequences
open import Data.List.Relation.Binary.Pointwise as Pointwise
   using (Pointwise; []; _∷_; head; tail)

import Data.List.Relation.Binary.Lex as Core

------------------------------------------------------------------------
-- Re-exporting core definitions

open Core public
  using (Lex-<; Lex-≤; base; halt; this; next; ¬≤-this; ¬≤-next)

------------------------------------------------------------------------
-- Strict lexicographic ordering.

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

  -- Properties

  module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where

    private
      _≋_ = Pointwise _≈_
      _<_ = Lex-< _≈_ _≺_

    xs≮[] : ∀ {xs} → ¬ xs < []
    xs≮[] (base ())

    ¬[]<[] : ¬ [] < []
    ¬[]<[] = xs≮[]

    <-irreflexive : Irreflexive _≈_ _≺_ → Irreflexive _≋_ _<_
    <-irreflexive irr (x≈y ∷ xs≋ys) (this x<y)     = irr x≈y x<y
    <-irreflexive irr (x≈y ∷ xs≋ys) (next _ xs⊴ys) =
      <-irreflexive irr xs≋ys xs⊴ys

    <-asymmetric : Symmetric _≈_ → _≺_ Respects₂ _≈_ → Asymmetric _≺_ →
                   Asymmetric _<_
    <-asymmetric sym resp as = asym
      where
      irrefl : Irreflexive _≈_ _≺_
      irrefl = asym⇒irr resp sym as

      asym : Asymmetric _<_
      asym (base bot)       _                = bot
      asym (this x<y)       (this y<x)       = as x<y y<x
      asym (this x<y)       (next y≈x ys⊴xs) = irrefl (sym y≈x) x<y
      asym (next x≈y xs⊴ys) (this y<x)       = irrefl (sym x≈y) y<x
      asym (next x≈y xs⊴ys) (next y≈x ys⊴xs) = asym xs⊴ys ys⊴xs

    <-antisymmetric : Symmetric _≈_ → Irreflexive _≈_ _≺_ →
                      Asymmetric _≺_ → Antisymmetric _≋_ _<_
    <-antisymmetric = Core.antisymmetric

    <-transitive : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ →
                   Transitive _≺_ → Transitive _<_
    <-transitive = Core.transitive

    <-compare : Symmetric _≈_ → Trichotomous _≈_ _≺_ →
                Trichotomous _≋_ _<_
    <-compare sym tri []       []       = tri≈ ¬[]<[] []    ¬[]<[]
    <-compare sym tri []       (y ∷ ys) = tri< halt   (λ()) (λ())
    <-compare sym tri (x ∷ xs) []       = tri> (λ())  (λ()) halt
    <-compare sym tri (x ∷ xs) (y ∷ ys) with tri x y
    ... | tri< x<y x≉y y≮x =
          tri< (this x<y) (x≉y ∘ head) (¬≤-this (x≉y ∘ sym) y≮x)
    ... | tri> x≮y x≉y y<x =
          tri> (¬≤-this x≉y x≮y) (x≉y ∘ head) (this y<x)
    ... | tri≈ x≮y x≈y y≮x with <-compare sym tri xs ys
    ...   | tri< xs<ys xs≉ys ys≮xs =
            tri< (next x≈y xs<ys) (xs≉ys ∘ tail) (¬≤-next y≮x ys≮xs)
    ...   | tri≈ xs≮ys xs≈ys ys≮xs =
            tri≈ (¬≤-next x≮y xs≮ys) (x≈y ∷ xs≈ys) (¬≤-next y≮x ys≮xs)
    ...   | tri> xs≮ys xs≉ys ys<xs =
            tri> (¬≤-next x≮y xs≮ys) (xs≉ys ∘ tail) (next (sym x≈y) ys<xs)

    <-decidable : Decidable _≈_ → Decidable _≺_ → Decidable _<_
    <-decidable = Core.decidable (no id)

    <-respects₂ : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ →
                  _<_ Respects₂ _≋_
    <-respects₂ = Core.respects₂

    <-isStrictPartialOrder : IsStrictPartialOrder _≈_ _≺_ →
                             IsStrictPartialOrder _≋_ _<_
    <-isStrictPartialOrder spo = record
      { isEquivalence = Pointwise.isEquivalence isEquivalence
      ; irrefl        = <-irreflexive irrefl
      ; trans         = Core.transitive isEquivalence <-resp-≈ trans
      ; <-resp-≈      = Core.respects₂ isEquivalence <-resp-≈
      } where open IsStrictPartialOrder spo

    <-isStrictTotalOrder : IsStrictTotalOrder _≈_ _≺_ →
                           IsStrictTotalOrder _≋_ _<_
    <-isStrictTotalOrder sto = record
      { isStrictPartialOrder = <-isStrictPartialOrder isStrictPartialOrder
      ; compare              = <-compare Eq.sym compare
      } where open IsStrictTotalOrder sto

<-strictPartialOrder : ∀ {a ℓ₁ ℓ₂} → StrictPartialOrder a ℓ₁ ℓ₂ →
                       StrictPartialOrder _ _ _
<-strictPartialOrder spo = record
  { isStrictPartialOrder = <-isStrictPartialOrder isStrictPartialOrder
  } where open StrictPartialOrder spo

<-strictTotalOrder : ∀ {a ℓ₁ ℓ₂} → StrictTotalOrder a ℓ₁ ℓ₂ →
                       StrictTotalOrder _ _ _
<-strictTotalOrder sto = record
  { isStrictTotalOrder = <-isStrictTotalOrder isStrictTotalOrder
  } where open StrictTotalOrder sto

------------------------------------------------------------------------
-- Non-strict lexicographic ordering.

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

  -- Properties

  ≤-reflexive : (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) →
                Pointwise _≈_ ⇒ Lex-≤ _≈_ _≺_
  ≤-reflexive _≈_ _≺_ []            = base tt
  ≤-reflexive _≈_ _≺_ (x≈y ∷ xs≈ys) =
    next x≈y (≤-reflexive _≈_ _≺_ xs≈ys)

  module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where

    private
      _≋_ = Pointwise _≈_
      _≤_ = Lex-≤ _≈_ _≺_

    ≤-antisymmetric : Symmetric _≈_ → Irreflexive _≈_ _≺_ →
                      Asymmetric _≺_ → Antisymmetric _≋_ _≤_
    ≤-antisymmetric = Core.antisymmetric

    ≤-transitive : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ →
                   Transitive _≺_ → Transitive _≤_
    ≤-transitive = Core.transitive

    -- Note that trichotomy is an unnecessarily strong precondition for
    -- the following lemma.

    ≤-total : Symmetric _≈_ → Trichotomous _≈_ _≺_ → Total _≤_
    ≤-total _   _   []       []       = inj₁ (base tt)
    ≤-total _   _   []       (x ∷ xs) = inj₁ halt
    ≤-total _   _   (x ∷ xs) []       = inj₂ halt
    ≤-total sym tri (x ∷ xs) (y ∷ ys) with tri x y
    ... | tri< x<y _ _ = inj₁ (this x<y)
    ... | tri> _ _ y<x = inj₂ (this y<x)
    ... | tri≈ _ x≈y _ with ≤-total sym tri xs ys
    ...   | inj₁ xs≲ys = inj₁ (next      x≈y  xs≲ys)
    ...   | inj₂ ys≲xs = inj₂ (next (sym x≈y) ys≲xs)

    ≤-decidable : Decidable _≈_ → Decidable _≺_ → Decidable _≤_
    ≤-decidable = Core.decidable (yes tt)

    ≤-respects₂ : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ →
                  _≤_ Respects₂ _≋_
    ≤-respects₂ = Core.respects₂

    ≤-isPreorder : IsEquivalence _≈_ → Transitive _≺_ →
                   _≺_ Respects₂ _≈_ → IsPreorder _≋_ _≤_
    ≤-isPreorder eq tr resp = record
      { isEquivalence = Pointwise.isEquivalence eq
      ; reflexive     = ≤-reflexive _≈_ _≺_
      ; trans         = Core.transitive eq resp tr
      }

    ≤-isPartialOrder : IsStrictPartialOrder _≈_ _≺_ →
                       IsPartialOrder _≋_ _≤_
    ≤-isPartialOrder  spo = record
      { isPreorder = ≤-isPreorder isEquivalence trans <-resp-≈
      ; antisym    = Core.antisymmetric Eq.sym irrefl asym
      }
      where open IsStrictPartialOrder spo

    ≤-isDecPartialOrder : IsStrictTotalOrder _≈_ _≺_ →
                          IsDecPartialOrder _≋_ _≤_
    ≤-isDecPartialOrder sto = record
      { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
      ; _≟_            = Pointwise.decidable _≟_
      ; _≤?_           = ≤-decidable _≟_ _<?_
      } where open IsStrictTotalOrder sto

    ≤-isTotalOrder : IsStrictTotalOrder _≈_ _≺_ → IsTotalOrder _≋_ _≤_
    ≤-isTotalOrder sto = record
      { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
      ; total          = ≤-total Eq.sym compare
      }
      where open IsStrictTotalOrder sto

    ≤-isDecTotalOrder : IsStrictTotalOrder _≈_ _≺_ →
                        IsDecTotalOrder _≋_ _≤_
    ≤-isDecTotalOrder sto = record
      { isTotalOrder = ≤-isTotalOrder sto
      ; _≟_          = Pointwise.decidable _≟_
      ; _≤?_         = ≤-decidable _≟_ _<?_
      }
      where open IsStrictTotalOrder sto

≤-preorder : ∀ {a ℓ₁ ℓ₂} → Preorder a ℓ₁ ℓ₂ → Preorder _ _ _
≤-preorder pre = record
  { isPreorder = ≤-isPreorder isEquivalence trans ∼-resp-≈
  } where open Preorder pre

≤-partialOrder : ∀ {a ℓ₁ ℓ₂} → StrictPartialOrder a ℓ₁ ℓ₂ → Poset _ _ _
≤-partialOrder spo = record
  { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
  } where open StrictPartialOrder spo

≤-decPoset : ∀ {a ℓ₁ ℓ₂} → StrictTotalOrder a ℓ₁ ℓ₂ →
             DecPoset _ _ _
≤-decPoset sto = record
  { isDecPartialOrder = ≤-isDecPartialOrder isStrictTotalOrder
  } where open StrictTotalOrder sto


≤-decTotalOrder : ∀ {a ℓ₁ ℓ₂} → StrictTotalOrder a ℓ₁ ℓ₂ →
                  DecTotalOrder _ _ _
≤-decTotalOrder sto = record
  { isDecTotalOrder = ≤-isDecTotalOrder isStrictTotalOrder
  } where open StrictTotalOrder sto