|
1
|
1 {-# OPTIONS --universe-polymorphism #-}
|
|
|
2
|
|
|
3 open import Level
|
|
|
4 open import Data.Empty
|
|
|
5 open import Data.Product
|
|
|
6 open import Data.Nat.Base
|
|
|
7 open import Data.Sum
|
|
|
8 open import Data.Unit
|
|
|
9 open import Relation.Binary
|
|
|
10 open import Relation.Binary.Core
|
|
|
11 open import Relation.Nullary
|
|
|
12 open import utilities
|
|
|
13
|
|
|
14 module RelOp (S : Set) where
|
|
|
15
|
|
|
16 data Id {l} {X : Set} : Rel X l where
|
|
|
17 ref : {x : X} -> Id x x
|
|
|
18
|
|
|
19 -- substId1 | x == y & P(x) => P(y)
|
|
|
20 substId1 : ∀ {l} -> {X : Set} -> {x y : X} ->
|
|
|
21 Id {l} x y -> (P : Pred X) -> P x -> P y
|
|
|
22 substId1 ref P q = q
|
|
|
23
|
|
|
24 -- substId2 | x == y & P(y) => P(x)
|
|
|
25 substId2 : ∀ {l} -> {X : Set} -> {x y : X} ->
|
|
|
26 Id {l} x y -> (P : Pred X) -> P y -> P x
|
|
|
27 substId2 ref P q = q
|
|
|
28
|
|
|
29 -- for X ⊆ S (formally, X : Pred S)
|
|
|
30 -- delta X = { (a, a) | a ∈ X }
|
|
|
31 delta : ∀ {l} -> Pred S -> Rel S l
|
|
|
32 delta X a b = X a × Id a b
|
|
|
33
|
|
|
34 -- deltaGlob = delta S
|
|
|
35 deltaGlob : ∀ {l} -> Rel S l
|
|
|
36 deltaGlob = delta (λ (s : S) → ⊤)
|
|
|
37
|
|
|
38 -- emptyRel = \varnothing
|
|
|
39 emptyRel : Rel S Level.zero
|
|
|
40 emptyRel a b = ⊥
|
|
|
41
|
|
|
42 -- comp R1 R2 = R2 ∘ R1 (= R1; R2)
|
|
|
43 comp : ∀ {l} -> Rel S l -> Rel S l -> Rel S l
|
|
|
44 comp R1 R2 a b = ∃ (λ (a' : S) → R1 a a' × R2 a' b)
|
|
|
45
|
|
|
46 -- union R1 R2 = R1 ∪ R2
|
|
|
47 union : ∀ {l} -> Rel S l -> Rel S l -> Rel S l
|
|
|
48 union R1 R2 a b = R1 a b ⊎ R2 a b
|
|
|
49
|
|
|
50 -- repeat n R = R^n
|
|
|
51 repeat : ∀ {l} -> ℕ -> Rel S l -> Rel S l
|
|
|
52 repeat ℕ.zero R = deltaGlob
|
|
|
53 repeat (ℕ.suc m) R = comp (repeat m R) R
|
|
|
54
|
|
|
55 -- unionInf f = ⋃_{n ∈ ω} f(n)
|
|
|
56 unionInf : ∀ {l} -> (ℕ -> Rel S l) -> Rel S l
|
|
|
57 unionInf f a b = ∃ (λ (n : ℕ) → f n a b)
|
|
|
58 -- restPre X R = { (s1,s2) ∈ R | s1 ∈ X }
|
|
|
59 restPre : ∀ {l} -> Pred S -> Rel S l -> Rel S l
|
|
|
60 restPre X R a b = X a × R a b
|
|
|
61
|
|
|
62 -- restPost X R = { (s1,s2) ∈ R | s2 ∈ X }
|
|
|
63 restPost : ∀ {l} -> Pred S -> Rel S l -> Rel S l
|
|
|
64 restPost X R a b = R a b × X b
|
|
|
65
|
|
|
66 deltaRestPre : (X : Pred S) -> (R : Rel S Level.zero) -> (a b : S) ->
|
|
|
67 Iff (restPre X R a b) (comp (delta X) R a b)
|
|
|
68 deltaRestPre X R a b
|
|
|
69 = (λ (h : restPre X R a b) → a , (proj₁ h , ref) , proj₂ h) ,
|
|
|
70 λ (h : comp (delta X) R a b) → proj₁ (proj₁ (proj₂ h)) ,
|
|
|
71 substId2
|
|
|
72 (proj₂ (proj₁ (proj₂ h)))
|
|
|
73 (λ z → R z b) (proj₂ (proj₂ h))
|
|
|
74
|
|
|
75 deltaRestPost : (X : Pred S) -> (R : Rel S Level.zero) -> (a b : S) ->
|
|
|
76 Iff (restPost X R a b) (comp R (delta X) a b)
|
|
|
77 deltaRestPost X R a b
|
|
|
78 = (λ (h : restPost X R a b) → b , proj₁ h , proj₂ h , ref) ,
|
|
|
79 λ (h : comp R (delta X) a b) →
|
|
|
80 substId1 (proj₂ (proj₂ (proj₂ h))) (R a) (proj₁ (proj₂ h)) ,
|
|
|
81 substId1 (proj₂ (proj₂ (proj₂ h))) X (proj₁ (proj₂ (proj₂ h)))
|
