------------------------------------------------------------------------
-- Unary and binary relations
------------------------------------------------------------------------

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

module Relation where

open import Equality.Propositional
open import Prelude

open import Bijection equality-with-J as Bijection using (_↔_)
open import Equality.Decision-procedures equality-with-J
import Equality.Groupoid equality-with-J as EG
open import Function-universe equality-with-J hiding (id; _∘_)
open import Groupoid equality-with-J

-- Unary relations.

Rel : ∀ {ℓ₁} ℓ₂ → Set ℓ₁ → Set (ℓ₁ ⊔ lsuc ℓ₂)
Rel ℓ A = A → Set ℓ

-- Homogeneous binary relations.

Rel₂ : ∀ {ℓ₁} ℓ₂ → Set ℓ₁ → Set (ℓ₁ ⊔ lsuc ℓ₂)
Rel₂ ℓ A = Rel ℓ (A × A)

-- One kind of unary relation transformer.

Trans : ∀ {a} ℓ → Set a → Set (a ⊔ lsuc ℓ)
Trans ℓ A = Rel ℓ A → Rel ℓ A

-- One kind of binary relation transformer.

Trans₂ : ∀ {a} ℓ → Set a → Set (a ⊔ lsuc ℓ)
Trans₂ ℓ A = Trans ℓ (A × A)

-- The converse of a binary relation.

infixr  _⁻¹

_⁻¹ : ∀ {a ℓ} {A : Set a} → Rel₂ ℓ A → Rel₂ ℓ A
R ⁻¹ = R ∘ swap

-- Composition of binary relations.

infixr  _⊙_

_⊙_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} →
      Rel₂ ℓ₁ A → Rel₂ ℓ₂ A → Rel₂ (a ⊔ ℓ₁ ⊔ ℓ₂) A
(R ⊙ S) (x , z) = ∃ λ y → R (x , y) × S (y , z)

-- Composition of a relation with itself, with the base case as a
-- parameter.

composition : ∀ {a} {A : Set a} →
              Rel₂ a A → Rel₂ a A → ℕ → Rel₂ a A
composition R S zero    = R
composition R S (suc n) = S ⊙ composition R S n

-- Composition of a binary relation with itself, with the relation
-- itself as the base case.

infix  _^^[1+_]

_^^[1+_] : ∀ {a} {A : Set a} →
           Rel₂ a A → ℕ → Rel₂ a A
R ^^[1+ n ] = composition R R n

-- Composition of a binary relation with itself, with equality as the
-- base case.

infix  _^^_

_^^_ : ∀ {a} {A : Set a} →
       Rel₂ a A → ℕ → Rel₂ a A
R ^^ n = composition (uncurry _≡_) R n

-- Intersection of relations.

infixr  _∩_

_∩_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} →
      Rel ℓ₁ A → Rel ℓ₂ A → Rel (ℓ₁ ⊔ ℓ₂) A
R ∩ S = λ x → R x × S x

-- Union of relations.

infixr  _∪_

_∪_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} →
      Rel ℓ₁ A → Rel ℓ₂ A → Rel (ℓ₁ ⊔ ℓ₂) A
R ∪ S = λ x → R x ⊎ S x

-- Reflexive closure of binary relations.

_⁼ : ∀ {a ℓ} {A : Set a} →
     Rel₂ ℓ A → Rel₂ (a ⊔ ℓ) A
R ⁼ = R ∪ uncurry _≡_

-- Transitive closure of binary relations.

_⁺ : ∀ {a} {A : Set a} →
     Rel₂ a A → Rel₂ a A
(R ⁺) x = ∃ λ n → (R ^^[1+ n ]) x

-- Reflexive transitive closure of binary relations.

_* : ∀ {a} {A : Set a} →
     Rel₂ a A → Rel₂ a A
(R *) x = ∃ λ n → (R ^^ n) x

-- Repeated composition of a function with itself.

infix  _^[_]_

_^[_]_ : ∀ {a} {A : Set a} → (A → A) → ℕ → A → A
f ^[ zero  ] x = x
f ^[ suc n ] x = f (f ^[ n ] x)

-- Unions of families of relation transformers.

