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

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

module Data.Vec.Relation.Binary.Lex.Core {a} {A : Set a} where

open import Data.Empty
open import Data.Nat using (ℕ; suc)
import Data.Nat.Properties as ℕ
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; uncurry)
open import Data.Vec.Base using (Vec; []; _∷_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
open import Function.Base using (flip)
open import Function.Bundles using (_⇔_; mk⇔)
open import Level using (Level; _⊔_)
open import Relation.Binary.Core using (Rel; REL)
open import Relation.Binary.Definitions
  using (Transitive; Symmetric; Asymmetric; Antisymmetric; Irreflexive; Trans; _Respects₂_; _Respectsˡ_; _Respectsʳ_; Decidable; Irrelevant)
open import Relation.Binary.Structures using (IsPartialEquivalence)
open import Relation.Binary.PropositionalEquality.Core as P
  using (_≡_; refl; cong)
import Relation.Nullary as Nullary
open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_; _⊎-dec_)
open import Relation.Nullary.Negation

private
  variable
    ℓ₁ ℓ₂ : Level

------------------------------------------------------------------------
-- Definition

-- The lexicographic ordering itself can be either strict or non-strict,
-- depending on whether type P is inhabited.

data Lex {A : Set a} (P : Set) (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂)
       : ∀ {m n} → REL (Vec A m) (Vec A n) (a ⊔ ℓ₁ ⊔ ℓ₂) where
  base : (p : P) → Lex P _≈_ _≺_ [] []
  this : ∀ {x y m n} {xs : Vec A m} {ys : Vec A n}
         (x≺y : x ≺ y) (m≡n : m ≡ n) → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)
  next : ∀ {x y m n} {xs : Vec A m} {ys : Vec A n}
         (x≈y : x ≈ y) (xs<ys : Lex P _≈_ _≺_ xs ys) → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)

------------------------------------------------------------------------
-- Operations

map-P : ∀ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} {P₁ P₂ : Set} → (P₁ → P₂) →
        ∀ {m n} {xs : Vec A m} {ys : Vec A n} →
        Lex P₁ _≈_ _≺_ xs ys → Lex P₂ _≈_ _≺_ xs ys
