------------------------------------------------------------------------
-- The Agda standard library
--
-- Transitive closures
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Binary.Construct.Closure.Transitive where
open import Function.Base using (id; _∘_; _∋_)
open import Function.Bundles using (_⇔_; mk⇔)
open import Induction.WellFounded
open import Level using (Level; _⊔_)
open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_)
open import Relation.Binary.Definitions
using (Reflexive; Symmetric; Transitive)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
private
variable
a ℓ ℓ₁ ℓ₂ : Level
A B : Set a
------------------------------------------------------------------------
-- Definition
infixr 5 _∷_
infix 4 TransClosure
data TransClosure {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
[_] : ∀ {x y} (x∼y : x ∼ y) → TransClosure _∼_ x y
_∷_ : ∀ {x y z} (x∼y : x ∼ y) (y∼⁺z : TransClosure _∼_ y z) → TransClosure _∼_ x z
syntax TransClosure R x y = x ⟨ R ⟩⁺ y
------------------------------------------------------------------------
-- Operations
module _ {_∼_ : Rel A ℓ} where
private
_∼⁺_ = TransClosure _∼_
infixr 5 _∷ʳ_
_∷ʳ_ : ∀ {x y z} → (x∼⁺y : x ∼⁺ y) (y∼z : y ∼ z) → x ∼⁺ z
[ x∼y ] ∷ʳ y∼z = x∼y ∷ [ y∼z ]
(x∼y ∷ x∼⁺y) ∷ʳ y∼z = x∼y ∷ (x∼⁺y ∷ʳ y∼z)
infixr 5 _++_
_++_ : ∀ {x y z} → x ∼⁺ y → y ∼⁺ z → x ∼⁺ z
[ x∼y ] ++ y∼⁺z = x∼y ∷ y∼⁺z
(x∼y ∷ y∼⁺z) ++ z∼⁺u = x∼y ∷ (y∼⁺z ++ z∼⁺u)
------------------------------------------------------------------------
-- Properties
module _ (_∼_ : Rel A ℓ) where
private
_∼⁺_ = TransClosure _∼_
module ∼⊆∼⁺ = Subrelation {_<₂_ = _∼⁺_} [_]
reflexive : Reflexive _∼_ → Reflexive _∼⁺_
reflexive refl = [ refl ]
symmetric : Symmetric _∼_ → Symmetric _∼⁺_
symmetric sym [ x∼y ] = [ sym x∼y ]
symmetric sym (x∼y ∷ y∼⁺z) = symmetric sym y∼⁺z ∷ʳ sym x∼y
transitive : Transitive _∼⁺_
transitive = _++_
transitive⁻ : Transitive _∼_ → _∼⁺_ ⇒ _∼_
transitive⁻ trans [ x∼y ] = x∼y
transitive⁻ trans (x∼y ∷ x∼⁺y) = trans x∼y (transitive⁻ trans x∼⁺y)
accessible⁻ : ∀ {x} → Acc _∼⁺_ x → Acc _∼_ x
accessible⁻ = ∼⊆∼⁺.accessible
wellFounded⁻ : WellFounded _∼⁺_ → WellFounded _∼_
wellFounded⁻ = ∼⊆∼⁺.wellFounded
accessible : ∀ {x} → Acc _∼_ x → Acc _∼⁺_ x
accessible acc[x] = acc (wf-acc acc[x])
where
wf-acc : ∀ {x} → Acc _∼_ x → WfRec _∼⁺_ (Acc _∼⁺_) x
wf-acc (acc rec) [ y∼x ] = acc (wf-acc (rec y∼x))
wf-acc acc[x] (y∼z ∷ z∼⁺x) = acc-inverse (wf-acc acc[x] z∼⁺x) [ y∼z ]
wellFounded : WellFounded _∼_ → WellFounded _∼⁺_
wellFounded wf x = accessible (wf x)
------------------------------------------------------------------------
-- Alternative definition of transitive closure
infix 4 Plus
syntax Plus R x y = x [ R ]⁺ y
data Plus {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
[_] : ∀ {x y} (x∼y : x ∼ y) → x [ _∼_ ]⁺ y
_∼⁺⟨_⟩_ : ∀ x {y z} (x∼⁺y : x [ _∼_ ]⁺ y) (y∼⁺z : y [ _∼_ ]⁺ z) →
x [ _∼_ ]⁺ z
module _ {_∼_ : Rel A ℓ} where
[]-injective : ∀ {x y p q} → (x [ _∼_ ]⁺ y ∋ [ p ]) ≡ [ q ] → p ≡ q
[]-injective ≡.refl = ≡.refl
-- See also ∼⁺⟨⟩-injectiveˡ and ∼⁺⟨⟩-injectiveʳ in
-- Relation.Binary.Construct.Closure.Transitive.WithK.
-- "Equational" reasoning notation. Example:
--
-- lemma =
-- x ∼⁺⟨ [ lemma₁ ] ⟩
-- y ∼⁺⟨ lemma₂ ⟩∎
-- z ∎
finally : ∀ {_∼_ : Rel A ℓ} x y → x [ _∼_ ]⁺ y → x [ _∼_ ]⁺ y
finally _ _ = id
syntax finally x y x∼⁺y = x ∼⁺⟨ x∼⁺y ⟩∎ y ∎
infixr 2 _∼⁺⟨_⟩_
infix 3 finally
-- Map.
map : {_R₁_ : Rel A ℓ} {_R₂_ : Rel B ℓ₂} {f : A → B} →
_R₁_ =[ f ]⇒ _R₂_ → Plus _R₁_ =[ f ]⇒ Plus _R₂_
map R₁⇒R₂ [ xRy ] = [ R₁⇒R₂ xRy ]
map R₁⇒R₂ (x ∼⁺⟨ xR⁺z ⟩ zR⁺y) =
_ ∼⁺⟨ map R₁⇒R₂ xR⁺z ⟩ map R₁⇒R₂ zR⁺y
-- Plus and TransClosure are equivalent.
equivalent : ∀ {_∼_ : Rel A ℓ} {x y} →
Plus _∼_ x y ⇔ TransClosure _∼_ x y
equivalent {_∼_ = _∼_} = mk⇔ complete sound
where
complete : Plus _∼_ ⇒ TransClosure _∼_
complete [ x∼y ] = [ x∼y ]
complete (x ∼⁺⟨ x∼⁺y ⟩ y∼⁺z) = complete x∼⁺y ++ complete y∼⁺z
sound : TransClosure _∼_ ⇒ Plus _∼_
sound [ x∼y ] = [ x∼y ]
sound (x∼y ∷ y∼⁺z) = _ ∼⁺⟨ [ x∼y ] ⟩ sound y∼⁺z
------------------------------------------------------------------------
-- Deprecations
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- v1.5
Plus′ = TransClosure
{-# WARNING_ON_USAGE Plus′
"Warning: Plus′ was deprecated in v1.5.
Please use TransClosure 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