-
Notifications
You must be signed in to change notification settings - Fork 0
/
Combinators.agda
180 lines (137 loc) · 6.47 KB
/
Combinators.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
module Combinators where
open import Relation.Binary.PropositionalEquality
hiding (inspect)
open import Relation.Binary.Core
open import Relation.Nullary
open import Data.List hiding (product ; sum ; [_] ; filter)
open import Data.Empty
open import Data.Unit hiding (_≟_ ; _≤_)
open import Data.Sum hiding (map ; [_,_])
open import Data.Product hiding (map ; <_,_>)
open import Data.Bool
open import Utilities.ListMonad
open import Utilities.ListProperties
open import Utilities.ListsAddition
open import Utilities.Logic
open import Finiteness
union : {X : Set} → {P Q : X → Set}
→ ListableSubset X P
→ ListableSubset X Q
→ ListableSubset X (λ x → P x ⊎ Q x)
union {X} {P} {Q} (els1 , p2i1 , i2p1) (els2 , p2i2 , i2p2)
= els1 ++ els2 , i2p' , p2i'
where
∈-split' : {X : Set} → {x : X} → (xs₁ xs₂ : List X)
→ x ∈ (xs₁ ++ xs₂) → (x ∈ xs₁) ⊎ (x ∈ xs₂)
∈-split' xs₁ xs₂ = ∈-split {_} {xs₁} {xs₂}
p2i' : (x : X) → P x ⊎ Q x → x ∈ (els1 ++ els2)
p2i' x (inj₁ x₁) = ∈-weak-rgt {_} {els2} (i2p1 x x₁)
p2i' x (inj₂ y) = ∈-weak-lft {_} {els1} (i2p2 x y)
i2p' : (x : X) → x ∈ (els1 ++ els2) → P x ⊎ Q x
i2p' x xin with ∈-split' els1 els2 xin
i2p' x xin | inj₁ x₁ = inj₁ (p2i1 x x₁)
i2p' x xin | inj₂ y = inj₂ (p2i2 x y)
open import Relation.Nullary.Decidable
rest : {X : Set} → (x : X) → (P : X → Set) → (pd : Dec (P x))
→ ⌊ pd ⌋ ≡ true → P x
rest x p (yes p₁) pr = p₁
rest x p (no ¬p) ()
restOp : {X : Set} → (x : X) → (P : X → Set) → (pd : Dec (P x))
→ P x → ⌊ pd ⌋ ≡ true
restOp x p (yes p₁) px = refl
restOp x p (no ¬p) px = ex-falso-quodlibet (¬p px)
intersection : {X : Set} → {P Q : X → Set}
→ (Pdec : (x : X) → Dec (P x))
→ ListableSubset X P
→ ListableSubset X Q
→ ListableSubset X (λ x → P x × Q x)
intersection {X} {P} {Q} pd (els1 , p2i1 , i2p1)
(els2 , p2i2 , i2p2)
= filter (λ x → ⌊ pd x ⌋) els2 , i2p' , p2i'
where
p2i' : (x : X) → P x × Q x → x ∈ filter (λ x₁ → ⌊ pd x₁ ⌋) els2
p2i' x (px , qx) = filter-in2 els2 x (λ x₁ → ⌊ pd x₁ ⌋) (i2p2 x qx) (restOp x P (pd x) px)
i2p' : (x : X) → x ∈ filter (λ x₁ → ⌊ pd x₁ ⌋) els2 → P x × Q x
i2p' x xin = p2i1 x (i2p1 x (rest x P (pd x) ((filter-el x els2 (λ x₁ → ⌊ pd x₁ ⌋) xin)))) ,
p2i2 x (filter-∈ x els2 (λ x₁ → ⌊ pd x₁ ⌋) xin)
<_,_> : {X Y : Set} → (X → Set) → (Y → Set) → (X × Y → Set)
<_,_> P Q (x , y) = P x × Q y
[_,,_] : {X Y : Set} → (X → Set) → (Y → Set) → (X ⊎ Y → Set)
[_,,_] P Q (inj₁ x) = P x
[_,,_] P Q (inj₂ y) = Q y
product : {X : Set}{P : X → Set}{Y : Set}{Q : Y → Set}
→ ListableSubset X P
→ ListableSubset Y Q
→ ListableSubset (X × Y) < P , Q >
product {X} {P} {Y} {Q} (els1 , p2i1 , i2p1)
(els2 , p2i2 , i2p2) =
els1 >>= (λ x →
els2 >>= (λ y →
return (x , y))) , hlp , hlp2
where
hlp2 : (x : X × Y) → < P , Q > x →
x ∈ els1 >>= (λ x₁ → els2 >>= (λ y → return (x₁ , y)))
hlp2 (x1 , y1) (pr1 , pr2) = list-monad-ht (x1 , y1) els1
(λ x₁ → els2 >>= (λ y → return (x₁ , y))) x1
(i2p1 x1 pr1)
(list-monad-ht (x1 , y1) els2 _ y1 (i2p2 y1 pr2) here)
hlp : (x : X × Y) →
x ∈ els1 >>= (λ x₁ → els2 >>= (λ y → return (x₁ , y))) →
< P , Q > x
hlp x pr with list-monad-th x els1 (λ x₁ → els2 >>= (λ y → return (x₁ , y))) pr
... | o1 , o2 , o3 with list-monad-th x els2 _ o3
hlp .(o1 , p1) pr | o1 , o2 , o3 | p1 , p2 , here = p2i1 o1 o2 , p2i2 p1 p2
hlp x pr | o1 , o2 , o3 | p1 , p2 , there ()
sum : {X : Set}{P : X → Set}{Y : Set}{Q : Y → Set}
→ ListableSubset X P
→ ListableSubset Y Q
→ ListableSubset (X ⊎ Y) [ P ,, Q ]
sum {X} {P} {Y} {Q} (els1 , p2i1 , i2p1) (els2 , p2i2 , i2p2)
= Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2 , hlp , hlp2
where
hlp : (x : X ⊎ Y) → x ∈ (Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2) → [ P ,, Q ] x
hlp (inj₁ x) xi = p2i1 x (xi1' x els1 els2 xi)
where
xi1' : {X : Set} → (x : X) → (els1 : List X)
→ {Y : Set} → (els2 : List Y)
→ inj₁ x ∈ (Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2)
→ x ∈ els1
xi1' x [] [] ()
xi1' x [] (x₁ ∷ ys) (there pr) = xi1' x [] ys pr
xi1' x₁ (.x₁ ∷ els1) ys here = here
xi1' x (x₁ ∷ els1) ys (there pr) = there (xi1' x els1 ys pr)
hlp (inj₂ y) xi = p2i2 y (xi2' y els1 els2 xi)
where
xi2' : {X : Set}{Y : Set} → (y : Y) → (els1 : List X)
→ (els2 : List Y)
→ inj₂ y ∈ (Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2)
→ y ∈ els2
xi2' y [] [] ()
xi2' y [] (.y ∷ els2) here = here
xi2' y [] (x ∷ els2) (there pr) = there (xi2' y [] els2 pr)
xi2' y (x ∷ els1) els2 (there pr) = xi2' y els1 els2 pr
hlp2 : (x : X ⊎ Y) → [ P ,, Q ] x →
x ∈ (Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2)
hlp2 (inj₁ x) pr = xi1 x els1 els2 (i2p1 x pr)
where
xi1 : {X : Set} → (x : X) → (els1 : List X)
→ {Y : Set} → (els2 : List Y) → x ∈ els1
→ inj₁ x ∈ (Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2)
xi1 x ._ els2 here = here
xi1 x ._ els2 (there xi) = there (xi1 x _ els2 xi)
hlp2 (inj₂ y) pr = xi2 y els1 els2 (i2p2 y pr)
where
xi2 : {X Y : Set} → (y : Y) → (els1 : List X)
→ (els2 : List Y) → y ∈ els2
→ inj₂ y ∈ (Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2)
xi2 y [] [] ()
xi2 y [] (.y ∷ els2) here = here
xi2 y [] (x ∷ els2) (there pr) = there (xi2 y [] els2 pr)
xi2 y (x ∷ els1) els2 pr = there (xi2 y els1 els2 pr)
kfWithEq2Dec : {X : Set}{P : X → Set}
→ DecEq X
→ ListableSubset X P
→ ∀ x → Dec (P x)
kfWithEq2Dec d (l , s , c) x with eq2in d x l
kfWithEq2Dec d (l , s , c) x | yes p = yes (s _ p)
kfWithEq2Dec d (l , s , c) x | no ¬p = no (λ px → ¬p (c _ px))