------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic ordering of same-length vector
------------------------------------------------------------------------

-- The definitions of lexicographic orderings used here is suitable if
-- the argument order is a (non-strict) partial order.

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

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

open import Data.Empty
open import Data.Unit.Base using (⊤; tt)
open import Data.Product.Base using (proj₁; proj₂)
open import Data.Nat.Base using (ℕ)
open import Data.Vec.Base using (Vec; []; _∷_)
import Data.Vec.Relation.Binary.Lex.Strict as Strict
open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
  using (Pointwise; []; _∷_; head; tail)
open import Function.Base using (id)
open import Level using (Level; _⊔_)
open import Relation.Binary.Core using (REL; Rel; _⇒_)
open import Relation.Binary.Bundles
  using (Poset; StrictPartialOrder; DecPoset; DecStrictPartialOrder; DecTotalOrder; StrictTotalOrder; Preorder; TotalOrder)
open import Relation.Binary.Structures
  using (IsEquivalence; IsPartialOrder; IsStrictPartialOrder; IsDecPartialOrder; IsDecStrictPartialOrder; IsDecTotalOrder; IsStrictTotalOrder; IsPreorder; IsTotalOrder)
open import Relation.Binary.Definitions
  using (Irreflexive; _Respects₂_; Antisymmetric; Asymmetric; Symmetric; Trans; Decidable; Total; Trichotomous)
import Relation.Binary.Construct.NonStrictToStrict as Conv
open import Relation.Nullary hiding (Irrelevant)

private
  variable
    a ℓ₁ ℓ₂ : Level
    A : Set a

------------------------------------------------------------------------
-- Publicly re-export definitions from Core
------------------------------------------------------------------------

open import Data.Vec.Relation.Binary.Lex.Core as Core public
  using (base; this; next; ≰-this; ≰-next)

------------------------------------------------------------------------
-- Definitions
------------------------------------------------------------------------

module _ {A : Set a} (_≈_ : Rel A ℓ₁) (_≼_ : Rel A ℓ₂) where

  Lex-< : ∀ {m n} → REL (Vec A m) (Vec A n) (a ⊔ ℓ₁ ⊔ ℓ₂)
  Lex-< = Core.Lex {A = A} ⊥ _≈_ (Conv._<_ _≈_ _≼_)

  Lex-≤ : ∀ {m n} → REL (Vec A m) (Vec A n) (a ⊔ ℓ₁ ⊔ ℓ₂)
  Lex-≤ = Core.Lex {A = A} ⊤ _≈_ (Conv._<_ _≈_ _≼_)

