------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on characters
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Char.Properties where
open import Data.Bool.Base using (Bool)
open import Data.Char.Base using (Char; _≈_; _≉_; _<_; _≤_; toℕ)
import Data.Nat.Base as ℕ using (ℕ; _<_; _≤_)
import Data.Nat.Properties as ℕ
using (_<?_; <-cmp; <-isStrictPartialOrder; <-isStrictTotalOrder
; <-strictPartialOrder; <-strictTotalOrder; <-irrefl; <-trans; <-asym
; _≟_)
open import Data.Product.Base using (_,_)
open import Function.Base using (const; _∘′_)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Nullary.Decidable using (map′; isYes)
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.Bundles
using (Setoid; DecSetoid; StrictPartialOrder; StrictTotalOrder; Preorder
; Poset; DecPoset)
open import Relation.Binary.Structures
using (IsDecEquivalence; IsStrictPartialOrder; IsStrictTotalOrder
; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsEquivalence)
open import Relation.Binary.Definitions
using (Decidable; DecidableEquality; Trichotomous; Irreflexive
; Transitive; Asymmetric; Antisymmetric; Symmetric; Substitutive
; Reflexive; tri<; tri≈; tri>)
import Relation.Binary.Construct.On as On
using (decidable; transitive; asymmetric; isStrictPartialOrder
; isStrictTotalOrder; strictPartialOrder; strictTotalOrder)
import Relation.Binary.Construct.Closure.Reflexive as Refl
using (Refl; reflexive)
import Relation.Binary.Construct.Closure.Reflexive.Properties as Refl
using (trans; antisym; decidable)
open import Relation.Binary.PropositionalEquality.Core as ≡
using (_≡_; _≢_; refl; cong; sym; trans; subst)
import Relation.Binary.PropositionalEquality.Properties as ≡ using
(isDecEquivalence; setoid; decSetoid; isEquivalence)
------------------------------------------------------------------------
-- Primitive properties
open import Agda.Builtin.Char.Properties
renaming ( primCharToNatInjective to toℕ-injective)
public
------------------------------------------------------------------------
-- Properties of _≈_
≈⇒≡ : _≈_ ⇒ _≡_
≈⇒≡ = toℕ-injective _ _
≉⇒≢ : _≉_ ⇒ _≢_
≉⇒≢ p refl = p refl
≈-reflexive : _≡_ ⇒ _≈_
≈-reflexive = cong toℕ
------------------------------------------------------------------------
-- Properties of _≡_
infix 4 _≟_
_≟_ : DecidableEquality Char
x ≟ y = map′ ≈⇒≡ ≈-reflexive (toℕ x ℕ.≟ toℕ y)
setoid : Setoid _ _
setoid = ≡.setoid Char
decSetoid : DecSetoid _ _
decSetoid = ≡.decSetoid _≟_
isDecEquivalence : IsDecEquivalence _≡_
isDecEquivalence = ≡.isDecEquivalence _≟_
------------------------------------------------------------------------
-- Boolean equality test.
--
-- Why is the definition _==_ = primCharEquality not used? One reason
-- is that the present definition can sometimes improve type
-- inference, at least with the version of Agda that is current at the
-- time of writing: see unit-test below.
infix 4 _==_
_==_ : Char → Char → Bool
c₁ == c₂ = isYes (c₁ ≟ c₂)
private
-- The following unit test does not type-check (at the time of
-- writing) if _==_ is replaced by primCharEquality.
data P : (Char → Bool) → Set where
MkP : (c : Char) → P (c ==_)
unit-test : P ('x' ==_)
unit-test = MkP _
------------------------------------------------------------------------
-- Properties of _<_
infix 4 _<?_
_<?_ : Decidable _<_
_<?_ = On.decidable toℕ ℕ._<_ ℕ._<?_
<-cmp : Trichotomous _≡_ _<_
<-cmp c d with ℕ.<-cmp (toℕ c) (toℕ d)
... | tri< lt ¬eq ¬gt = tri< lt (≉⇒≢ ¬eq) ¬gt
... | tri≈ ¬lt eq ¬gt = tri≈ ¬lt (≈⇒≡ eq) ¬gt
... | tri> ¬lt ¬eq gt = tri> ¬lt (≉⇒≢ ¬eq) gt
<-irrefl : Irreflexive _≡_ _<_
<-irrefl = ℕ.<-irrefl ∘′ cong toℕ
<-trans : Transitive _<_
<-trans {c} {d} {e} = On.transitive toℕ ℕ._<_ ℕ.<-trans {c} {d} {e}
<-asym : Asymmetric _<_
<-asym {c} {d} = On.asymmetric toℕ ℕ._<_ ℕ.<-asym {c} {d}
<-isStrictPartialOrder : IsStrictPartialOrder _≡_ _<_
<-isStrictPartialOrder = record
{ isEquivalence = ≡.isEquivalence
; irrefl = <-irrefl
; trans = λ {a} {b} {c} → <-trans {a} {b} {c}
; <-resp-≈ = (λ {c} → ≡.subst (c <_))
, (λ {c} → ≡.subst (_< c))
}
<-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
<-isStrictTotalOrder = record
{ isStrictPartialOrder = <-isStrictPartialOrder
; compare = <-cmp
}
<-strictPartialOrder : StrictPartialOrder _ _ _
<-strictPartialOrder = record
{ isStrictPartialOrder = <-isStrictPartialOrder
}
<-strictTotalOrder : StrictTotalOrder _ _ _
<-strictTotalOrder = record
{ isStrictTotalOrder = <-isStrictTotalOrder
}
------------------------------------------------------------------------
-- Properties of _≤_
infix 4 _≤?_
_≤?_ : Decidable _≤_
_≤?_ = Refl.decidable <-cmp
≤-reflexive : _≡_ ⇒ _≤_
≤-reflexive = Refl.reflexive
≤-trans : Transitive _≤_
≤-trans = Refl.trans (λ {a} {b} {c} → <-trans {a} {b} {c})
≤-antisym : Antisymmetric _≡_ _≤_
≤-antisym = Refl.antisym _≡_ refl ℕ.<-asym
≤-isPreorder : IsPreorder _≡_ _≤_
≤-isPreorder = record
{ isEquivalence = ≡.isEquivalence
; reflexive = ≤-reflexive
; trans = ≤-trans
}
≤-isPartialOrder : IsPartialOrder _≡_ _≤_
≤-isPartialOrder = record
{ isPreorder = ≤-isPreorder
; antisym = ≤-antisym
}
≤-isDecPartialOrder : IsDecPartialOrder _≡_ _≤_
≤-isDecPartialOrder = record
{ isPartialOrder = ≤-isPartialOrder
; _≟_ = _≟_
; _≤?_ = _≤?_
}
≤-preorder : Preorder _ _ _
≤-preorder = record { isPreorder = ≤-isPreorder }
≤-poset : Poset _ _ _
≤-poset = record { isPartialOrder = ≤-isPartialOrder }
≤-decPoset : DecPoset _ _ _
≤-decPoset = record { isDecPartialOrder = ≤-isDecPartialOrder }
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 1.5
≈-refl : Reflexive _≈_
≈-refl = refl
{-# WARNING_ON_USAGE ≈-refl
"Warning: ≈-refl was deprecated in v1.5.
Please use Propositional Equality's refl instead."
#-}
≈-sym : Symmetric _≈_
≈-sym = sym
{-# WARNING_ON_USAGE ≈-sym
"Warning: ≈-sym was deprecated in v1.5.
Please use Propositional Equality's sym instead."
#-}
≈-trans : Transitive _≈_
≈-trans = trans
{-# WARNING_ON_USAGE ≈-trans
"Warning: ≈-trans was deprecated in v1.5.
Please use Propositional Equality's trans instead."
#-}
≈-subst : ∀ {ℓ} → Substitutive _≈_ ℓ
≈-subst P x≈y p = subst P (≈⇒≡ x≈y) p
{-# WARNING_ON_USAGE ≈-subst
"Warning: ≈-subst was deprecated in v1.5.
Please use Propositional Equality's subst instead."
#-}
infix 4 _≈?_
_≈?_ : Decidable _≈_
x ≈? y = toℕ x ℕ.≟ toℕ y
≈-isEquivalence : IsEquivalence _≈_
≈-isEquivalence = record
{ refl = refl
; sym = sym
; trans = trans
}
≈-setoid : Setoid _ _
≈-setoid = record
{ isEquivalence = ≈-isEquivalence
}
≈-isDecEquivalence : IsDecEquivalence _≈_
≈-isDecEquivalence = record
{ isEquivalence = ≈-isEquivalence
; _≟_ = _≈?_
}
≈-decSetoid : DecSetoid _ _
≈-decSetoid = record
{ isDecEquivalence = ≈-isDecEquivalence
}
{-# WARNING_ON_USAGE _≈?_
"Warning: _≈?_ was deprecated in v1.5.
Please use _≟_ instead."
#-}
{-# WARNING_ON_USAGE ≈-isEquivalence
"Warning: ≈-isEquivalence was deprecated in v1.5.
Please use Propositional Equality's isEquivalence instead."
#-}
{-# WARNING_ON_USAGE ≈-setoid
"Warning: ≈-setoid was deprecated in v1.5.
Please use Propositional Equality's setoid instead."
#-}
{-# WARNING_ON_USAGE ≈-isDecEquivalence
"Warning: ≈-isDecEquivalence was deprecated in v1.5.
Please use Propositional Equality's isDecEquivalence instead."
#-}
{-# WARNING_ON_USAGE ≈-decSetoid
"Warning: ≈-decSetoid was deprecated in v1.5.
Please use Propositional Equality's decSetoid instead."
#-}
≡-setoid : Setoid _ _
≡-setoid = setoid
{-# WARNING_ON_USAGE ≡-setoid
"Warning: ≡-setoid was deprecated in v1.5.
Please use setoid instead."
#-}
≡-decSetoid : DecSetoid _ _
≡-decSetoid = decSetoid
{-# WARNING_ON_USAGE ≡-decSetoid
"Warning: ≡-decSetoid was deprecated in v1.5.
Please use decSetoid instead."
#-}
<-isStrictPartialOrder-≈ : IsStrictPartialOrder _≈_ _<_
<-isStrictPartialOrder-≈ = On.isStrictPartialOrder toℕ ℕ.<-isStrictPartialOrder
{-# WARNING_ON_USAGE <-isStrictPartialOrder-≈
"Warning: <-isStrictPartialOrder-≈ was deprecated in v1.5.
Please use <-isStrictPartialOrder instead."
#-}
<-isStrictTotalOrder-≈ : IsStrictTotalOrder _≈_ _<_
<-isStrictTotalOrder-≈ = On.isStrictTotalOrder toℕ ℕ.<-isStrictTotalOrder
{-# WARNING_ON_USAGE <-isStrictTotalOrder-≈
"Warning: <-isStrictTotalOrder-≈ was deprecated in v1.5.
Please use <-isStrictTotalOrder instead."
#-}
<-strictPartialOrder-≈ : StrictPartialOrder _ _ _
<-strictPartialOrder-≈ = On.strictPartialOrder ℕ.<-strictPartialOrder toℕ
{-# WARNING_ON_USAGE <-strictPartialOrder-≈
"Warning: <-strictPartialOrder-≈ was deprecated in v1.5.
Please use <-strictPartialOrder instead."
#-}
<-strictTotalOrder-≈ : StrictTotalOrder _ _ _
<-strictTotalOrder-≈ = On.strictTotalOrder ℕ.<-strictTotalOrder toℕ
{-# WARNING_ON_USAGE <-strictTotalOrder-≈
"Warning: <-strictTotalOrder-≈ was deprecated in v1.5.
Please use <-strictTotalOrder instead."
#-}
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