⋃ : ∀ {a b} ℓ {A : Set a} {B : Set b} →
    (A → Trans (a ⊔ ℓ) B) → Trans (a ⊔ ℓ) B
⋃ _ F R = λ b → ∃ λ a → F a R b

-- An analogue of ⋃ₙ Fⁿ.

infix  _^ω_

_^ω_ : ∀ {a ℓ} {A : Set a} → Trans ℓ A → Trans ℓ A
_^ω_ F = ⋃ _ (F ^[_]_)

-- Relation containment.

infix  _⊆_

_⊆_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} →
      Rel ℓ₁ A → Rel ℓ₂ A → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
R ⊆ S = ∀ {x} → R x → S x

-- "Equational" reasoning combinators.

infix  -1 finally-⊆
infixr -2 _⊆⟨_⟩_ _⊆⟨⟩_

_⊆⟨_⟩_ : ∀ {a p q r} {A : Set a}
         (P : Rel p A) {Q : Rel q A} {R : Rel r A} →
         P ⊆ Q → Q ⊆ R → P ⊆ R
_ ⊆⟨ P⊆Q ⟩ Q⊆R = Q⊆R ∘ P⊆Q

_⊆⟨⟩_ : ∀ {a p q} {A : Set a}
        (P : Rel p A) {Q : Rel q A} →
        P ⊆ Q → P ⊆ Q
_ ⊆⟨⟩ P⊆Q = P⊆Q

finally-⊆ : ∀ {a p q} {A : Set a}
            (P : Rel p A) (Q : Rel q A) →
            P ⊆ Q → P ⊆ Q
finally-⊆ _ _ P⊆Q = P⊆Q

syntax finally-⊆ P Q P⊆Q = P ⊆⟨ P⊆Q ⟩∎ Q ∎

-- Preservation lemmas for _⊆_.

infix  _⊆-cong-→_

⊆-cong :
  ∀ {k a r₁ r₂ s₁ s₂} {A : Set a}
    {R₁ : Rel r₁ A} {S₁ : Rel s₁ A}
    {R₂ : Rel r₂ A} {S₂ : Rel s₂ A} →
  Extensionality? ⌊ k ⌋-sym (a ⊔ r₁ ⊔ r₂) (r₁ ⊔ r₂ ⊔ s₁ ⊔ s₂) →
  (∀ {x} → R₁ x ↝[ ⌊ k ⌋-sym ] R₂ x) →
  (∀ {x} → S₁ x ↝[ ⌊ k ⌋-sym ] S₂ x) →
  R₁ ⊆ S₁ ↝[ ⌊ k ⌋-sym ] R₂ ⊆ S₂
⊆-cong {k} {a} {r₁} {r₂} ext R₁↝R₂ S₁↝S₂ =
  implicit-∀-cong
    (lower-extensionality? ⌊ k ⌋-sym (r₁ ⊔ r₂) lzero ext) $
  →-cong (lower-extensionality? ⌊ k ⌋-sym a (r₁ ⊔ r₂) ext)
         R₁↝R₂ S₁↝S₂

_⊆-cong-→_ :
  ∀ {a r₁ r₂ s₁ s₂} {A : Set a}
    {R₁ : Rel r₁ A} {S₁ : Rel s₁ A}
    {R₂ : Rel r₂ A} {S₂ : Rel s₂ A} →
  R₂ ⊆ R₁ → S₁ ⊆ S₂ → R₁ ⊆ S₁ → R₂ ⊆ S₂
R₂→R₁ ⊆-cong-→ S₁→S₂ = implicit-∀-cong _ $ →-cong-→ R₂→R₁ S₁→S₂

⊆-congʳ :
  ∀ {k a r s₁ s₂} {A : Set a}
    {R : Rel r A} {S₁ : Rel s₁ A} {S₂ : Rel s₂ A} →
  Extensionality? k (a ⊔ r) (r ⊔ s₁ ⊔ s₂) →
  (∀ {x} → S₁ x ↝[ k ] S₂ x) →
  R ⊆ S₁ ↝[ k ] R ⊆ S₂
⊆-congʳ {k} {a} {r} ext S₁↝S₂ =
  implicit-∀-cong (lower-extensionality? k r lzero ext) $
  ∀-cong (lower-extensionality? k a r ext) λ _ →
  S₁↝S₂

