Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison generic-filter.agda @ 388:19687f3304c9
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 25 Jul 2020 12:54:28 +0900 |
parents | 8b0715e28b33 |
children | cb183674facf |
comparison
equal
deleted
inserted
replaced
387:8b0715e28b33 | 388:19687f3304c9 |
---|---|
58 record _f⊆_ (f g : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where | 58 record _f⊆_ (f g : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where |
59 field | 59 field |
60 extend : {x : Nat} → (fr : dom f (lift x) ) → dom g (lift x ) | 60 extend : {x : Nat} → (fr : dom f (lift x) ) → dom g (lift x ) |
61 feq : {x : Nat} → {fr : dom f (lift x) } → pmap f (lift x) fr ≡ pmap g (lift x) (extend fr) | 61 feq : {x : Nat} → {fr : dom f (lift x) } → pmap f (lift x) fr ≡ pmap g (lift x) (extend fr) |
62 | 62 |
63 record Gf (f : Nat → Two) (p : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where | |
64 field | |
65 gn : Nat | |
66 f<n : (f ↑ gn) f⊆ p | |
67 | |
68 record FiniteF (p : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where | 63 record FiniteF (p : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where |
69 field | 64 field |
70 f-max : Nat | 65 f-max : Nat |
71 f-func : Nat → Two | 66 f-func : Nat → Two |
72 f-p⊆f : p f⊆ (f-func ↑ f-max) | 67 f-p⊆f : p f⊆ (f-func ↑ f-max) |
82 -- ; dense-f = λ x → record { dom = {!!} ; pmap = {!!} } | 77 -- ; dense-f = λ x → record { dom = {!!} ; pmap = {!!} } |
83 -- ; dense-d = λ {p} d → {!!} | 78 -- ; dense-d = λ {p} d → {!!} |
84 -- ; dense-p = λ {p} d → {!!} | 79 -- ; dense-p = λ {p} d → {!!} |
85 -- } | 80 -- } |
86 | 81 |
87 open Gf | |
88 open _f⊆_ | 82 open _f⊆_ |
89 open import Data.Nat.Properties | 83 open import Data.Nat.Properties |
90 | |
91 GF : (Nat → Two ) → F-Filter (PFunc (Lift n Nat) (Lift n Two)) (λ x → Lift (suc n) (One {n}) ) _f⊆_ _f∩_ | |
92 GF f = record { | |
93 filter = λ p → Gf f p | |
94 ; f⊆P = lift OneObj | |
95 ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q } | |
96 ; filter2 = λ {p} {q} fp fq → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq } | |
97 } where | |
98 f1 : {p q : PFunc (Lift n Nat) (Lift n Two) } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q | |
99 f1 {p} {q} fp p⊆q = record { extend = λ {x} x<g → extend p⊆q (extend (f<n fp ) x<g) ; feq = λ {x} {fr} → lemma {x} {fr} } where | |
100 lemma : {x : Nat} {fr : Lift n (x ≤ gn fp)} → pmap (f ↑ gn fp) (lift x) fr ≡ pmap q (lift x) (extend p⊆q (extend (f<n fp) fr)) | |
101 lemma {x} {fr} = begin | |
102 pmap (f ↑ gn fp) (lift x) fr | |
103 ≡⟨ feq (f<n fp ) ⟩ | |
104 pmap p (lift x) (extend (f<n fp) fr) | |
105 ≡⟨ feq p⊆q ⟩ | |
106 pmap q (lift x) (extend p⊆q (extend (f<n fp) fr)) | |
107 ∎ where open ≡-Reasoning | |
108 f2 : {p q : PFunc (Lift n Nat) (Lift n Two) } → (fp : Gf f p ) → (fq : Gf f q ) → (f ↑ (min (gn fp) (gn fq))) f⊆ (p f∩ q) | |
109 f2 {p} {q} fp fq = record { extend = λ {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where | |
110 fmin : PFunc (Lift n Nat) (Lift n Two) | |
111 fmin = f ↑ (min (gn fp) (gn fq)) | |
112 lemma1 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p (lift x)) (gr : dom q (lift x)) → pmap p (lift x) fr ≡ pmap q (lift x) gr | |
113 lemma1 {x} x<g fr gr = begin | |
114 pmap p (lift x) fr | |
115 ≡⟨ meq p ⟩ | |
116 pmap p (lift x) (extend (f<n fp) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _)))) | |
117 ≡⟨ sym (feq (f<n fp)) ⟩ | |
118 pmap (f ↑ (min (gn fp) (gn fq))) (lift x) x<g | |
119 ≡⟨ feq (f<n fq) ⟩ | |
120 pmap q (lift x) (extend (f<n fq) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _)))) | |
121 ≡⟨ meq q ⟩ | |
122 pmap q (lift x) gr | |
123 ∎ where open ≡-Reasoning | |
124 lemma2 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → dom (p f∩ q) (lift x) | |
125 lemma2 x<g = record { proj1 = extend (f<n fp ) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))) ; | |
126 proj2 = record {proj1 = extend (f<n fq ) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))) ; proj2 = lemma1 x<g }} | |
127 f∩→⊆ : (p q : PFunc (Lift n Nat) (Lift n Two) ) → (p f∩ q ) f⊆ q | |
128 f∩→⊆ p q = record { | |
129 extend = λ {x} pq → proj1 (proj2 pq) | |
130 ; feq = λ {x} {fr} → (proj2 (proj2 fr)) (proj1 fr) (proj1 (proj2 fr)) | |
131 } | |
132 lemma3 : {x : Nat} → ( fr : Lift n (x ≤ min (gn fp) (gn fq))) → pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr ≡ pmap (p f∩ q) (lift x) (lemma2 fr) | |
133 lemma3 {x} fr = | |
134 pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr | |
135 ≡⟨ feq (f<n fq) ⟩ | |
136 pmap q (lift x) (extend (f<n fq) ( lift (≤-trans (lower fr) (m⊓n≤n _ _)) )) | |
137 ≡⟨ sym (feq (f∩→⊆ p q ) {x} {lemma2 fr} ) ⟩ | |
138 pmap (p f∩ q) (lift x) (lemma2 fr) | |
139 ∎ where open ≡-Reasoning | |
140 | 84 |
141 | 85 |
142 ODSuc : (y : HOD) → infinite ∋ y → HOD | 86 ODSuc : (y : HOD) → infinite ∋ y → HOD |
143 ODSuc y lt = Union (y , (y , y)) | 87 ODSuc y lt = Union (y , (y , y)) |
144 | 88 |
198 ω→2f x = {!!} | 142 ω→2f x = {!!} |
199 | 143 |
200 ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD | 144 ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD |
201 ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) )) | 145 ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) )) |
202 | 146 |
203 record Gfo (x : Ordinal) : Set n where | |
204 field | |
205 gfunc : Ordinal | |
206 gmax : Ordinal | |
207 gcond : (odef ω→2 gfunc) ∧ (odef infinite gmax) | |
208 gfdef : {!!} -- ( ↑n (ord→od gfunc) (ord→od gmax) (subst₂ ? ? ? gcond) ) ⊆ ord→od x | |
209 pcond : odef HODω2 x | |
210 | |
211 open Gfo | |
212 | |
213 HODGf : HOD | |
214 HODGf = record { od = record { def = λ x → Gfo x } ; odmax = next o∅ ; <odmax = {!!} } | |
215 | |
216 G : (Nat → Two) → Filter HODω2 | |
217 G f = record { | |
218 filter = HODGf | |
219 ; f⊆PL = {!!} | |
220 ; filter1 = {!!} | |
221 ; filter2 = {!!} | |
222 } where | |
223 filter0 : HOD | |
224 filter0 = {!!} | |
225 f⊆PL1 : filter0 ⊆ Power HODω2 | |
226 f⊆PL1 = {!!} | |
227 filter11 : { p q : HOD } → q ⊆ HODω2 → filter0 ∋ p → p ⊆ q → filter0 ∋ q | |
228 filter11 = {!!} | |
229 filter12 : { p q : HOD } → filter0 ∋ p → filter0 ∋ q → filter0 ∋ (p ∩ q) | |
230 filter12 = {!!} | |
231 | |
232 -- the set of finite partial functions from ω to 2 | 147 -- the set of finite partial functions from ω to 2 |
233 | 148 |
234 Hω2f : Set (suc n) | 149 Hω2f : Set (suc n) |
235 Hω2f = (Nat → Set n) → Two | 150 Hω2f = (Nat → Set n) → Two |
236 | 151 |
242 field | 157 field |
243 ctl→ : Nat → Ordinal | 158 ctl→ : Nat → Ordinal |
244 ctl← : Ordinal → Nat | 159 ctl← : Ordinal → Nat |
245 ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x | 160 ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x |
246 ctl-iso← : { x : Nat } → ctl← (ctl→ x ) ≡ x | 161 ctl-iso← : { x : Nat } → ctl← (ctl→ x ) ≡ x |
162 | |
163 record CountableHOD : Set (suc (suc n)) where | |
164 field | |
165 phod : HOD | |
166 ptl→ : Nat → Ordinal | |
167 ptl→∈P : (i : Nat) → odef phod (ptl→ i) | |
168 ptl← : (x : Ordinal) → odef phod x → Nat | |
169 ptl-iso→ : { x : Ordinal } → (lt : odef phod x ) → ptl→ (ptl← x lt ) ≡ x | |
170 ptl-iso← : { x : Nat } → ptl← (ptl→ x ) (ptl→∈P x) ≡ x | |
171 | |
247 | 172 |
248 open CountableOrdinal | 173 open CountableOrdinal |
249 | 174 open CountableHOD |
250 PGOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Set n | 175 |
251 PGOD i C p q = ¬ ( odef (ord→od (ctl→ C i)) q ∧ ( (x : Ordinal ) → odef (ord→od p) x → odef (ord→od q) x )) | 176 PGHOD : (P : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD |
252 | 177 PGHOD P i C p = record { od = record { def = λ x → odef (ord→od (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (ord→od p) y → odef (ord→od x) y ) } |
253 PGHOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD | 178 ; odmax = ctl→ C i ; <odmax = λ {y} lt → odefo→o< (proj1 lt)} |
254 PGHOD i C p = record { od = record { def = λ x → PGOD i C {!!} {!!} } ; odmax = {!!} ; <odmax = {!!} } | 179 |
255 | 180 next-p : (P : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → Ordinal |
256 ord-compare : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Ordinal | 181 next-p P i C p with ODC.decp O ( PGHOD P i C p =h= od∅ ) |
257 ord-compare i C p q with ODC.p∨¬p O ( (q : Ordinal ) → PGOD i C p q ) | 182 next-p P i C p | yes y = p |
258 ord-compare i C p q | case1 y = p | 183 next-p P i C p | no not = od→ord (ODC.minimal O (PGHOD P i C p ) not) |
259 ord-compare i C p q | case2 n = od→ord (ODC.minimal O (PGHOD i C p ) (∅< (subst₂ (λ j k → odef j {!!} ) refl {!!} n)) ) | 184 |
260 | 185 data PD (P : CountableHOD ) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) → Set n where |
261 data PD (P : HOD) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) → Set (suc n) where | |
262 pd0 : PD P C o∅ 0 | 186 pd0 : PD P C o∅ 0 |
263 -- pdq : {q pnx : Ordinal } {n : Nat} → (pn : PD P C pnx n ) → odef (ctl→ C n) q → ord→od p0x ⊆ ord→od q → PD P C q (suc n) | 187 pdsuc : {p : Ordinal } {i : Nat} → PD P C p i → PD P C (next-p P i C p) (Suc i) |
264 | 188 |
265 P-GenericFilter : {P : HOD} → (C : CountableOrdinal) → GenericFilter P | 189 record PDN (P : CountableHOD ) (C : CountableOrdinal) (x : Ordinal) : Set n where |
190 field | |
191 px∈ω : odef (phod P) x | |
192 pdod : PD P C x (ptl← P x px∈ω) | |
193 | |
194 open PDN | |
195 | |
196 PDHOD : (P : CountableHOD ) → (C : CountableOrdinal) → HOD | |
197 PDHOD P C = record { od = record { def = λ x → PDN P C x } | |
198 ; odmax = odmax (phod P) ; <odmax = λ {y} lt → <odmax (phod P) (px∈ω lt) } where | |
199 | |
200 -- | |
201 -- p 0 ≡ ∅ | |
202 -- p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q | |
203 --- else p n | |
204 | |
205 Gω2r : (x : Ordinal) → (lt : infinite ∋ ord→od x ) → Hω2 (ω→nat (ord→od x) lt ) x | |
206 Gω2r x = subst (λ k → (lt : odef infinite (od→ord (ord→od x))) → Hω2 (ω→nat (ord→od x) lt ) k ) diso ( ε-induction {ψ} {!!} (ord→od x)) where | |
207 ψ : HOD → Set n | |
208 ψ y = (lt : odef infinite (od→ord y) ) → Hω2 (ω→nat y lt ) (od→ord y ) | |
209 ind : {x : HOD} → ({y : HOD} → OD.def (od x) (od→ord y) → | |
210 (lt : infinite-d (od→ord y)) → Hω2 (ω→nat y lt) (od→ord y)) → | |
211 (lt : infinite-d (od→ord x)) → Hω2 (ω→nat x lt) (od→ord x) | |
212 ind {x} prev lt with ω→nat x lt | |
213 ... | Zero = subst (λ k → Hω2 Zero k) ? hφ | |
214 ... | Suc t = {!!} | |
215 | |
216 P-GenericFilter : {P : CountableHOD } → (C : CountableOrdinal) → GenericFilter (phod P) | |
266 P-GenericFilter {P} C = record { | 217 P-GenericFilter {P} C = record { |
267 genf = record { filter = {!!} ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} } | 218 genf = record { filter = PDHOD P C ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} } |
268 ; generic = λ D → {!!} | 219 ; generic = λ D → {!!} |
269 } | 220 } |