{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Binary.Lex where
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit.Base using (⊤; tt)
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; uncurry)
open import Data.List.Base using (List; []; _∷_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Function.Base using (_∘_; flip; id)
open import Function.Bundles using (_⇔_; mk⇔)
open import Level using (_⊔_)
open import Relation.Nullary.Negation using (¬_)
open import Relation.Nullary.Decidable as Dec
using (Dec; yes; no; _×-dec_; _⊎-dec_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Structures using (IsEquivalence)
open import Relation.Binary.Definitions
using (Symmetric; Transitive; Irreflexive; Asymmetric; Antisymmetric; Decidable; _Respects₂_; _Respects_)
open import Data.List.Relation.Binary.Pointwise.Base
using (Pointwise; []; _∷_; head; tail)
open import Data.List.Relation.Binary.Lex.Core public
module _ {a ℓ₁ ℓ₂} {A : Set a} {P : Set}
{_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
private
_≋_ = Pointwise _≈_
_<_ = Lex P _≈_ _≺_
¬≤-this : ∀ {x y xs ys} → ¬ (x ≈ y) → ¬ (x ≺ y) →
¬ (x ∷ xs) < (y ∷ ys)
¬≤-this x≉y x≮y (this x≺y) = x≮y x≺y
¬≤-this x≉y x≮y (next x≈y xs<ys) = x≉y x≈y
¬≤-next : ∀ {x y xs ys} → ¬ x ≺ y → ¬ xs < ys →
¬ (x ∷ xs) < (y ∷ ys)
¬≤-next x≮y xs≮ys (this x≺y) = x≮y x≺y
¬≤-next x≮y xs≮ys (next _ xs<ys) = xs≮ys xs<ys
antisymmetric : Symmetric _≈_ → Irreflexive _≈_ _≺_ →
Asymmetric _≺_ → Antisymmetric _≋_ _<_
antisymmetric sym ir asym = as
where
as : Antisymmetric _≋_ _<_
as (base _) (base _) = []
as (this x≺y) (this y≺x) = ⊥-elim (asym x≺y y≺x)
as (this x≺y) (next y≈x ys<xs) = ⊥-elim (ir (sym y≈x) x≺y)
as (next x≈y xs<ys) (this y≺x) = ⊥-elim (ir (sym x≈y) y≺x)
as (next x≈y xs<ys) (next y≈x ys<xs) = x≈y ∷ as xs<ys ys<xs
toSum : ∀ {x y xs ys} → (x ∷ xs) < (y ∷ ys) → (x ≺ y ⊎ (x ≈ y × xs < ys))
toSum (this x≺y) = inj₁ x≺y
toSum (next x≈y xs<ys) = inj₂ (x≈y , xs<ys)
transitive : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ → Transitive _≺_ →
Transitive _<_
transitive eq resp tr = trans
where
trans : Transitive (Lex P _≈_ _≺_)
trans (base p) (base _) = base p
trans (base y) halt = halt
trans halt (this y≺z) = halt
trans halt (next y≈z ys<zs) = halt
trans (this x≺y) (this y≺z) = this (tr x≺y y≺z)
trans (this x≺y) (next y≈z ys<zs) = this (proj₁ resp y≈z x≺y)
trans (next x≈y xs<ys) (this y≺z) =
this (proj₂ resp (IsEquivalence.sym eq x≈y) y≺z)
trans (next x≈y xs<ys) (next y≈z ys<zs) =
next (IsEquivalence.trans eq x≈y y≈z) (trans xs<ys ys<zs)
respects₂ : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ → _<_ Respects₂ _≋_
respects₂ eq (resp₁ , resp₂) = resp¹ , resp²
where
open IsEquivalence eq using (sym; trans)
resp¹ : ∀ {xs} → Lex P _≈_ _≺_ xs Respects _≋_
resp¹ [] xs<[] = xs<[]
resp¹ (_ ∷ _) halt = halt
resp¹ (x≈y ∷ _) (this z≺x) = this (resp₁ x≈y z≺x)
resp¹ (x≈y ∷ xs≋ys) (next z≈x zs<xs) =
next (trans z≈x x≈y) (resp¹ xs≋ys zs<xs)
resp² : ∀ {ys} → flip (Lex P _≈_ _≺_) ys Respects _≋_
resp² [] []<ys = []<ys
resp² (x≈z ∷ _) (this x≺y) = this (resp₂ x≈z x≺y)
resp² (x≈z ∷ xs≋zs) (next x≈y xs<ys) =
next (trans (sym x≈z) x≈y) (resp² xs≋zs xs<ys)
[]<[]-⇔ : P ⇔ [] < []
[]<[]-⇔ = mk⇔ base (λ { (base p) → p })
∷<∷-⇔ : ∀ {x y xs ys} → (x ≺ y ⊎ (x ≈ y × xs < ys)) ⇔ (x ∷ xs) < (y ∷ ys)
∷<∷-⇔ = mk⇔ [ this , uncurry next ] toSum
module _ (dec-P : Dec P) (dec-≈ : Decidable _≈_) (dec-≺ : Decidable _≺_)
where
decidable : Decidable _<_
decidable [] [] = Dec.map []<[]-⇔ dec-P
decidable [] (y ∷ ys) = yes halt
decidable (x ∷ xs) [] = no λ()
decidable (x ∷ xs) (y ∷ ys) =
Dec.map ∷<∷-⇔ (dec-≺ x y ⊎-dec (dec-≈ x y ×-dec decidable xs ys))