------------------------------------------------------------------------
-- 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 using (⊥; ⊥-elim)
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.Decidable.Core using (yes; no)
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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4