------------------------------------------------------------------------
-- 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.Base 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 ≡
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) (≡.trans m≡n n≡o)
transitive′ (this x≺y m≡n) (next y≈z ys<zs) = this (≺-respʳ-≈ y≈z x≺y) (≡.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) (≡.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 ℕ.≟ 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