Mercurial > hg > Papers > 2020 > soto-midterm
comparison src/RelOp.agda @ 1:73127e0ab57c
(none)
| author | soto@cr.ie.u-ryukyu.ac.jp |
|---|---|
| date | Tue, 08 Sep 2020 18:38:08 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| 0:b919985837a3 | 1:73127e0ab57c |
|---|---|
| 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))) |