-- Relation containment (_⊆_) is not antisymmetric (with respect to
-- propositional equality) if the index type is inhabited.

⊆-not-antisymmetric :
  ∀ {ℓ x} {X : Set x} →
  X →
  ¬ ({R S : Rel ℓ X} → R ⊆ S → S ⊆ R → R ≡ S)
⊆-not-antisymmetric {ℓ} {X = X} x antisym = Bool.true≢false true≡false
  where
  R S : Rel ℓ X
  R = λ _ → ↑ _ ⊤
  S = λ _ → ↑ _ Bool

  R≡S : R ≡ S
  R≡S = antisym (λ _ → lift true) _

  ⊤≡Bool : ↑ _ ⊤ ≡ ↑ _ Bool
  ⊤≡Bool = cong (_$ x) R≡S

  ⊤↔Bool : ⊤ ↔ Bool
  ⊤↔Bool =
    ⊤         ↝⟨ inverse Bijection.↑↔ ⟩
    ↑ _ ⊤     ↝⟨ ≡⇒↝ _ ⊤≡Bool ⟩
    ↑ _ Bool  ↝⟨ Bijection.↑↔ ⟩□
    Bool      □

  true≡false : true ≡ false
  true≡false =
    true                                   ≡⟨ sym $ _↔_.right-inverse-of ⊤↔Bool _ ⟩
    _↔_.to ⊤↔Bool (_↔_.from ⊤↔Bool true)   ≡⟨⟩
    _↔_.to ⊤↔Bool tt                       ≡⟨⟩
    _↔_.to ⊤↔Bool (_↔_.from ⊤↔Bool false)  ≡⟨ _↔_.right-inverse-of ⊤↔Bool _ ⟩∎
    false                                  ∎

-- Monotonicity of relation transformers.

Monotone :
  ∀ {a ℓ} {A : Set a} →
  Trans ℓ A → Set (a ⊔ lsuc ℓ)
Monotone F = ∀ {R S} → R ⊆ S → F R ⊆ F S

-- A relation transformer is extensive if the input is always
-- contained in the output.

Extensive : ∀ {ℓ} {I : Set ℓ} → Trans ℓ I → Set (lsuc ℓ)
Extensive G = ∀ R → R ⊆ G R

-- A definition that turns into a notion of symmetry if the first
-- argument is instantiated with the swap function. In that case this
-- definition is similar to one of those given by Pous and Sangiorgi
-- in Section 6.3.4.1 of "Enhancements of the bisimulation proof
-- method".

Symmetric : ∀ {ℓ} {I : Set ℓ} → (I → I) → Trans ℓ I → Set (lsuc ℓ)
Symmetric f F = ∀ R → F (R ∘ f) ⊆ F R ∘ f

-- If f is an involution, then the inclusion in Symmetric f F holds
-- also in the other direction.

involution→other-symmetry :
  ∀ {ℓ} {I : Set ℓ} (F : Trans ℓ I) {f : I → I} →
  f ∘ f ≡ id → Symmetric f F → ∀ R → F R ∘ f ⊆ F (R ∘ f)
involution→other-symmetry F {f} inv symm R =
  F R ∘ f            ⊆⟨ (λ {x} → subst (λ g → F (R ∘ g) (f x)) (sym inv)) ⟩
  F (R ∘ f ∘ f) ∘ f  ⊆⟨ symm _ ⟩
  F (R ∘ f) ∘ f ∘ f  ⊆⟨ (λ {x} → subst (λ g → F (R ∘ f) (g x)) inv) ⟩∎
  F (R ∘ f)          ∎

-- Composition is associative.

⊙-assoc : ∀ {a ℓ₁ ℓ₂ ℓ₃} {A : Set a} →
          (R₁ : Rel₂ ℓ₁ A) {R₂ : Rel₂ ℓ₂ A} (R₃ : Rel₂ ℓ₃ A) →
          ∀ p → (R₁ ⊙ (R₂ ⊙ R₃)) p ↔ ((R₁ ⊙ R₂) ⊙ R₃) p
