|
1472
|
1 {-# OPTIONS --cubical-compatible --safe #-}
|
|
|
2 open import Level
|
|
|
3 open import Ordinals
|
|
|
4 open import logic
|
|
|
5 open import Relation.Nullary
|
|
|
6
|
|
431
|
7 open import Level
|
|
1472
|
8 open import Ordinals
|
|
|
9 import HODBase
|
|
|
10 import OD
|
|
|
11 open import Relation.Nullary
|
|
|
12 module partfunc {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) where
|
|
|
13
|
|
|
14 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
15 open import Data.Empty
|
|
|
16
|
|
|
17 import OrdUtil
|
|
|
18
|
|
|
19 open Ordinals.Ordinals O
|
|
|
20 open Ordinals.IsOrdinals isOrdinal
|
|
|
21 import ODUtil
|
|
431
|
22
|
|
|
23 open import logic
|
|
1472
|
24 open import nat
|
|
|
25
|
|
|
26 open OrdUtil O
|
|
|
27 open ODUtil O HODAxiom ho<
|
|
431
|
28
|
|
|
29 open _∧_
|
|
|
30 open _∨_
|
|
|
31 open Bool
|
|
|
32
|
|
1472
|
33 open HODBase._==_
|
|
|
34
|
|
|
35 open HODBase.ODAxiom HODAxiom
|
|
|
36 open OD O HODAxiom
|
|
|
37
|
|
|
38 open HODBase.HOD
|
|
|
39
|
|
|
40
|
|
|
41 open import Relation.Nullary
|
|
|
42 open import Relation.Binary
|
|
|
43 open import Data.Empty
|
|
|
44 open import Relation.Binary
|
|
|
45 open import Relation.Binary.Core
|
|
|
46 open import Relation.Binary.PropositionalEquality
|
|
|
47 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
|
48
|
|
|
49 open import Data.Empty
|
|
|
50 open import Data.Unit using ( ⊤ ; tt )
|
|
|
51 open import Data.List hiding (filter ; find)
|
|
|
52 open import Data.Maybe
|
|
|
53
|
|
|
54 open _∧_
|
|
|
55 open _∨_
|
|
|
56 open Bool
|
|
|
57
|
|
|
58 data Two : Set where
|
|
|
59 i0 : Two
|
|
|
60 i1 : Two
|
|
|
61
|
|
431
|
62 ----
|
|
|
63 --
|
|
|
64 -- Partial Function without ZF
|
|
|
65 --
|
|
|
66
|
|
1472
|
67 record PFunc {n m l : Level } (Dom : Set n) (Cod : Set m) : Set (suc (n ⊔ m ⊔ l)) where
|
|
431
|
68 field
|
|
1472
|
69 dom : Dom → Set l
|
|
431
|
70 pmap : (x : Dom ) → dom x → Cod
|
|
|
71 meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q
|
|
|
72
|
|
|
73 ----
|
|
|
74 --
|
|
|
75 -- PFunc (Lift n Nat) Cod is equivalent to List (Maybe Cod)
|
|
|
76 --
|
|
|
77
|
|
1472
|
78 data Findp {n : Level} {Cod : Set n} : List (Maybe Cod) → (x : Nat) → Set (suc n) where
|
|
|
79 v0 : {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v ∷ f ) Zero
|
|
|
80 vn : {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x)
|
|
431
|
81
|
|
|
82 open PFunc
|
|
|
83
|
|
1472
|
84 find : {n : Level} {Cod : Set n} → (f : List (Maybe Cod) ) → (x : Nat) → Findp f x → Cod
|
|
431
|
85 find (just v ∷ _) 0 (v0 v) = v
|
|
|
86 find (_ ∷ n) (Suc i) (vn p) = find n i p
|
|
|
87
|
|
1472
|
88 findpeq : {n : Level} {Cod : Set n} → (f : List (Maybe Cod)) → {x : Nat} {p q : Findp f x } → find f x p ≡ find f x q
|
|
431
|
89 findpeq n {0} {v0 _} {v0 _} = refl
|
|
|
90 findpeq [] {Suc x} {()}
|
|
|
91 findpeq (just x₁ ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q}
|
|
|
92 findpeq (nothing ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q}
|
|
|
93
|
|
1472
|
94 List→PFunc : {Cod : Set (suc n)} → List (Maybe Cod) → PFunc (Lift n Nat) Cod
|
|
|
95 List→PFunc fp = record { dom = λ x → Lift zero (Findp fp (lower x))
|
|
431
|
96 ; pmap = λ x y → find fp (lower x) (lower y)
|
|
1472
|
97 ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q}
|
|
431
|
98 }
|
|
|
99 ----
|
|
|
100 --
|
|
|
101 -- to List (Maybe Two) is a Latice
|
|
|
102 --
|
|
|
103
|
|
|
104 _3⊆b_ : (f g : List (Maybe Two)) → Bool
|
|
|
105 [] 3⊆b [] = true
|
|
|
106 [] 3⊆b (nothing ∷ g) = [] 3⊆b g
|
|
|
107 [] 3⊆b (_ ∷ g) = true
|
|
|
108 (nothing ∷ f) 3⊆b [] = f 3⊆b []
|
|
|
109 (nothing ∷ f) 3⊆b (_ ∷ g) = f 3⊆b g
|
|
|
110 (just i0 ∷ f) 3⊆b (just i0 ∷ g) = f 3⊆b g
|
|
|
111 (just i1 ∷ f) 3⊆b (just i1 ∷ g) = f 3⊆b g
|
|
|
112 _ 3⊆b _ = false
|
|
|
113
|
|
|
114 _3⊆_ : (f g : List (Maybe Two)) → Set
|
|
|
115 f 3⊆ g = (f 3⊆b g) ≡ true
|
|
|
116
|
|
|
117 _3∩_ : (f g : List (Maybe Two)) → List (Maybe Two)
|
|
|
118 [] 3∩ (nothing ∷ g) = nothing ∷ ([] 3∩ g)
|
|
|
119 [] 3∩ g = []
|
|
|
120 (nothing ∷ f) 3∩ [] = nothing ∷ f 3∩ []
|
|
|
121 f 3∩ [] = []
|
|
|
122 (just i0 ∷ f) 3∩ (just i0 ∷ g) = just i0 ∷ ( f 3∩ g )
|
|
|
123 (just i1 ∷ f) 3∩ (just i1 ∷ g) = just i1 ∷ ( f 3∩ g )
|
|
|
124 (_ ∷ f) 3∩ (_ ∷ g) = nothing ∷ ( f 3∩ g )
|
|
|
125
|
|
|
126 3∩⊆f : { f g : List (Maybe Two) } → (f 3∩ g ) 3⊆ f
|
|
|
127 3∩⊆f {[]} {[]} = refl
|
|
|
128 3∩⊆f {[]} {just _ ∷ g} = refl
|
|
|
129 3∩⊆f {[]} {nothing ∷ g} = 3∩⊆f {[]} {g}
|
|
|
130 3∩⊆f {just _ ∷ f} {[]} = refl
|
|
|
131 3∩⊆f {nothing ∷ f} {[]} = 3∩⊆f {f} {[]}
|
|
|
132 3∩⊆f {just i0 ∷ f} {just i0 ∷ g} = 3∩⊆f {f} {g}
|
|
|
133 3∩⊆f {just i1 ∷ f} {just i1 ∷ g} = 3∩⊆f {f} {g}
|
|
|
134 3∩⊆f {just i0 ∷ f} {just i1 ∷ g} = 3∩⊆f {f} {g}
|
|
|
135 3∩⊆f {just i1 ∷ f} {just i0 ∷ g} = 3∩⊆f {f} {g}
|
|
|
136 3∩⊆f {nothing ∷ f} {just _ ∷ g} = 3∩⊆f {f} {g}
|
|
|
137 3∩⊆f {just i0 ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g}
|
|
|
138 3∩⊆f {just i1 ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g}
|
|
|
139 3∩⊆f {nothing ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g}
|
|
|
140
|
|
|
141 3∩sym : { f g : List (Maybe Two) } → (f 3∩ g ) ≡ (g 3∩ f )
|
|
|
142 3∩sym {[]} {[]} = refl
|
|
|
143 3∩sym {[]} {just _ ∷ g} = refl
|
|
|
144 3∩sym {[]} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {[]} {g})
|
|
|
145 3∩sym {just _ ∷ f} {[]} = refl
|
|
|
146 3∩sym {nothing ∷ f} {[]} = cong (λ k → nothing ∷ k) (3∩sym {f} {[]})
|
|
|
147 3∩sym {just i0 ∷ f} {just i0 ∷ g} = cong (λ k → just i0 ∷ k) (3∩sym {f} {g})
|
|
|
148 3∩sym {just i0 ∷ f} {just i1 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
|
|
|
149 3∩sym {just i1 ∷ f} {just i0 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
|
|
|
150 3∩sym {just i1 ∷ f} {just i1 ∷ g} = cong (λ k → just i1 ∷ k) (3∩sym {f} {g})
|
|
|
151 3∩sym {just i0 ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
|
|
|
152 3∩sym {just i1 ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
|
|
|
153 3∩sym {nothing ∷ f} {just i0 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
|
|
|
154 3∩sym {nothing ∷ f} {just i1 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
|
|
|
155 3∩sym {nothing ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
|
|
|
156
|
|
|
157 3⊆-[] : { h : List (Maybe Two) } → [] 3⊆ h
|
|
|
158 3⊆-[] {[]} = refl
|
|
|
159 3⊆-[] {just _ ∷ h} = refl
|
|
|
160 3⊆-[] {nothing ∷ h} = 3⊆-[] {h}
|
|
|
161
|
|
|
162 3⊆trans : { f g h : List (Maybe Two) } → f 3⊆ g → g 3⊆ h → f 3⊆ h
|
|
|
163 3⊆trans {[]} {[]} {[]} f<g g<h = refl
|
|
|
164 3⊆trans {[]} {[]} {just _ ∷ h} f<g g<h = refl
|
|
|
165 3⊆trans {[]} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {[]} {h} refl g<h
|
|
|
166 3⊆trans {[]} {nothing ∷ g} {[]} f<g g<h = refl
|
|
|
167 3⊆trans {[]} {just _ ∷ g} {just _ ∷ h} f<g g<h = refl
|
|
|
168 3⊆trans {[]} {nothing ∷ g} {just _ ∷ h} f<g g<h = refl
|
|
|
169 3⊆trans {[]} {nothing ∷ g} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {g} {h} f<g g<h
|
|
|
170 3⊆trans {nothing ∷ f} {[]} {[]} f<g g<h = f<g
|
|
|
171 3⊆trans {nothing ∷ f} {[]} {just _ ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h})
|
|
|
172 3⊆trans {nothing ∷ f} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g g<h
|
|
|
173 3⊆trans {nothing ∷ f} {nothing ∷ g} {[]} f<g g<h = 3⊆trans {f} {g} {[]} f<g g<h
|
|
|
174 3⊆trans {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
|
|
|
175 3⊆trans {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
|
|
|
176 3⊆trans {[]} {just i0 ∷ g} {[]} f<g ()
|
|
|
177 3⊆trans {[]} {just i1 ∷ g} {[]} f<g ()
|
|
|
178 3⊆trans {[]} {just x ∷ g} {nothing ∷ h} f<g g<h = 3⊆-[] {h}
|
|
|
179 3⊆trans {just i0 ∷ f} {[]} {h} () g<h
|
|
|
180 3⊆trans {just i1 ∷ f} {[]} {h} () g<h
|
|
|
181 3⊆trans {just x ∷ f} {just i0 ∷ g} {[]} f<g ()
|
|
|
182 3⊆trans {just x ∷ f} {just i1 ∷ g} {[]} f<g ()
|
|
|
183 3⊆trans {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
|
|
|
184 3⊆trans {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
|
|
|
185 3⊆trans {just x ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g ()
|
|
|
186 3⊆trans {just x ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g ()
|
|
|
187 3⊆trans {just i0 ∷ f} {nothing ∷ g} {_} () g<h
|
|
|
188 3⊆trans {just i1 ∷ f} {nothing ∷ g} {_} () g<h
|
|
|
189 3⊆trans {nothing ∷ f} {just i0 ∷ g} {[]} f<g ()
|
|
|
190 3⊆trans {nothing ∷ f} {just i1 ∷ g} {[]} f<g ()
|
|
|
191 3⊆trans {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
|
|
|
192 3⊆trans {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
|
|
|
193 3⊆trans {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g ()
|
|
|
194 3⊆trans {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g ()
|
|
|
195
|
|
|
196 3⊆∩f : { f g h : List (Maybe Two) } → f 3⊆ g → f 3⊆ h → f 3⊆ (g 3∩ h )
|
|
|
197 3⊆∩f {[]} {[]} {[]} f<g f<h = refl
|
|
|
198 3⊆∩f {[]} {[]} {x ∷ h} f<g f<h = 3⊆-[] {[] 3∩ (x ∷ h)}
|
|
|
199 3⊆∩f {[]} {x ∷ g} {h} f<g f<h = 3⊆-[] {(x ∷ g) 3∩ h}
|
|
|
200 3⊆∩f {nothing ∷ f} {[]} {[]} f<g f<h = 3⊆∩f {f} {[]} {[]} f<g f<h
|
|
|
201 3⊆∩f {nothing ∷ f} {[]} {just _ ∷ h} f<g f<h = f<g
|
|
|
202 3⊆∩f {nothing ∷ f} {[]} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {[]} {h} f<g f<h
|
|
|
203 3⊆∩f {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
|
|
|
204 3⊆∩f {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
|
|
|
205 3⊆∩f {nothing ∷ f} {just _ ∷ g} {[]} f<g f<h = f<h
|
|
|
206 3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
|
|
|
207 3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
|
|
|
208 3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
|
|
|
209 3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
|
|
|
210 3⊆∩f {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
|
|
|
211 3⊆∩f {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
|
|
|
212 3⊆∩f {nothing ∷ f} {nothing ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h
|
|
|
213 3⊆∩f {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
|
|
|
214 3⊆∩f {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
|
|
|
215
|
|
|
216 3↑22 : (f : Nat → Two) (i j : Nat) → List (Maybe Two)
|
|
|
217 3↑22 f Zero j = []
|
|
|
218 3↑22 f (Suc i) j = just (f j) ∷ 3↑22 f i (Suc j)
|
|
|
219
|
|
|
220 _3↑_ : (Nat → Two) → Nat → List (Maybe Two)
|
|
|
221 _3↑_ f i = 3↑22 f i 0
|
|
|
222
|
|
|
223 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (_3↑_ f x) 3⊆ (_3↑_ f y)
|
|
|
224 3↑< {f} {x} {y} x<y = lemma x y 0 x<y where
|
|
|
225 lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i )
|
|
|
226 lemma 0 y i z≤n with f i
|
|
|
227 lemma Zero Zero i z≤n | i0 = refl
|
|
|
228 lemma Zero (Suc y) i z≤n | i0 = 3⊆-[] {3↑22 f (Suc y) i}
|
|
|
229 lemma Zero Zero i z≤n | i1 = refl
|
|
|
230 lemma Zero (Suc y) i z≤n | i1 = 3⊆-[] {3↑22 f (Suc y) i}
|
|
|
231 lemma (Suc x) (Suc y) i (s≤s x<y) with f i
|
|
|
232 lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y
|
|
|
233 lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y
|
|
|
234
|
|
|
235 Finite3b : (p : List (Maybe Two) ) → Bool
|
|
|
236 Finite3b [] = true
|
|
|
237 Finite3b (just _ ∷ f) = Finite3b f
|
|
|
238 Finite3b (nothing ∷ f) = false
|
|
|
239
|
|
|
240 finite3cov : (p : List (Maybe Two) ) → List (Maybe Two)
|
|
|
241 finite3cov [] = []
|
|
|
242 finite3cov (just y ∷ x) = just y ∷ finite3cov x
|
|
|
243 finite3cov (nothing ∷ x) = just i0 ∷ finite3cov x
|
|
|
244
|
|
1096
|
245 record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where
|
|
|
246 field
|
|
|
247 filter : L → Set n
|
|
|
248 f⊆P : PL filter
|
|
|
249 filter1 : { p q : L } → PL (λ x → q ⊆ x ) → filter p → p ⊆ q → filter q
|
|
|
250 filter2 : { p q : L } → filter p → filter q → filter (p ∩ q)
|
|
|
251
|
|
|
252 record F-Dense {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where
|
|
|
253 field
|
|
|
254 dense : L → Set n
|
|
|
255 d⊆P : PL dense
|
|
|
256 dense-f : L → L
|
|
|
257 dense-d : { p : L} → PL (λ x → p ⊆ x ) → dense ( dense-f p )
|
|
|
258 dense-p : { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p)
|
|
|
259
|
|
|
260
|
|
1175
|
261 Dense-3 : F-Dense (List (Maybe Two) ) (λ x → ⊤ ) _3⊆_ _3∩_
|
|
431
|
262 Dense-3 = record {
|
|
|
263 dense = λ x → Finite3b x ≡ true
|
|
1175
|
264 ; d⊆P = tt
|
|
431
|
265 ; dense-f = λ x → finite3cov x
|
|
|
266 ; dense-d = λ {p} d → lemma1 p
|
|
|
267 ; dense-p = λ {p} d → lemma2 p
|
|
|
268 } where
|
|
|
269 lemma1 : (p : List (Maybe Two) ) → Finite3b (finite3cov p) ≡ true
|
|
|
270 lemma1 [] = refl
|
|
|
271 lemma1 (just i0 ∷ p) = lemma1 p
|
|
|
272 lemma1 (just i1 ∷ p) = lemma1 p
|
|
|
273 lemma1 (nothing ∷ p) = lemma1 p
|
|
|
274 lemma2 : (p : List (Maybe Two)) → p 3⊆ finite3cov p
|
|
|
275 lemma2 [] = refl
|
|
|
276 lemma2 (just i0 ∷ p) = lemma2 p
|
|
|
277 lemma2 (just i1 ∷ p) = lemma2 p
|
|
|
278 lemma2 (nothing ∷ p) = lemma2 p
|
|
|
279
|
|
|
280 -- min = Data.Nat._⊓_
|
|
|
281 -- m≤m⊔n = Data.Nat._⊔_
|
|
|
282 -- open import Data.Nat.Properties
|
|
|
283
|
