view paper/src/RelOp.agda @ 19:046b2b20d6c7 default tip

fix
author ryokka
date Mon, 09 Mar 2020 11:25:49 +0900
parents
children
line wrap: on
line source

{-# OPTIONS --universe-polymorphism #-}

open import Level
open import Data.Empty
open import Data.Product
open import Data.Nat.Base
open import Data.Sum
open import Data.Unit
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Nullary
open import utilities

module RelOp (S : Set) where

data Id {l} {X : Set} : Rel X l where
  ref : {x : X} -> Id x x

-- substId1 | x == y & P(x) => P(y)
substId1 :  ∀ {l} -> {X : Set} -> {x y : X} ->
           Id {l} x y -> (P : Pred X) -> P x -> P y
substId1 ref P q = q

-- substId2 | x == y & P(y) => P(x)
substId2 :  ∀ {l} -> {X : Set} -> {x y : X} ->
           Id {l} x  y -> (P : Pred X) -> P y -> P x
substId2 ref P q = q

-- for X ⊆ S (formally, X : Pred S)
-- delta X = { (a, a) | a ∈ X }
delta : ∀ {l} -> Pred S -> Rel S l
delta X a b = X a × Id a b 

-- deltaGlob = delta S
deltaGlob : ∀ {l} -> Rel S l
deltaGlob = delta (λ (s : S) → ⊤)

-- emptyRel = \varnothing
emptyRel : Rel S Level.zero
emptyRel a b = ⊥

-- comp R1 R2 = R2 ∘ R1 (= R1; R2)
comp : ∀ {l} -> Rel S l -> Rel S l -> Rel S l
comp R1 R2 a b = ∃ (λ (a' : S) → R1 a a' × R2 a' b)

-- union R1 R2 = R1 ∪ R2
union : ∀ {l} -> Rel S l -> Rel S l -> Rel S l
union R1 R2 a b = R1 a b ⊎ R2 a b

-- repeat n R = R^n
repeat : ∀ {l} -> ℕ -> Rel S l -> Rel S l
repeat ℕ.zero R = deltaGlob
repeat (ℕ.suc m) R = comp (repeat m R) R

-- unionInf f = ⋃_{n ∈ ω} f(n)
unionInf : ∀ {l} -> (ℕ -> Rel S l) -> Rel S l
unionInf f a b = ∃ (λ (n : ℕ) → f n a b)
-- restPre X R = { (s1,s2) ∈ R | s1 ∈ X }
restPre : ∀ {l} -> Pred S -> Rel S l -> Rel S l
restPre X R a b = X a × R a b

-- restPost X R = { (s1,s2) ∈ R | s2 ∈ X }
restPost : ∀ {l} -> Pred S -> Rel S l -> Rel S l
restPost X R a b = R a b × X b

deltaRestPre : (X : Pred S) -> (R : Rel S Level.zero) -> (a b : S) ->
               Iff (restPre X R a b) (comp (delta X) R a b)
deltaRestPre X R a b
  = (λ (h : restPre X R a b) → a , (proj₁ h , ref) , proj₂ h) ,
     λ (h : comp (delta X) R a b) → proj₁ (proj₁ (proj₂ h)) ,
       substId2
         (proj₂ (proj₁ (proj₂ h)))
         (λ z → R z b) (proj₂ (proj₂ h))

deltaRestPost : (X : Pred S) -> (R : Rel S Level.zero) -> (a b : S) ->
                Iff (restPost X R a b) (comp R (delta X) a b)
deltaRestPost X R a b
  = (λ (h : restPost X R a b) → b , proj₁ h , proj₂ h , ref) ,
     λ (h : comp R (delta X) a b) →
       substId1 (proj₂ (proj₂ (proj₂ h))) (R a) (proj₁ (proj₂ h)) ,
       substId1 (proj₂ (proj₂ (proj₂ h))) X (proj₁ (proj₂ (proj₂ h)))