Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/filter.agda @ 1138:dd18bb8d2893
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 13 Jan 2023 13:03:45 +0900 |
parents | d618788852e5 |
children | 4517d0721b59 |
comparison
equal
deleted
inserted
replaced
1137:d618788852e5 | 1138:dd18bb8d2893 |
---|---|
300 | 300 |
301 open zorn O _⊂_ PO | 301 open zorn O _⊂_ PO |
302 | 302 |
303 open import Relation.Binary.Structures | 303 open import Relation.Binary.Structures |
304 | 304 |
305 record is-filter { L P : HOD } (LP : L ⊆ Power P) (filter : Ordinal ) : Set n where | 305 record IsFilter { L P : HOD } (LP : L ⊆ Power P) (filter : Ordinal ) : Set n where |
306 field | 306 field |
307 f⊆L : (* filter) ⊆ L | 307 f⊆L : (* filter) ⊆ L |
308 filter1 : { p q : Ordinal } → odef L q → odef (* filter) p → (* p) ⊆ (* q) → odef (* filter) q | 308 filter1 : { p q : Ordinal } → odef L q → odef (* filter) p → (* p) ⊆ (* q) → odef (* filter) q |
309 filter2 : { p q : Ordinal } → odef (* filter) p → odef (* filter) q → odef L (& ((* p) ∩ (* q))) → odef (* filter) (& ((* p) ∩ (* q))) | 309 filter2 : { p q : Ordinal } → odef (* filter) p → odef (* filter) q → odef L (& ((* p) ∩ (* q))) → odef (* filter) (& ((* p) ∩ (* q))) |
310 proper : ¬ (odef (* filter ) o∅) | 310 proper : ¬ (odef (* filter ) o∅) |
311 | 311 |
312 -- all filter contains F | 312 -- all filter contains F |
313 F⊆X : { L P : HOD } (LP : L ⊆ Power P) → Filter {L} {P} LP → HOD | 313 F⊆X : { L P : HOD } (LP : L ⊆ Power P) → Filter {L} {P} LP → HOD |
314 F⊆X {L} {P} LP F = record { od = record { def = λ x → is-filter {L} {P} LP x ∧ ( filter F ⊆ * x) } ; odmax = osuc (& L) | 314 F⊆X {L} {P} LP F = record { od = record { def = λ x → IsFilter {L} {P} LP x ∧ ( filter F ⊆ * x) } ; odmax = osuc (& L) |
315 ; <odmax = λ {x} lt → fx00 lt } where | 315 ; <odmax = λ {x} lt → fx00 lt } where |
316 fx00 : {x : Ordinal } → is-filter LP x ∧ filter F ⊆ * x → x o< osuc (& L) | 316 fx00 : {x : Ordinal } → IsFilter LP x ∧ filter F ⊆ * x → x o< osuc (& L) |
317 fx00 {x} lt = subst (λ k → k o< osuc (& L)) &iso ( ⊆→o≤ (is-filter.f⊆L (proj1 lt )) ) | 317 fx00 {x} lt = subst (λ k → k o< osuc (& L)) &iso ( ⊆→o≤ (IsFilter.f⊆L (proj1 lt )) ) |
318 | 318 |
319 F→Maximum : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P \ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) | 319 F→Maximum : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P \ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) |
320 → (F : Filter {L} {P} LP) → o∅ o< & L → {y : Ordinal } → odef (filter F) y → (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP F | 320 → (F : Filter {L} {P} LP) → o∅ o< & L → {y : Ordinal } → odef (filter F) y → (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP F |
321 F→Maximum {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = mf ; F⊆mf = ? | 321 F→Maximum {L} {P} LP NEG CAP F 0<L {y} 0<F Fprop = record { mf = mf ; F⊆mf = ? |
322 ; proper = subst (λ k → ¬ ( odef (filter mf ) k)) (sym ord-od∅) ( is-filter.proper imf) ; is-maximum = {!!} } where | 322 ; proper = subst (λ k → ¬ ( odef (filter mf ) k)) (sym ord-od∅) ( IsFilter.proper imf) ; is-maximum = {!!} } where |
323 FX : HOD | 323 FX : HOD |
324 FX = F⊆X {L} {P} LP F | 324 FX = F⊆X {L} {P} LP F |
325 FX∋F : odef FX (& (filter F)) | |
326 oF = & (filter F) | 325 oF = & (filter F) |
327 mf11 : { p q : Ordinal } → odef L q → odef (* oF) p → (* p) ⊆ (* q) → odef (* oF) q | 326 mf11 : { p q : Ordinal } → odef L q → odef (* oF) p → (* p) ⊆ (* q) → odef (* oF) q |
328 mf11 {p} {q} Lq Fp p⊆q = subst₂ (λ j k → odef j k ) (sym *iso) &iso ( filter1 F (subst (λ k → odef L k) (sym &iso) Lq) | 327 mf11 {p} {q} Lq Fp p⊆q = subst₂ (λ j k → odef j k ) (sym *iso) &iso ( filter1 F (subst (λ k → odef L k) (sym &iso) Lq) |
329 (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp) p⊆q ) | 328 (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp) p⊆q ) |
330 mf12 : { p q : Ordinal } → odef (* oF) p → odef (* oF) q → odef L (& ((* p) ∩ (* q))) → odef (* oF) (& ((* p) ∩ (* q))) | 329 mf12 : { p q : Ordinal } → odef (* oF) p → odef (* oF) q → odef L (& ((* p) ∩ (* q))) → odef (* oF) (& ((* p) ∩ (* q))) |
331 mf12 {p} {q} Fp Fq Lpq = subst (λ k → odef k (& ((* p) ∩ (* q))) ) (sym *iso) | 330 mf12 {p} {q} Fp Fq Lpq = subst (λ k → odef k (& ((* p) ∩ (* q))) ) (sym *iso) |
332 ( filter2 F (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp) (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fq) Lpq) | 331 ( filter2 F (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp) (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fq) Lpq) |
332 FX∋F : odef FX (& (filter F)) | |
333 FX∋F = ⟪ record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) (f⊆L F) ; filter1 = mf11 ; filter2 = mf12 | 333 FX∋F = ⟪ record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) (f⊆L F) ; filter1 = mf11 ; filter2 = mf12 |
334 ; proper = subst₂ (λ j k → ¬ (odef j k) ) (sym *iso) ord-od∅ Fprop } | 334 ; proper = subst₂ (λ j k → ¬ (odef j k) ) (sym *iso) ord-od∅ Fprop } |
335 , subst (λ k → filter F ⊆ k ) (sym *iso) ( λ x → x ) ⟫ | 335 , subst (λ k → filter F ⊆ k ) (sym *iso) ( λ x → x ) ⟫ |
336 SUP⊆ : (B : HOD) → B ⊆ FX → IsTotalOrderSet B → SUP FX B | 336 SUP⊆ : (B : HOD) → B ⊆ FX → IsTotalOrderSet B → SUP FX B |
337 SUP⊆ B B⊆FX OB = record { sup = Union B ; isSUP = record { ax = mf13 ; x≤sup = ? } } where | 337 SUP⊆ B B⊆FX OB with trio< (& B) o∅ |
338 ... | tri< a ¬b ¬c = ⊥-elim (¬x<0 a ) | |
339 ... | tri≈ ¬a b ¬c = record { sup = filter F ; isSUP = record { ax = FX∋F ; x≤sup = λ {y} zy → ⊥-elim (o<¬≡ (sym b) (∈∅< zy)) } } | |
340 ... | tri> ¬a ¬b 0<B = record { sup = Union B ; isSUP = record { ax = mf13 ; x≤sup = ? } } where | |
341 mf20 : HOD | |
342 mf20 = ODC.minimal O B (λ eq → (o<¬≡ (cong (&) (sym (==→o≡ eq))) (subst (λ k → k o< & B) (sym ord-od∅) 0<B ))) | |
343 mf18 : odef B (& mf20 ) | |
344 mf18 = ODC.x∋minimal O B (λ eq → (o<¬≡ (cong (&) (sym (==→o≡ eq))) (subst (λ k → k o< & B) (sym ord-od∅) 0<B ))) | |
338 mf16 : Union B ⊆ L | 345 mf16 : Union B ⊆ L |
339 mf16 record { owner = b ; ao = Bb ; ox = bx } = is-filter.f⊆L ( proj1 ( B⊆FX Bb )) bx | 346 mf16 record { owner = b ; ao = Bb ; ox = bx } = IsFilter.f⊆L ( proj1 ( B⊆FX Bb )) bx |
340 mf17 : {p q : Ordinal} → odef L q → odef (* (& (Union B))) p → * p ⊆ * q → odef (* (& (Union B))) q | 347 mf17 : {p q : Ordinal} → odef L q → odef (* (& (Union B))) p → * p ⊆ * q → odef (* (& (Union B))) q |
341 mf17 {p} {q} Lq bp p⊆q with subst (λ k → odef k p ) *iso bp | 348 mf17 {p} {q} Lq bp p⊆q with subst (λ k → odef k p ) *iso bp |
342 ... | record { owner = owner ; ao = ao ; ox = ox } = subst (λ k → odef k q) (sym *iso) | 349 ... | record { owner = owner ; ao = ao ; ox = ox } = subst (λ k → odef k q) (sym *iso) |
343 record { owner = ? ; ao = ? ; ox = ? } | 350 record { owner = owner ; ao = ao ; ox = IsFilter.filter1 mf30 Lq ox p⊆q } where |
344 mf14 : is-filter LP (& (Union B)) | 351 mf30 : IsFilter {L} {P} LP owner |
345 mf14 = record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) mf16 ; filter1 = mf17 ; filter2 = ? ; proper = ? } | 352 mf30 = proj1 ( B⊆FX ao ) |
353 mf31 : {p q : Ordinal} → odef (* (& (Union B))) p → odef (* (& (Union B))) q → odef L (& ((* p) ∩ (* q))) → odef (* (& (Union B))) (& ((* p) ∩ (* q))) | |
354 mf31 {p} {q} bp bq Lpq with subst (λ k → odef k p ) *iso bp | subst (λ k → odef k q ) *iso bq | |
355 ... | record { owner = bp ; ao = Bbp ; ox = bbp } | record { owner = bq ; ao = Bbq ; ox = bbq } | |
356 with OB (subst (λ k → odef B k) (sym &iso) Bbp) (subst (λ k → odef B k) (sym &iso) Bbq) | |
357 ... | tri< bp⊂bq ¬b ¬c = ? | |
358 ... | tri≈ ¬a bq=bp ¬c = ? | |
359 ... | tri> ¬a ¬b bq⊂bp = ? | |
360 mf14 : IsFilter LP (& (Union B)) | |
361 mf14 = record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) mf16 ; filter1 = mf17 ; filter2 = mf31 ; proper = ? } | |
346 mf15 : filter F ⊆ Union B | 362 mf15 : filter F ⊆ Union B |
347 mf15 {x} Fx = record { owner = ? ; ao = ? ; ox = subst (λ k → odef k x) (sym *iso) Fx } | 363 mf15 {x} Fx = record { owner = & mf20 ; ao = mf18 ; ox = subst (λ k → odef k x) (sym *iso) (mf22 Fx) } where |
364 mf22 : odef (filter F) x → odef mf20 x | |
365 mf22 Fx = subst (λ k → odef k x) *iso ( proj2 (B⊆FX mf18) Fx ) | |
348 mf13 : odef FX (& (Union B)) | 366 mf13 : odef FX (& (Union B)) |
349 mf13 = ⟪ mf14 , subst (λ k → filter F ⊆ k ) (sym *iso) mf15 ⟫ | 367 mf13 = ⟪ mf14 , subst (λ k → filter F ⊆ k ) (sym *iso) mf15 ⟫ |
350 mx : Maximal FX | 368 mx : Maximal FX |
351 mx = Zorn-lemma (∈∅< FX∋F) SUP⊆ | 369 mx = Zorn-lemma (∈∅< FX∋F) SUP⊆ |
352 imf : is-filter {L} {P} LP (& (Maximal.maximal mx)) | 370 imf : IsFilter {L} {P} LP (& (Maximal.maximal mx)) |
353 imf = proj1 (Maximal.as mx) | 371 imf = proj1 (Maximal.as mx) |
354 mf00 : (* (& (Maximal.maximal mx))) ⊆ L | 372 mf00 : (* (& (Maximal.maximal mx))) ⊆ L |
355 mf00 = is-filter.f⊆L imf | 373 mf00 = IsFilter.f⊆L imf |
356 mf01 : { p q : HOD } → L ∋ q → (* (& (Maximal.maximal mx))) ∋ p → p ⊆ q → (* (& (Maximal.maximal mx))) ∋ q | 374 mf01 : { p q : HOD } → L ∋ q → (* (& (Maximal.maximal mx))) ∋ p → p ⊆ q → (* (& (Maximal.maximal mx))) ∋ q |
357 mf01 {p} {q} Lq Fq p⊆q = is-filter.filter1 imf Lq Fq | 375 mf01 {p} {q} Lq Fq p⊆q = IsFilter.filter1 imf Lq Fq |
358 (λ {x} lt → subst (λ k → odef k x) (sym *iso) ( p⊆q (subst (λ k → odef k x) *iso lt ) )) | 376 (λ {x} lt → subst (λ k → odef k x) (sym *iso) ( p⊆q (subst (λ k → odef k x) *iso lt ) )) |
359 mf02 : { p q : HOD } → (* (& (Maximal.maximal mx))) ∋ p → (* (& (Maximal.maximal mx))) ∋ q → L ∋ (p ∩ q) | 377 mf02 : { p q : HOD } → (* (& (Maximal.maximal mx))) ∋ p → (* (& (Maximal.maximal mx))) ∋ q → L ∋ (p ∩ q) |
360 → (* (& (Maximal.maximal mx))) ∋ (p ∩ q) | 378 → (* (& (Maximal.maximal mx))) ∋ (p ∩ q) |
361 mf02 {p} {q} Fp Fq Lpq = subst₂ (λ j k → odef (* (& (Maximal.maximal mx))) (& (j ∩ k ))) *iso *iso ( | 379 mf02 {p} {q} Fp Fq Lpq = subst₂ (λ j k → odef (* (& (Maximal.maximal mx))) (& (j ∩ k ))) *iso *iso ( |
362 is-filter.filter2 imf Fp Fq (subst₂ (λ j k → odef L (& (j ∩ k ))) (sym *iso) (sym *iso) Lpq )) | 380 IsFilter.filter2 imf Fp Fq (subst₂ (λ j k → odef L (& (j ∩ k ))) (sym *iso) (sym *iso) Lpq )) |
363 mf : Filter {L} {P} LP | 381 mf : Filter {L} {P} LP |
364 mf = record { filter = * (& (Maximal.maximal mx)) ; f⊆L = mf00 | 382 mf = record { filter = * (& (Maximal.maximal mx)) ; f⊆L = mf00 |
365 ; filter1 = mf01 | 383 ; filter1 = mf01 |
366 ; filter2 = mf02 } | 384 ; filter2 = mf02 } |
367 | 385 |