------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic ordering of lists
------------------------------------------------------------------------
-- 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.List.Relation.Binary.Lex.NonStrict where
open import Data.Empty using (⊥)
open import Data.Unit.Base using (⊤; tt)
open import Data.List.Base using (List; []; _∷_)
open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
open import Function.Base using (const; id)
import Data.List.Relation.Binary.Lex.Strict as Strict
open import Level using (Level; _⊔_)
open import Relation.Nullary.Negation.Core using (¬_)
open import Relation.Nullary using (yes; no)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Bundles
open import Relation.Binary.Structures
using (IsEquivalence; IsPartialOrder; IsStrictPartialOrder; IsTotalOrder
; IsStrictTotalOrder; IsPreorder; IsDecTotalOrder)
open import Relation.Binary.Definitions
using (Irreflexive; _Respects₂_; Antisymmetric; Asymmetric; Symmetric
; Transitive; Decidable; Total; Trichotomous)
import Relation.Binary.Construct.NonStrictToStrict as Conv
import Data.List.Relation.Binary.Lex as Core
------------------------------------------------------------------------
-- Publically re-export definitions from Core
open Core public
using (base; halt; this; next; ²-this; ²-next)
------------------------------------------------------------------------
-- Strict lexicographic ordering.
module _ {a ℓ₁ ℓ₂} {A : Set a} where
Lex-< : (_≈_ : Rel A ℓ₁) (_≼_ : Rel A ℓ₂) → Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂)
Lex-< _≈_ _≼_ = Core.Lex ⊥ _≈_ (Conv._<_ _≈_ _≼_)
-- Properties
module _ {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂} where
private
_≋_ = Pointwise _≈_
_<_ = Lex-< _≈_ _≼_
<-irreflexive : Irreflexive _≋_ _<_
<-irreflexive = Strict.<-irreflexive (Conv.<-irrefl _≈_ _≼_)
<-asymmetric : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ →
Antisymmetric _≈_ _≼_ → Asymmetric _<_
<-asymmetric eq resp antisym =
Strict.<-asymmetric sym (Conv.<-resp-≈ _ _ eq resp)
(Conv.<-asym _≈_ _ antisym)
where open IsEquivalence eq
<-antisymmetric : Symmetric _≈_ → Antisymmetric _≈_ _≼_ →
Antisymmetric _≋_ _<_
<-antisymmetric sym antisym =
Core.antisymmetric sym
(Conv.<-irrefl _≈_ _≼_)
(Conv.<-asym _ _≼_ antisym)
<-transitive : IsPartialOrder _≈_ _≼_ → Transitive _<_
<-transitive po =
Core.transitive isEquivalence
(Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
(Conv.<-trans _ _≼_ po)
where open IsPartialOrder po
<-resp₂ : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ → _<_ Respects₂ _≋_
<-resp₂ eq resp = Core.respects₂ eq (Conv.<-resp-≈ _ _ eq resp)
<-compare : Symmetric _≈_ → Decidable _≈_ → Antisymmetric _≈_ _≼_ →
Total _≼_ → Trichotomous _≋_ _<_
<-compare sym _≟_ antisym tot =
Strict.<-compare sym (Conv.<-trichotomous _ _ sym _≟_ antisym tot)
<-decidable : Decidable _≈_ → Decidable _≼_ → Decidable _<_
<-decidable _≟_ _≼?_ =
Core.decidable (no id) _≟_ (Conv.<-decidable _ _ _≟_ _≼?_)
<-isStrictPartialOrder : IsPartialOrder _≈_ _≼_ →
IsStrictPartialOrder _≋_ _<_
<-isStrictPartialOrder po =
Strict.<-isStrictPartialOrder
(Conv.<-isStrictPartialOrder _ _ po)
<-isStrictTotalOrder : Decidable _≈_ → IsTotalOrder _≈_ _≼_ →
IsStrictTotalOrder _≋_ _<_
<-isStrictTotalOrder dec tot =
Strict.<-isStrictTotalOrder
(Conv.<-isStrictTotalOrder₁ _ _ dec tot)
<-strictPartialOrder : ∀ {a ℓ₁ ℓ₂} → Poset a ℓ₁ ℓ₂ →
StrictPartialOrder _ _ _
<-strictPartialOrder po = record
{ isStrictPartialOrder = <-isStrictPartialOrder isPartialOrder
} where open Poset po
<-strictTotalOrder : ∀ {a ℓ₁ ℓ₂} → DecTotalOrder a ℓ₁ ℓ₂ →
StrictTotalOrder _ _ _
<-strictTotalOrder dtot = record
{ isStrictTotalOrder = <-isStrictTotalOrder _≟_ isTotalOrder
} where open DecTotalOrder dtot
------------------------------------------------------------------------
-- Non-strict lexicographic ordering.
module _ {a ℓ₁ ℓ₂} {A : Set a} where
Lex-≤ : (_≈_ : Rel A ℓ₁) (_≼_ : Rel A ℓ₂) → Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂)
Lex-≤ _≈_ _≼_ = Core.Lex ⊤ _≈_ (Conv._<_ _≈_ _≼_)
≤-reflexive : ∀ _≈_ _≼_ → Pointwise _≈_ ⇒ Lex-≤ _≈_ _≼_
≤-reflexive _≈_ _≼_ = Strict.≤-reflexive _≈_ (Conv._<_ _≈_ _≼_)
-- Properties
module _ {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂} where
private
_≋_ = Pointwise _≈_
_≤_ = Lex-≤ _≈_ _≼_
≤-antisymmetric : Symmetric _≈_ → Antisymmetric _≈_ _≼_ →
Antisymmetric _≋_ _≤_
≤-antisymmetric sym antisym =
Core.antisymmetric sym
(Conv.<-irrefl _≈_ _≼_)
(Conv.<-asym _ _≼_ antisym)
≤-transitive : IsPartialOrder _≈_ _≼_ → Transitive _≤_
≤-transitive po =
Core.transitive isEquivalence
(Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
(Conv.<-trans _ _≼_ po)
where open IsPartialOrder po
≤-resp₂ : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ → _≤_ Respects₂ _≋_
≤-resp₂ eq resp = Core.respects₂ eq (Conv.<-resp-≈ _ _ eq resp)
≤-decidable : Decidable _≈_ → Decidable _≼_ → Decidable _≤_
≤-decidable _≟_ _≼?_ =
Core.decidable (yes tt) _≟_ (Conv.<-decidable _ _ _≟_ _≼?_)
≤-total : Symmetric _≈_ → Decidable _≈_ → Antisymmetric _≈_ _≼_ →
Total _≼_ → Total _≤_
≤-total sym dec-≈ antisym tot =
Strict.≤-total sym (Conv.<-trichotomous _ _ sym dec-≈ antisym tot)
≤-isPreorder : IsPartialOrder _≈_ _≼_ → IsPreorder _≋_ _≤_
≤-isPreorder po =
Strict.≤-isPreorder
isEquivalence (Conv.<-trans _ _ po)
(Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
where open IsPartialOrder po
≤-isPartialOrder : IsPartialOrder _≈_ _≼_ → IsPartialOrder _≋_ _≤_
≤-isPartialOrder po =
Strict.≤-isPartialOrder
(Conv.<-isStrictPartialOrder _ _ po)
≤-isTotalOrder : Decidable _≈_ → IsTotalOrder _≈_ _≼_ →
IsTotalOrder _≋_ _≤_
≤-isTotalOrder dec tot =
Strict.≤-isTotalOrder
(Conv.<-isStrictTotalOrder₁ _ _ dec tot)
≤-isDecTotalOrder : IsDecTotalOrder _≈_ _≼_ →
IsDecTotalOrder _≋_ _≤_
≤-isDecTotalOrder dtot =
Strict.≤-isDecTotalOrder
(Conv.<-isStrictTotalOrder₂ _ _ dtot)
≤-preorder : ∀ {a ℓ₁ ℓ₂} → Poset a ℓ₁ ℓ₂ → Preorder _ _ _
≤-preorder po = record
{ isPreorder = ≤-isPreorder isPartialOrder
} where open Poset po
≤-partialOrder : ∀ {a ℓ₁ ℓ₂} → Poset a ℓ₁ ℓ₂ → Poset _ _ _
≤-partialOrder po = record
{ isPartialOrder = ≤-isPartialOrder isPartialOrder
} where open Poset po
≤-decTotalOrder : ∀ {a ℓ₁ ℓ₂} → DecTotalOrder a ℓ₁ ℓ₂ →
DecTotalOrder _ _ _
≤-decTotalOrder dtot = record
{ isDecTotalOrder = ≤-isDecTotalOrder isDecTotalOrder
} where open DecTotalOrder dtot
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