Skip to content

Relations.SRTclosure

Martin Escardo, 3 February 2021.

⋆ Symmetric closure of a relation.

⋆ Iteration of a relation.

⋆ Reflexive-transitive closure of a relation.

⋆ Symmetric-reflexive-transitive closure of a relation.

⋆ propositional, symmetric-reflexive-transitive closure of a relation.

⋆ A special kind of Church-Rosser property.


{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan hiding (_^_)

module Relations.SRTclosure where

open import UF.Subsingletons
open import UF.PropTrunc

open import Naturals.Addition renaming (_+_ to right-addition)


We work with addition defined by induction on the left argument:


_βˆ”_ : β„• β†’ β„• β†’ β„•
m βˆ” n = right-addition n m

_βŠ‘_ : {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ π“₯ Μ‡ ) β†’ (X β†’ X β†’ 𝓦 Μ‡ ) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
R βŠ‘ S = βˆ€ x y β†’ R x y β†’ S x y

is-prop-valued-rel is-equiv-rel : {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡
is-prop-valued-rel A = βˆ€ x y β†’ is-prop (A x y)
is-equiv-rel       A = is-prop-valued-rel A
                     Γ— reflexive A
                     Γ— symmetric A
                     Γ— transitive A

The symmetric closure of a relation A:


module _ {𝓀 : Universe}
         {X : 𝓀 Μ‡ }
         (A : X β†’ X β†’ π“₯ Μ‡ )
       where

 s-closure : X β†’ X β†’ π“₯ Μ‡
 s-closure x y = A x y + A y x

 s-symmetric : symmetric s-closure
 s-symmetric x y (inl a) = inr a
 s-symmetric x y (inr a) = inl a

 s-extension : A βŠ‘ s-closure
 s-extension x y = inl

 s-induction : (R : X β†’ X β†’ 𝓦 Μ‡ )
             β†’ symmetric R
             β†’ A βŠ‘ R
             β†’ s-closure βŠ‘ R
 s-induction R s A-included-in-R x y (inl a) = A-included-in-R x y a
 s-induction R s A-included-in-R x y (inr a) = s y x (A-included-in-R y x a)


To define the reflexive-transitive closure, we first consider the
iteration of a relation B:


module _ {𝓀 : Universe}
         {X : 𝓀 Μ‡ }
         (B : X β†’ X β†’ 𝓀 Μ‡ )
       where

 iteration : β„• β†’ X β†’ X β†’ 𝓀 Μ‡
 iteration 0        x y = x ＝ y
 iteration (succ n) x y = Ξ£ z κž‰ X , B x z Γ— iteration n z y

 iteration-reflexive : (x : X) β†’ iteration 0 x x
 iteration-reflexive x = refl

 iteration-transitive' : (n : β„•) (x y z : X) β†’ iteration n x y β†’ B y z β†’ iteration (succ n) x z
 iteration-transitive' 0        x x z refl        b  = z , b , refl
 iteration-transitive' (succ n) x y z (t , b , c) b' = t , b , iteration-transitive' n t y z c b'

 iteration-transitive'-converse : (n : β„•) (x z : X)
                                β†’ iteration (succ n) x z
                                β†’ Ξ£ y κž‰ X , iteration n x y Γ— B y z
 iteration-transitive'-converse 0        x z (z , b , refl)       = x , refl , b
 iteration-transitive'-converse (succ n) x z (y , b , t , b' , i) = Ξ³
  where
   IH : Ξ£ u κž‰ X , iteration n y u Γ— B u z
   IH = iteration-transitive'-converse n y z (t , b' , i)

   u : X
   u = pr₁ IH

   i' : iteration n y u
   i' = pr₁ (prβ‚‚ IH)

   b'' : B u z
   b'' = prβ‚‚ (prβ‚‚ IH)

   Ξ³ : Ξ£ u κž‰ X , iteration (succ n) x u Γ— B u z
   Ξ³ = u , (y , b , i') , b''

 iteration-symmetric : symmetric B β†’ (m : β„•) β†’ symmetric (iteration m)
 iteration-symmetric sym 0        x x refl        = refl
 iteration-symmetric sym (succ m) x y (z , b , c) = Ξ³
   where
    c' : iteration m y z
    c' = iteration-symmetric sym m z y c

    Ξ³ : iteration (succ m) y x
    Ξ³ = iteration-transitive' m y z x c' (sym x z b)

 iteration-transitive : (m n : β„•) (x y z : X) β†’ iteration m x y β†’ iteration n y z β†’ iteration (m βˆ” n) x z
 iteration-transitive 0        n x x z refl        c' = c'
 iteration-transitive (succ m) n x y z (t , b , c) c' = t , b , iteration-transitive m n t y z c c'


This is regarding the above anonymous module but needs to be outside it:


private
 _^_ : {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ 𝓀 Μ‡ ) β†’ β„• β†’ (X β†’ X β†’ 𝓀 Μ‡ )
 _^_ = iteration


The reflexive-transitive closure of a relation B:


module _ {𝓀 : Universe}
         {X : 𝓀 Μ‡ }
         (B : X β†’ X β†’ 𝓀 Μ‡ )
       where

 rt-closure : X β†’ X β†’ 𝓀 Μ‡
 rt-closure x y = Ξ£ n κž‰ β„• , (B ^ n) x y

 rt-reflexive : reflexive rt-closure
 rt-reflexive x = 0 , refl

 rt-symmetric : symmetric B β†’ symmetric rt-closure
 rt-symmetric s x y (m , c) = m , iteration-symmetric B s m x y c

 rt-transitive : transitive rt-closure
 rt-transitive x y z (m , c) (m' , c') = (m βˆ” m') , iteration-transitive B m m' x y z c c'

 rt-extension : B βŠ‘ rt-closure
 rt-extension x y b = 1 , y , b , refl

 rt-induction : (R : X β†’ X β†’ π“₯ Μ‡ )
              β†’ reflexive R
              β†’ transitive R
              β†’ B βŠ‘ R
              β†’ rt-closure βŠ‘ R
 rt-induction R r t B-included-in-R = Ξ³
  where
   Ξ³ : (x y : X) β†’ rt-closure x y β†’ R x y
   Ξ³ x x (0      , refl)      = r x
   Ξ³ x y (succ n , z , b , c) = t x z y (B-included-in-R x z b) (Ξ³ z y (n , c))


By combining the symmetric closure with the reflective-transitive
closure, we get the symmetric-reflexive-transitive-closure:


module _ {𝓀 : Universe}
         {X : 𝓀 Μ‡ }
         (A : X β†’ X β†’ 𝓀 Μ‡ )
       where

 srt-closure : X β†’ X β†’ 𝓀 Μ‡
 srt-closure = rt-closure (s-closure A)

 srt-symmetric : symmetric srt-closure
 srt-symmetric = rt-symmetric (s-closure A) (s-symmetric A)

 srt-reflexive : reflexive srt-closure
 srt-reflexive = rt-reflexive (s-closure A)

 srt-transitive : transitive srt-closure
 srt-transitive = rt-transitive (s-closure A)

 srt-extension'' : s-closure A βŠ‘ srt-closure
 srt-extension'' = rt-extension (s-closure A)

 srt-extension' : A βŠ‘ s-closure A
 srt-extension' = s-extension A

 srt-extension : A βŠ‘ srt-closure
 srt-extension x y = srt-extension'' x y ∘ srt-extension' x y

 rt-gives-srt : (x y : X) β†’ rt-closure A x y β†’ srt-closure x y
 rt-gives-srt x y (m , i) = g m x y i
  where
   f : (n : β„•) (x y : X) β†’ iteration A n x y β†’ iteration (s-closure A) n x y
   f 0        x x refl        = refl
   f (succ n) x y (z , e , i) = z , inl e , (f n z y i)

   g : (n : β„•) (x y : X) β†’ iteration A n x y β†’ srt-closure x y
   g 0        x x refl        = srt-reflexive x
   g (succ n) x y (z , e , i) = succ n , z , inl e , f n z y i

 srt-induction : (R : X β†’ X β†’ π“₯ Μ‡ )
               β†’ symmetric R
               β†’ reflexive R
               β†’ transitive R
               β†’ A βŠ‘ R
               β†’ srt-closure βŠ‘ R
 srt-induction R s r t A-included-in-R x y = Ξ³
  where
   Ξ΄ : s-closure A βŠ‘ R
   Ξ΄ = s-induction A R s A-included-in-R

   Ξ³ : srt-closure x y β†’ R x y
   Ξ³ = rt-induction (s-closure A) R r t Ξ΄ x y


The proposition-valued, symmetric-reflexive-transitive closure of a
relation A:


module psrt
        (pt : propositional-truncations-exist)
        {𝓀 : Universe}
        {X : 𝓀 Μ‡ }
        (A : X β†’ X β†’ 𝓀 Μ‡ )
       where

 open PropositionalTruncation pt

 psrt-closure : X β†’ X β†’ 𝓀 Μ‡
 psrt-closure x y = βˆ₯ srt-closure A x y βˆ₯

 psrt-is-prop-valued : (x y : X) β†’ is-prop (psrt-closure x y)
 psrt-is-prop-valued x y = βˆ₯βˆ₯-is-prop

 psrt-symmetric : symmetric psrt-closure
 psrt-symmetric x y = βˆ₯βˆ₯-functor (srt-symmetric A x y)

 psrt-reflexive : reflexive psrt-closure
 psrt-reflexive x = ∣ srt-reflexive A x ∣

 psrt-transitive : transitive psrt-closure
 psrt-transitive x y z = βˆ₯βˆ₯-functorβ‚‚ (srt-transitive A x y z)

 psrt-extension : A βŠ‘ psrt-closure
 psrt-extension x y a = βˆ₯βˆ₯-functor (srt-extension A x y) ∣ a ∣

 psrt-induction : (R : X β†’ X β†’ π“₯ Μ‡ )
                β†’ ((x y : X) β†’ is-prop (R x y))
                β†’ reflexive R
                β†’ symmetric R
                β†’ transitive R
                β†’ A βŠ‘ R
                β†’ psrt-closure βŠ‘ R
 psrt-induction R p r s t A-included-in-R x y =
  βˆ₯βˆ₯-rec (p x y) (srt-induction A R s r t A-included-in-R x y)

 psrt-is-equiv-rel : is-equiv-rel psrt-closure
 psrt-is-equiv-rel = psrt-is-prop-valued ,
                     psrt-reflexive ,
                     psrt-symmetric ,
                     psrt-transitive

Any proposition-valued relation that is logically equivalent to an
equivalence relation is itself an equivalence relation. Unfortunately,
we cannot use univalence to perform this transport as the types live
in different universes.


is-equiv-rel-transport : {X : 𝓀 Μ‡ }
                         (A : X β†’ X β†’ π“₯ Μ‡ )
                         (B : X β†’ X β†’ 𝓦 Μ‡ )
                       β†’ is-prop-valued-rel B
                       β†’ ((x y : X) β†’ A x y ↔ B x y)
                       β†’ is-equiv-rel A
                       β†’ is-equiv-rel B
is-equiv-rel-transport {X} A B p' e (p , r , s , t) = (p' , r' , s' , t')
 where
  r' : reflexive B
  r' x = lr-implication (e x x) (r x)

  s' : symmetric B
  s' x y b = lr-implication (e y x) (s x y (rl-implication (e x y) b))

  t' : transitive B
  t' x y z b b' = lr-implication (e x z)
                    (t x y z (rl-implication (e x y) b)
                             (rl-implication (e y z) b'))