map-P f (base p)         = base (f p)
map-P f (this x≺y m≡n)   = this x≺y m≡n
map-P f (next x≈y xs<ys) = next x≈y (map-P f xs<ys)

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

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

  length-equal : ∀ {m n} {xs : Vec A m} {ys : Vec A n} →
                 Lex P _≈_ _≺_ xs ys → m ≡ n
  length-equal (base _)         = refl
  length-equal (this x≺y m≡n)   = cong suc m≡n
  length-equal (next x≈y xs<ys) = cong suc (length-equal xs<ys)

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

  private
    _≋_ = Pointwise _≈_
    _<ₗₑₓ_ = Lex P _≈_ _≺_

  ≰-this : ∀ {x y m n} {xs : Vec A m} {ys : Vec A n} →
           ¬ (x ≈ y) → ¬ (x ≺ y) → ¬ (x ∷ xs) <ₗₑₓ (y ∷ ys)
  ≰-this x≉y x≮y (this x≺y m≡n)   = contradiction x≺y x≮y
  ≰-this x≉y x≮y (next x≈y xs<ys) = contradiction x≈y x≉y

  ≰-next : ∀ {x y m n} {xs : Vec A m} {ys : Vec A n} →
           ¬ (x ≺ y) → ¬ (xs <ₗₑₓ ys) → ¬ (x ∷ xs) <ₗₑₓ (y ∷ ys)
  ≰-next x≮y xs≮ys (this x≺y m≡n)   = contradiction x≺y x≮y
  ≰-next x≮y xs≮ys (next x≈y xs<ys) = contradiction xs<ys xs≮ys

  P⇔[]<[] : P ⇔ [] <ₗₑₓ []
  P⇔[]<[] = mk⇔ base (λ { (base p) → p })

  toSum : ∀ {x y n} {xs ys : Vec A n} → (x ∷ xs) <ₗₑₓ (y ∷ ys) → (x ≺ y ⊎ (x ≈ y × xs <ₗₑₓ ys))
  toSum (this x≺y m≡n)   = inj₁ x≺y
  toSum (next x≈y xs<ys) = inj₂ (x≈y , xs<ys)

  ∷<∷-⇔ : ∀ {x y n} {xs ys : Vec A n} → (x ≺ y ⊎ (x ≈ y × xs <ₗₑₓ ys)) ⇔ (x ∷ xs) <ₗₑₓ (y ∷ ys)
  ∷<∷-⇔ = mk⇔ [ flip this refl , uncurry next ] toSum

  module _ (≈-equiv : IsPartialEquivalence _≈_)
           ((≺-respʳ-≈ , ≺-respˡ-≈) : _≺_ Respects₂ _≈_)
           (≺-trans : Transitive _≺_)
           (open IsPartialEquivalence ≈-equiv)
           where

    transitive′ : ∀ {m n o P₂} → Trans (Lex P _≈_ _≺_ {m} {n}) (Lex P₂ _≈_ _≺_ {n} {o}) (Lex (P × P₂) _≈_ _≺_)
    transitive′ (base p₁)        (base p₂)        = base (p₁ , p₂)
    transitive′ (this x≺y m≡n)   (this y≺z n≡o)   = this (≺-trans x≺y y≺z) (P.trans m≡n n≡o)
    transitive′ (this x≺y m≡n)   (next y≈z ys<zs) = this (≺-respʳ-≈ y≈z x≺y) (P.trans m≡n (length-equal ys<zs))
    transitive′ (next x≈y xs<ys) (this y≺z n≡o)   = this (≺-respˡ-≈ (sym x≈y) y≺z) (P.trans (length-equal xs<ys) n≡o)
    transitive′ (next x≈y xs<ys) (next y≈z ys<zs) = next (trans x≈y y≈z) (transitive′ xs<ys ys<zs)

    transitive : ∀ {m n o} → Trans (_<ₗₑₓ_ {m} {n}) (_<ₗₑₓ_ {n} {o}) _<ₗₑₓ_
    transitive xs<ys ys<zs = map-P proj₁ (transitive′ xs<ys ys<zs)

  module _ (≈-sym : Symmetric _≈_) (≺-irrefl : Irreflexive _≈_ _≺_) (≺-asym : Asymmetric _≺_) where

    antisym : ∀ {n} → Antisymmetric (_≋_ {n}) (_<ₗₑₓ_)
    antisym (base _)         (base _)         = []
    antisym (this x≺y m≡n)   (this y≺x n≡m)   = ⊥-elim (≺-asym x≺y y≺x)
    antisym (this x≺y m≡n)   (next y≈x ys<xs) = ⊥-elim (≺-irrefl (≈-sym y≈x) x≺y)
    antisym (next x≈y xs<ys) (this y≺x m≡n)   = ⊥-elim (≺-irrefl (≈-sym x≈y) y≺x)
    antisym (next x≈y xs<ys) (next y≈x ys<xs) = x≈y ∷ (antisym xs<ys ys<xs)

  module _ (≈-equiv : IsPartialEquivalence _≈_) (open IsPartialEquivalence ≈-equiv) where

    respectsˡ : _≺_ Respectsˡ _≈_ → ∀ {m n} → (_<ₗₑₓ_ {m} {n}) Respectsˡ _≋_
    respectsˡ resp []            (base p)         = base p
    respectsˡ resp (x≈y ∷ xs≋ys) (this x≺z m≡n)   = this (resp x≈y x≺z) m≡n
    respectsˡ resp (x≈y ∷ xs≋ys) (next x≈z xs<zs) = next (trans (sym x≈y) x≈z) (respectsˡ resp xs≋ys xs<zs)

    respectsʳ : _≺_ Respectsʳ _≈_ → ∀ {m n} → (_<ₗₑₓ_ {m} {n}) Respectsʳ _≋_
    respectsʳ resp [] (base p)                    = base p
    respectsʳ resp (x≈y ∷ xs≋ys) (this x≺z m≡n)   = this (resp x≈y x≺z) m≡n
    respectsʳ resp (x≈y ∷ xs≋ys) (next x≈z xs<zs) = next (trans x≈z x≈y) (respectsʳ resp xs≋ys xs<zs)

    respects₂ : _≺_ Respects₂ _≈_ → ∀ {n} → (_<ₗₑₓ_ {n} {n}) Respects₂ _≋_
    respects₂ (≺-resp-≈ʳ , ≺-resp-≈ˡ) = respectsʳ ≺-resp-≈ʳ , respectsˡ ≺-resp-≈ˡ

  module _ (P? : Dec P) (_≈?_ : Decidable _≈_) (_≺?_ : Decidable _≺_) where

    decidable : ∀ {m n} → Decidable (_<ₗₑₓ_ {m} {n})
    decidable {m} {n} xs ys with m Data.Nat.≟ n
    decidable {_} {_} []       []       | yes refl = Dec.map P⇔[]<[] P?
    decidable {_} {_} (x ∷ xs) (y ∷ ys) | yes refl = Dec.map ∷<∷-⇔ ((x ≺? y) ⊎-dec (x ≈? y) ×-dec (decidable xs ys))
    decidable {_} {_} _        _        | no  m≢n    = no (λ xs<ys → contradiction (length-equal xs<ys) m≢n)

  module _ (P-irrel  : Nullary.Irrelevant P)
           (≈-irrel  : Irrelevant _≈_)
           (≺-irrel  : Irrelevant _≺_)
           (≺-irrefl : Irreflexive _≈_ _≺_)
           where

    irrelevant : ∀ {m n} → Irrelevant (_<ₗₑₓ_ {m} {n})
    irrelevant (base p₁)          (base p₂)          rewrite P-irrel p₁ p₂                                = refl
    irrelevant (this x≺y₁ m≡n₁)   (this x≺y₂ m≡n₂)   rewrite ≺-irrel x≺y₁ x≺y₂ | ℕ.≡-irrelevant m≡n₁ m≡n₂ = refl
    irrelevant (this x≺y m≡n)     (next x≈y xs<ys₂)  = contradiction x≺y (≺-irrefl x≈y)
    irrelevant (next x≈y xs<ys₁)  (this x≺y m≡n)     = contradiction x≺y (≺-irrefl x≈y)
    irrelevant (next x≈y₁ xs<ys₁) (next x≈y₂ xs<ys₂) rewrite ≈-irrel x≈y₁ x≈y₂ | irrelevant xs<ys₁ xs<ys₂ = refl