module Data.Star where
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Function
import Relation.Binary.PreorderReasoning as PreR
infixr 5 _◅_
data Star {I : Set} (T : Rel I) : Rel I where
ε : Reflexive (Star T)
_◅_ : ∀ {i j k} (x : T i j) (xs : Star T j k) → Star T i k
infixr 5 _◅◅_
_◅◅_ : ∀ {I} {T : Rel I} → Transitive (Star T)
ε ◅◅ ys = ys
(x ◅ xs) ◅◅ ys = x ◅ (xs ◅◅ ys)
◅◅-assoc : ∀ {I} {T : Rel I} {i j k l}
(xs : Star T i j) (ys : Star T j k)
(zs : Star T k l) →
(xs ◅◅ ys) ◅◅ zs ≡ xs ◅◅ (ys ◅◅ zs)
◅◅-assoc ε ys zs = ≡-refl
◅◅-assoc (x ◅ xs) ys zs = ≡-cong (_◅_ x) (◅◅-assoc xs ys zs)
infixl 5 _▻_
_▻_ : ∀ {I} {T : Rel I} {i j k} →
Star T j k → T i j → Star T i k
_▻_ = flip _◅_
infixr 5 _▻▻_
_▻▻_ : ∀ {I} {T : Rel I} {i j k} →
Star T j k → Star T i j → Star T i k
_▻▻_ = flip _◅◅_
gmap : ∀ {I} {T : Rel I} {J} {U : Rel J} →
(f : I → J) → T =[ f ]⇒ U → Star T =[ f ]⇒ Star U
gmap f g ε = ε
gmap f g (x ◅ xs) = g x ◅ gmap f g xs
map : ∀ {I} {T U : Rel I} → T ⇒ U → Star T ⇒ Star U
map = gmap id
gfold : ∀ {I J T} (f : I → J) P →
Trans T (P on₁ f) (P on₁ f) → Reflexive (P on₁ f) →
Star T =[ f ]⇒ P
gfold f P _⊕_ ∅ ε = ∅
gfold f P _⊕_ ∅ (x ◅ xs) = x ⊕ gfold f P _⊕_ ∅ xs
fold : ∀ {I T} (P : Rel I) →
Trans T P P → Reflexive P → Star T ⇒ P
fold = gfold id
gfoldl : ∀ {I J T} (f : I → J) P →
Trans (P on₁ f) T (P on₁ f) →
Trans (P on₁ f) (Star T) (P on₁ f)
gfoldl f P _⊕_ ∅ ε = ∅
gfoldl f P _⊕_ ∅ (x ◅ xs) = gfoldl f P _⊕_ (∅ ⊕ x) xs
foldl : ∀ {I T} (P : Rel I) →
Trans P T P →
Trans P (Star T) P
foldl = gfoldl id
concat : ∀ {I} {T : Rel I} → Star (Star T) ⇒ Star T
concat {T = T} = fold (Star T) _◅◅_ ε
revApp : ∀ {I} {T U : Rel I} → Sym T U →
∀ {i j k} → Star T j i → Star U j k → Star U i k
revApp rev ε ys = ys
revApp rev (x ◅ xs) ys = revApp rev xs (rev x ◅ ys)
reverse : ∀ {I} {T U : Rel I} → Sym T U → Sym (Star T) (Star U)
reverse rev xs = revApp rev xs ε
return : ∀ {I} {T : Rel I} → T ⇒ Star T
return x = x ◅ ε
kleisliStar : ∀ {I J} {T : Rel I} {U : Rel J} (f : I → J) →
T =[ f ]⇒ Star U → Star T =[ f ]⇒ Star U
kleisliStar f g = concat ∘ gmap f g
_⋆ : ∀ {I} {T U : Rel I} →
T ⇒ Star U → Star T ⇒ Star U
_⋆ = kleisliStar id
infixl 1 _>>=_
_>>=_ : ∀ {I} {T U : Rel I} {i j} →
Star T i j → T ⇒ Star U → Star U i j
m >>= f = (f ⋆) m
starPreorder : ∀ {I} (T : Rel I) → Preorder
starPreorder {I} T = record
{ carrier = I
; _≈_ = _≡_
; _∼_ = Star T
; isPreorder = record
{ isEquivalence = ≡-isEquivalence
; reflexive = reflexive
; trans = _◅◅_
; ≈-resp-∼ = ≡-resp (Star T)
}
}
where
reflexive : _≡_ ⇒ Star T
reflexive ≡-refl = ε
module StarReasoning {I : Set} (T : Rel I) where
open PreR (starPreorder T) public
renaming (_∼⟨_⟩_ to _⟶⋆⟨_⟩_)
infixr 2 _⟶⟨_⟩_
_⟶⟨_⟩_ : ∀ x {y z} → T x y → y IsRelatedTo z → x IsRelatedTo z
x ⟶⟨ x⟶y ⟩ y⟶⋆z = x ⟶⋆⟨ x⟶y ◅ ε ⟩ y⟶⋆z