------------------------------------------------------------------------
-- Properties of Lex-<
------------------------------------------------------------------------

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

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

  <-irrefl : ∀ {m n} → Irreflexive (_≋_ {m} {n}) _<_
  <-irrefl = Strict.<-irrefl (Conv.<-irrefl _≈_ _≼_)

  <-asym : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ → Antisymmetric _≈_ _≼_ →
           ∀ {n} → Asymmetric (_<_ {n} {n})
  <-asym ≈-equiv ≼-resp-≈ ≼-antisym = Strict.<-asym sym
    (Conv.<-resp-≈ _ _ ≈-equiv ≼-resp-≈)
    (Conv.<-asym _≈_ _ ≼-antisym)
    where open IsEquivalence ≈-equiv

  <-antisym : Symmetric _≈_ → Antisymmetric _≈_ _≼_ →
              ∀ {n} → Antisymmetric (_≋_ {n} {n}) _<_
  <-antisym ≈-sym ≼-antisym = Core.antisym ≈-sym
    (Conv.<-irrefl _≈_ _≼_)
    (Conv.<-asym _≈_ _≼_ ≼-antisym)

  <-trans : IsPartialOrder _≈_ _≼_ →
            ∀ {m n o} → Trans (_<_ {m} {n}) (_<_ {n} {o}) _<_
  <-trans ≼-isPartialOrder = Core.transitive Eq.isPartialEquivalence
    (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
    (Conv.<-trans _ _ ≼-isPartialOrder)
    where open IsPartialOrder ≼-isPartialOrder

  <-resp₂ : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ →
            ∀ {n} → _Respects₂_ (_<_ {n} {n}) _≋_
  <-resp₂ ≈-equiv ≼-resp-≈ = Core.respects₂
    (IsEquivalence.isPartialEquivalence ≈-equiv)
    (Conv.<-resp-≈ _ _ ≈-equiv ≼-resp-≈)

  <-cmp : Symmetric _≈_ → Decidable _≈_ → Antisymmetric _≈_ _≼_ → Total _≼_ →
          ∀ {n} → Trichotomous (_≋_ {n} {n}) _<_
  <-cmp ≈-sym _≟_ ≼-antisym ≼-total = Strict.<-cmp ≈-sym
    (Conv.<-trichotomous _ _ ≈-sym _≟_ ≼-antisym ≼-total)

  <-dec : Decidable _≈_ → Decidable _≼_ → ∀ {m n} → Decidable (_<_ {m} {n})
  <-dec _≟_ _≼?_ = Core.decidable (no id) _≟_
    (Conv.<-decidable _ _ _≟_ _≼?_)

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

  <-isStrictPartialOrder : IsPartialOrder _≈_ _≼_ →
                           ∀ {n} → IsStrictPartialOrder (_≋_ {n} {n}) _<_
  <-isStrictPartialOrder ≼-isPartialOrder {n} = Strict.<-isStrictPartialOrder
    (Conv.<-isStrictPartialOrder _ _ ≼-isPartialOrder)

  <-isDecStrictPartialOrder : IsDecPartialOrder _≈_ _≼_ →
                              ∀ {n} → IsDecStrictPartialOrder (_≋_ {n} {n}) _<_
  <-isDecStrictPartialOrder ≼-isDecPartialOrder {n} = Strict.<-isDecStrictPartialOrder
    (Conv.<-isDecStrictPartialOrder _ _ ≼-isDecPartialOrder)

  <-isStrictTotalOrder : IsDecTotalOrder _≈_ _≼_ →
                         ∀ {n} → IsStrictTotalOrder (_≋_ {n} {n}) _<_
  <-isStrictTotalOrder ≼-isDecTotalOrder {n} = Strict.<-isStrictTotalOrder
    (Conv.<-isStrictTotalOrder₂ _ _ ≼-isDecTotalOrder)

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

<-strictPartialOrder : Poset a ℓ₁ ℓ₂ → ℕ → StrictPartialOrder _ _ _
<-strictPartialOrder ≼-po n = record
  { isStrictPartialOrder = <-isStrictPartialOrder isPartialOrder {n = n}
  } where open Poset ≼-po

<-decStrictPartialOrder : DecPoset a ℓ₁ ℓ₂ → ℕ → DecStrictPartialOrder _ _ _
<-decStrictPartialOrder ≼-dpo n = record
  { isDecStrictPartialOrder = <-isDecStrictPartialOrder isDecPartialOrder {n = n}
  } where open DecPoset ≼-dpo

<-strictTotalOrder : DecTotalOrder a ℓ₁ ℓ₂ → ℕ → StrictTotalOrder _ _ _
<-strictTotalOrder ≼-dto n = record
  { isStrictTotalOrder = <-isStrictTotalOrder isDecTotalOrder {n = n}
  } where open DecTotalOrder ≼-dto

------------------------------------------------------------------------
-- Properties of Lex-≤
------------------------------------------------------------------------

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

  private
    _≋_ = Pointwise _≈_
    _<_ = Lex-< _≈_ _≼_
    _≤_ = Lex-≤ _≈_ _≼_

  <⇒≤ : ∀ {m n} {xs : Vec A m} {ys : Vec A n} → xs < ys → xs ≤ ys
  <⇒≤ = Core.map-P ⊥-elim

  ≤-refl : ∀ {m n} → (_≋_ {m} {n}) ⇒ _≤_
  ≤-refl = Strict.≤-refl

  ≤-antisym : Symmetric _≈_ → Antisymmetric _≈_ _≼_ →
              ∀ {n} → Antisymmetric (_≋_ {n} {n}) _≤_
  ≤-antisym ≈-sym ≼-antisym = Core.antisym ≈-sym
    (Conv.<-irrefl _≈_ _≼_)
    (Conv.<-asym _ _≼_ ≼-antisym)

  private
    trans : IsPartialOrder _≈_ _≼_ → ∀ {P₁ P₂} {m n o} →
            Trans (Core.Lex P₁ _≈_ (Conv._<_ _≈_ _≼_) {m} {n}) (Core.Lex P₂ _≈_ (Conv._<_ _≈_ _≼_) {n} {o}) _
    trans ≼-po = Core.transitive′
      (IsEquivalence.isPartialEquivalence isEquivalence)
      (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
      (Conv.<-trans _ _≼_ ≼-po)
      where open IsPartialOrder ≼-po

  ≤-trans : IsPartialOrder _≈_ _≼_ → ∀ {m n o} → Trans (_≤_ {m} {n}) (_≤_ {n} {o}) _≤_
  ≤-trans ≼-po xs≤ys ys≤zs = Core.map-P proj₁ (trans ≼-po xs≤ys ys≤zs)

  <-transʳ : IsPartialOrder _≈_ _≼_ → ∀ {m n o} → Trans (_≤_ {m} {n}) (_<_ {n} {o}) _<_
  <-transʳ ≼-po xs≤ys ys<zs = Core.map-P proj₂ (trans ≼-po xs≤ys ys<zs)

  <-transˡ : IsPartialOrder _≈_ _≼_ → ∀ {m n o} → Trans (_<_ {m} {n}) (_≤_ {n} {o}) _<_
  <-transˡ ≼-po xs<ys ys≤zs = Core.map-P proj₁ (trans ≼-po xs<ys ys≤zs)

  ≤-total : Symmetric _≈_ → Decidable _≈_ → Antisymmetric _≈_ _≼_ → Total _≼_ →
            ∀ {n} → Total (_≤_ {n})
  ≤-total ≈-sym _≟_ ≼-antisym ≼-total = Strict.≤-total ≈-sym
    (Conv.<-trichotomous _ _ ≈-sym _≟_ ≼-antisym ≼-total)

  ≤-dec : Decidable _≈_ → Decidable _≼_ →
          ∀ {m n} → Decidable (_≤_ {m} {n})
  ≤-dec _≟_ _≼?_ = Core.decidable (yes tt) _≟_
    (Conv.<-decidable _ _ _≟_ _≼?_)

  ≤-resp₂ : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ →
            ∀ {n} → _Respects₂_ (_≤_ {n} {n}) _≋_
  ≤-resp₂ ≈-equiv ≼-resp-≈ = Core.respects₂
    (IsEquivalence.isPartialEquivalence ≈-equiv)
    (Conv.<-resp-≈ _ _ ≈-equiv ≼-resp-≈)

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

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

  ≤-isPartialOrder : IsPartialOrder _≈_ _≼_ →
                     ∀ {n} → IsPartialOrder (_≋_ {n} {n}) _≤_
  ≤-isPartialOrder ≼-po = Strict.≤-isPartialOrder (Conv.<-isStrictPartialOrder _ _ ≼-po)

  ≤-isDecPartialOrder : IsDecPartialOrder _≈_ _≼_ →
                        ∀ {n} → IsDecPartialOrder (_≋_ {n} {n}) _≤_
  ≤-isDecPartialOrder ≼-dpo = Strict.≤-isDecPartialOrder (Conv.<-isDecStrictPartialOrder _ _ ≼-dpo)

  ≤-isTotalOrder : Decidable _≈_ → IsTotalOrder _≈_ _≼_ →
                   ∀ {n} → IsTotalOrder (_≋_ {n} {n}) _≤_
  ≤-isTotalOrder _≟_ ≼-isTotalOrder = Strict.≤-isTotalOrder (Conv.<-isStrictTotalOrder₁ _ _ _≟_ ≼-isTotalOrder)

  ≤-isDecTotalOrder : IsDecTotalOrder _≈_ _≼_ →
                      ∀ {n} → IsDecTotalOrder (_≋_ {n} {n}) _≤_
  ≤-isDecTotalOrder ≼-isDecTotalOrder  = Strict.≤-isDecTotalOrder (Conv.<-isStrictTotalOrder₂ _ _ ≼-isDecTotalOrder)

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

≤-preorder : Poset a ℓ₁ ℓ₂ → ℕ → Preorder _ _ _
≤-preorder ≼-po n = record
  { isPreorder = ≤-isPreorder isPartialOrder {n = n}
  } where open Poset ≼-po

≤-poset : Poset a ℓ₁ ℓ₂ → ℕ → Poset _ _ _
≤-poset ≼-po n = record
  { isPartialOrder = ≤-isPartialOrder isPartialOrder {n = n}
  } where open Poset ≼-po

≤-decPoset : DecPoset a ℓ₁ ℓ₂ → ℕ → DecPoset _ _ _
≤-decPoset ≼-dpo n = record
  { isDecPartialOrder = ≤-isDecPartialOrder isDecPartialOrder {n = n}
  } where open DecPoset ≼-dpo

≤-totalOrder : (≼-dto : TotalOrder a ℓ₁ ℓ₂) → Decidable (TotalOrder._≈_ ≼-dto) → ℕ → TotalOrder _ _ _
≤-totalOrder ≼-dto _≟_ n = record
  { isTotalOrder = ≤-isTotalOrder _≟_ isTotalOrder {n = n}
  } where open TotalOrder ≼-dto

≤-decTotalOrder : DecTotalOrder a ℓ₁ ℓ₂ → ℕ → DecTotalOrder _ _ _
≤-decTotalOrder ≼-dto n = record
  { isDecTotalOrder = ≤-isDecTotalOrder isDecTotalOrder {n = n}
  } where open DecTotalOrder ≼-dto

------------------------------------------------------------------------
-- Reasoning
------------------------------------------------------------------------

module ≤-Reasoning  {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂}
                    (≼-po : IsPartialOrder _≈_ _≼_)
                    (n : ℕ)
                    where

  open IsPartialOrder ≼-po

  open import Relation.Binary.Reasoning.Base.Triple
    (≤-isPreorder ≼-po {n})
    (<-asym isEquivalence ≤-resp-≈ antisym)
    (<-trans ≼-po)
    (<-resp₂ isEquivalence ≤-resp-≈)
    <⇒≤
    (<-transˡ ≼-po)
    (<-transʳ ≼-po)
    public