⊙-assoc R₁ {R₂} R₃ (a , d) =
  (∃ λ b → R₁ (a , b) × ∃ λ c → R₂ (b , c) × R₃ (c , d))    ↝⟨ ∃-cong (λ _ → ∃-comm) ⟩
  (∃ λ b → ∃ λ c → R₁ (a , b) × R₂ (b , c) × R₃ (c , d))    ↝⟨ ∃-comm ⟩
  (∃ λ c → ∃ λ b → R₁ (a , b) × R₂ (b , c) × R₃ (c , d))    ↝⟨ ∃-cong (λ _ → ∃-cong λ _ → Σ-assoc) ⟩
  (∃ λ c → ∃ λ b → (R₁ (a , b) × R₂ (b , c)) × R₃ (c , d))  ↝⟨ ∃-cong (λ _ → Σ-assoc) ⟩□
  (∃ λ c → (∃ λ b → R₁ (a , b) × R₂ (b , c)) × R₃ (c , d))  □

-- Several forms of composition preserve several kinds of functions.

⊙-cong :
  ∀ {k a r₁ r₂ s₁ s₂} {A : Set a} →
    {R₁ : Rel₂ r₁ A} {R₂ : Rel₂ r₂ A} →
    {S₁ : Rel₂ s₁ A} {S₂ : Rel₂ s₂ A} →
  (∀ p → R₁ p ↝[ k ] R₂ p) →
  (∀ p → S₁ p ↝[ k ] S₂ p) →
  ∀ p → (R₁ ⊙ S₁) p ↝[ k ] (R₂ ⊙ S₂) p
⊙-cong {R₁ = R₁} {R₂} {S₁} {S₂} R₁↝R₂ S₁↝S₂ (x , z) =
  (∃ λ y → R₁ (x , y) × S₁ (y , z))  ↝⟨ ∃-cong (λ _ → R₁↝R₂ _ ×-cong S₁↝S₂ _) ⟩□
  (∃ λ y → R₂ (x , y) × S₂ (y , z))  □

composition-cong :
  ∀ {k a} {A : Set a} {R₁ R₂ S₁ S₂ : Rel₂ a A} →
  (∀ p → R₁ p ↝[ k ] R₂ p) →
  (∀ p → S₁ p ↝[ k ] S₂ p) →
  ∀ n p → composition R₁ S₁ n p ↝[ k ] composition R₂ S₂ n p
composition-cong R₁↝R₂ S₁↝S₂ = λ where
  zero    → R₁↝R₂
  (suc n) → ⊙-cong S₁↝S₂ (composition-cong R₁↝R₂ S₁↝S₂ n)

^^[1+]-cong :
  ∀ {k a} {A : Set a} {R₁ R₂ : Rel₂ a A} →
  (∀ p → R₁ p ↝[ k ] R₂ p) →
  ∀ n p → (R₁ ^^[1+ n ]) p ↝[ k ] (R₂ ^^[1+ n ]) p
^^[1+]-cong R₁↝R₂ = composition-cong R₁↝R₂ R₁↝R₂

^^-cong :
  ∀ {k a} {A : Set a} {R₁ R₂ : Rel₂ a A} →
  (∀ p → R₁ p ↝[ k ] R₂ p) →
  ∀ n p → (R₁ ^^ n) p ↝[ k ] (R₂ ^^ n) p
^^-cong R₁↝R₂ = composition-cong (λ _ → _ □) R₁↝R₂

⁺-cong :
  ∀ {k a} {A : Set a} {R₁ R₂ : Rel₂ a A} →
  (∀ p → R₁ p ↝[ k ] R₂ p) →
  ∀ p → (R₁ ⁺) p ↝[ k ] (R₂ ⁺) p
⁺-cong R₁↝R₂ p = ∃-cong λ n → ^^[1+]-cong R₁↝R₂ n p

*-cong :
  ∀ {k a} {A : Set a} {R₁ R₂ : Rel₂ a A} →
  (∀ p → R₁ p ↝[ k ] R₂ p) →
  ∀ p → (R₁ *) p ↝[ k ] (R₂ *) p
*-cong R₁↝R₂ p = ∃-cong λ n → ^^-cong R₁↝R₂ n p

-- Two lemmas relating composition and _⊙_.

