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