|
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.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} @$\rightarrow$@ Id x x
|
|
|
18
|
|
|
19 -- substId1 | x == y & P(x) => P(y)
|
|
|
20 substId1 : @$\forall$@ {l} @$\rightarrow$@ {X : Set} @$\rightarrow$@ {x y : X} @$\rightarrow$@
|
|
|
21 Id {l} x y @$\rightarrow$@ (P : Pred X) @$\rightarrow$@ P x @$\rightarrow$@ P y
|
|
|
22 substId1 ref P q = q
|
|
|
23
|
|
|
24 -- substId2 | x == y & P(y) => P(x)
|
|
|
25 substId2 : @$\forall$@ {l} @$\rightarrow$@ {X : Set} @$\rightarrow$@ {x y : X} @$\rightarrow$@
|
|
|
26 Id {l} x y @$\rightarrow$@ (P : Pred X) @$\rightarrow$@ P y @$\rightarrow$@ 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 : @$\forall$@ {l} @$\rightarrow$@ Pred S @$\rightarrow$@ Rel S l
|
|
|
32 delta X a b = X a @$\times$@ Id a b
|
|
|
33
|
|
|
34 -- deltaGlob = delta S
|
|
|
35 deltaGlob : @$\forall$@ {l} @$\rightarrow$@ Rel S l
|
|
|
36 deltaGlob = delta (@$\lambda$@ (s : S) @$\rightarrow$@ @$\top$@)
|
|
|
37
|
|
|
38 -- emptyRel = \varnothing
|
|
|
39 emptyRel : Rel S Level.zero
|
|
|
40 emptyRel a b = @$\bot$@
|
|
|
41
|
|
|
42 -- comp R1 R2 = R2 ∘ R1 (= R1; R2)
|
|
|
43 comp : @$\forall$@ {l} @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l
|
|
|
44 comp R1 R2 a b = ∃ (@$\lambda$@ (a' : S) @$\rightarrow$@ R1 a a' @$\times$@ R2 a' b)
|
|
|
45
|
|
|
46 -- union R1 R2 = R1 ∪ R2
|
|
|
47 union : @$\forall$@ {l} @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l
|
|
|
48 union R1 R2 a b = R1 a b ⊎ R2 a b
|
|
|
49
|
|
|
50 -- repeat n R = R^n
|
|
|
51 repeat : @$\forall$@ {l} @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l
|
|
|
52 repeat @$\mathbb{N}$@.zero R = deltaGlob
|
|
|
53 repeat (@$\mathbb{N}$@.suc m) R = comp (repeat m R) R
|
|
|
54
|
|
|
55 -- unionInf f = ⋃_{n ∈ ω} f(n)
|
|
|
56 unionInf : @$\forall$@ {l} @$\rightarrow$@ (@$\mathbb{N}$@ @$\rightarrow$@ Rel S l) @$\rightarrow$@ Rel S l
|
|
|
57 unionInf f a b = ∃ (@$\lambda$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ f n a b)
|
|
|
58 -- restPre X R = { (s1,s2) ∈ R | s1 ∈ X }
|
|
|
59 restPre : @$\forall$@ {l} @$\rightarrow$@ Pred S @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l
|
|
|
60 restPre X R a b = X a @$\times$@ R a b
|
|
|
61
|
|
|
62 -- restPost X R = { (s1,s2) ∈ R | s2 ∈ X }
|
|
|
63 restPost : @$\forall$@ {l} @$\rightarrow$@ Pred S @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l
|
|
|
64 restPost X R a b = R a b @$\times$@ X b
|
|
|
65
|
|
|
66 deltaRestPre : (X : Pred S) @$\rightarrow$@ (R : Rel S Level.zero) @$\rightarrow$@ (a b : S) @$\rightarrow$@
|
|
|
67 Iff (restPre X R a b) (comp (delta X) R a b)
|
|
|
68 deltaRestPre X R a b
|
|
|
69 = (@$\lambda$@ (h : restPre X R a b) @$\rightarrow$@ a , (proj@$\_{1}$@ h , ref) , proj@$\_{2}$@ h) ,
|
|
|
70 @$\lambda$@ (h : comp (delta X) R a b) @$\rightarrow$@ proj@$\_{1}$@ (proj@$\_{1}$@ (proj@$\_{2}$@ h)) ,
|
|
|
71 substId2
|
|
|
72 (proj@$\_{2}$@ (proj@$\_{1}$@ (proj@$\_{2}$@ h)))
|
|
|
73 (@$\lambda$@ z @$\rightarrow$@ R z b) (proj@$\_{2}$@ (proj@$\_{2}$@ h))
|
|
|
74
|
|
|
75 deltaRestPost : (X : Pred S) @$\rightarrow$@ (R : Rel S Level.zero) @$\rightarrow$@ (a b : S) @$\rightarrow$@
|
|
|
76 Iff (restPost X R a b) (comp R (delta X) a b)
|
|
|
77 deltaRestPost X R a b
|
|
|
78 = (@$\lambda$@ (h : restPost X R a b) @$\rightarrow$@ b , proj@$\_{1}$@ h , proj@$\_{2}$@ h , ref) ,
|
|
|
79 @$\lambda$@ (h : comp R (delta X) a b) @$\rightarrow$@
|
|
|
80 substId1 (proj@$\_{2}$@ (proj@$\_{2}$@ (proj@$\_{2}$@ h))) (R a) (proj@$\_{1}$@ (proj@$\_{2}$@ h)) ,
|
|
|
81 substId1 (proj@$\_{2}$@ (proj@$\_{2}$@ (proj@$\_{2}$@ h))) X (proj@$\_{1}$@ (proj@$\_{2}$@ (proj@$\_{2}$@ h)))
|