composition-⊙-comm :
  ∀ {k a} {A : Set a} {R S : Rel₂ a A} →
  (∀ p → (R ⊙ S) p ↝[ k ] (S ⊙ R) p) →
  ∀ n p → (composition R S n ⊙ S) p ↝[ k ] (S ⊙ composition R S n) p
composition-⊙-comm             hyp zero    = hyp
composition-⊙-comm {R = R} {S} hyp (suc n) = λ p →
  ((S ⊙ composition R S n) ⊙ S) p  ↔⟨ inverse $ ⊙-assoc S S _ ⟩
  (S ⊙ (composition R S n ⊙ S)) p  ↝⟨ ⊙-cong (λ p → S p □) (composition-⊙-comm hyp n) _ ⟩□
  (S ⊙ (S ⊙ composition R S n)) p  □

composition⊙composition :
  ∀ {k a} {A : Set a} {R S : Rel₂ a A} m n₁ {n₂} →
  (∀ p → (R ⊙ composition R S n₁) p ↝[ k ] composition R S n₂ p) →
  ∀ p → (composition R S m ⊙ composition R S n₁) p ↝[ k ]
        composition R S (m + n₂) p
composition⊙composition {R = R} {S} = λ where
  zero n₁ {n₂} hyp p →
    (R ⊙ composition R S n₁) p  ↝⟨ hyp _ ⟩
    composition R S n₂ p        □
  (suc m) n₁ {n₂} hyp p →
    ((S ⊙ composition R S m) ⊙ composition R S n₁) p  ↔⟨ inverse $ ⊙-assoc S (composition R S n₁) _ ⟩
    (S ⊙ (composition R S m ⊙ composition R S n₁)) p  ↝⟨ ⊙-cong (λ p → S p □) (composition⊙composition m n₁ hyp) _ ⟩□
    (S ⊙ composition R S (m + n₂)) p            □

-- The transitive closure is transitive.

⁺-trans : ∀ {a} {A : Set a} {R : Rel₂ a A} {x y z} →
          (R ⁺) (x , y) → (R ⁺) (y , z) → (R ⁺) (x , z)
⁺-trans (m , xR¹⁺ᵐy) (n , yR¹⁺ⁿz) =
    m + suc n
  , composition⊙composition m n (λ _ → id) _ (_ , xR¹⁺ᵐy , yR¹⁺ⁿz)

-- The reflexive transitive closure is transitive.

*-trans : ∀ {a} {A : Set a} {R : Rel₂ a A} {x y z} →
          (R *) (x , y) → (R *) (y , z) → (R *) (x , z)
*-trans {R = R} (m , xRᵐy) (n , yRⁿz) =
  m + n , composition⊙composition m n lemma _ (_ , xRᵐy , yRⁿz)
  where
  lemma : ∀ p → (uncurry _≡_ ⊙ (R ^^ n)) p → (R ^^ n) p
  lemma _ (_ , refl , r) = r

-- Lemmas relating different forms of composition and swap.

⊙-swap :
  ∀ {k a r s} {A : Set a} {R : Rel₂ r A} {S : Rel₂ s A} →
  (∀ p → R p ↝[ k ] R (swap p)) →
  (∀ p → S p ↝[ k ] S (swap p)) →
  ∀ p → (R ⊙ S) p ↝[ k ] (S ⊙ R) (swap p)
⊙-swap {R = R} {S} R↝ S↝ (x , z) =
  (∃ λ y → R (x , y) × S (y , z))  ↝⟨ ∃-cong (λ _ → R↝ _ ×-cong S↝ _) ⟩
  (∃ λ y → R (y , x) × S (z , y))  ↔⟨ ∃-cong (λ _ → ×-comm) ⟩□
  (∃ λ y → S (z , y) × R (y , x))  □

composition-swap :
  ∀ {k a} {A : Set a} {R S : Rel₂ a A} →
  (∀ p → R p ↝[ k ] R (swap p)) →
  (∀ p → S p ↝[ k ] S (swap p)) →
  (∀ p → (R ⊙ S) p ↝[ k ] (S ⊙ R) p) →
  ∀ n p → composition R S n p ↝[ k ] composition R S n (swap p)
composition-swap {R = R} {S} R↝ S↝ hyp = λ where
  zero    p → R p         ↝⟨ R↝ _ ⟩□
              R (swap p)  □
  (suc n) p → (S ⊙ composition R S n) p         ↝⟨ ⊙-swap S↝ (composition-swap R↝ S↝ hyp n) _ ⟩
              (composition R S n ⊙ S) (swap p)  ↝⟨ composition-⊙-comm hyp n _ ⟩□
              (S ⊙ composition R S n) (swap p)  □

^^[1+]-swap :
  ∀ {k a} {A : Set a} {R : Rel₂ a A} →
  (∀ p → R p ↝[ k ] R (swap p)) →
  ∀ n p → (R ^^[1+ n ]) p ↝[ k ] (R ^^[1+ n ]) (swap p)
^^[1+]-swap R↝ = composition-swap R↝ R↝ (λ _ → _ □)

^^-swap :
  ∀ {k a} {A : Set a} {R : Rel₂ a A} →
  (∀ p → R p ↝[ k ] R (swap p)) →
  ∀ n p → (R ^^ n) p ↝[ k ] (R ^^ n) (swap p)
^^-swap {R = R} R↝ = composition-swap lemma₁ R↝ lemma₂
  where
  lemma₁ = λ { (x , y) →
    x ≡ y  ↔⟨ Groupoid.⁻¹-bijection (EG.groupoid _) ⟩□
    y ≡ x  □ }

  lemma₂ = λ { (x , z) →
    (∃ λ y → x ≡ y × R (y , z))  ↔⟨ ∃-cong (λ _ → ×-comm) ⟩
    (∃ λ y → R (y , z) × x ≡ y)  ↝⟨ ∃-cong (λ _ → ∃-cong λ _ → lemma₁ _) ⟩
    (∃ λ y → R (y , z) × y ≡ x)  ↔⟨ inverse $ ∃-intro _ _ ⟩
    R (x , z)                    ↔⟨ ∃-intro _ _ ⟩□
    (∃ λ y → R (x , y) × y ≡ z)  □}

⁺-swap :
  ∀ {k a} {A : Set a} {R : Rel₂ a A} →
  (∀ p → R p ↝[ k ] R (swap p)) →
  ∀ p → (R ⁺) p ↝[ k ] (R ⁺) (swap p)
⁺-swap {R = R} R↝ p =
  (R ⁺) p                           ↔⟨⟩
  (∃ λ n → (R ^^[1+ n ]) p)         ↝⟨ ∃-cong (λ n → ^^[1+]-swap R↝ n _) ⟩
  (∃ λ n → (R ^^[1+ n ]) (swap p))  ↔⟨⟩
  (R ⁺) (swap p)                    □

*-swap :
  ∀ {k a} {A : Set a} {R : Rel₂ a A} →
  (∀ p → R p ↝[ k ] R (swap p)) →
  ∀ p → (R *) p ↝[ k ] (R *) (swap p)
*-swap {R = R} R↝ p =
  (R *) p                      ↔⟨⟩
  (∃ λ n → (R ^^ n) p)         ↝⟨ ∃-cong (λ n → ^^-swap R↝ n _) ⟩
  (∃ λ n → (R ^^ n) (swap p))  ↔⟨⟩
  (R *) (swap p)               □

-- ⋃ constructs least upper bounds.

⊆-⋃ : ∀ {a b ℓ} {A : Set a} {B : Set b}
      (F : A → Trans (a ⊔ ℓ) B) a →
      ∀ R → F a R ⊆ ⋃ ℓ F R
⊆-⋃ {ℓ = ℓ} F a R =
  F a R                    ⊆⟨ a ,_ ⟩
  (λ x → ∃ λ a → F a R x)  ⊆⟨ id ⟩∎
  ⋃ ℓ F R                  ∎

⋃-⊆ : ∀ {a b ℓ} {A : Set a} {B : Set b}
      (F : A → Trans (a ⊔ ℓ) B) (G : Trans (a ⊔ ℓ) B) →
      (∀ {a} R → F a R ⊆ G R) →
      ∀ R → ⋃ ℓ F R ⊆ G R
⋃-⊆ {ℓ = ℓ} F G hyp R =
  ⋃ ℓ F R                  ⊆⟨⟩
  (λ x → ∃ λ a → F a R x)  ⊆⟨ hyp _ ∘ proj₂ ⟩∎
  G R                      ∎