Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/maximum-filter.agda @ 1205:83ac320583f8
...
| author | kono |
|---|---|
| date | Fri, 03 Mar 2023 10:42:58 +0800 |
| parents | 6216562a2bce |
| children | 45cd80181a29 |
| rev | line source |
|---|---|
| 457 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 2 | |
| 431 | 3 open import Level |
| 4 open import Ordinals | |
| 1153 | 5 module maximum-filter {n : Level } (O : Ordinals {n}) where |
| 431 | 6 |
| 7 open import zf | |
| 8 open import logic | |
| 9 import OD | |
| 10 | |
| 11 open import Relation.Nullary | |
| 12 open import Data.Empty | |
| 13 open import Relation.Binary.Core | |
| 14 open import Relation.Binary.PropositionalEquality | |
| 1124 | 15 import BAlgebra |
| 431 | 16 |
| 1124 | 17 open BAlgebra O |
| 431 | 18 |
| 19 open inOrdinal O | |
| 20 open OD O | |
| 21 open OD.OD | |
| 22 open ODAxiom odAxiom | |
| 23 | |
| 24 import OrdUtil | |
| 25 import ODUtil | |
| 26 open Ordinals.Ordinals O | |
| 27 open Ordinals.IsOrdinals isOrdinal | |
| 28 open Ordinals.IsNext isNext | |
| 29 open OrdUtil O | |
| 30 open ODUtil O | |
| 31 | |
| 32 | |
| 33 import ODC | |
| 34 open ODC O | |
| 35 | |
| 36 open _∧_ | |
| 37 open _∨_ | |
| 38 open Bool | |
| 39 | |
| 1153 | 40 open import filter O |
| 431 | 41 |
| 42 open Filter | |
| 43 | |
| 44 | |
| 1153 | 45 open import Relation.Binary |
| 46 open import Relation.Binary.Structures | |
| 1126 | 47 |
| 48 PO : IsStrictPartialOrder _≡_ _⊂_ | |
| 49 PO = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans } | |
| 50 ; trans = λ {a} {b} {c} → trans-⊂ {a} {b} {c} | |
| 1133 | 51 ; irrefl = λ x=y x<y → o<¬≡ (cong (&) x=y) (proj1 x<y) |
| 52 ; <-resp-≈ = record { fst = ( λ {x} {y} {y1} y=y1 xy1 → subst (λ k → x ⊂ k) y=y1 xy1 ) | |
| 53 ; snd = (λ {x} {x1} {y} x=x1 x1y → subst (λ k → k ⊂ x) x=x1 x1y ) } } | |
| 1126 | 54 |
| 1153 | 55 import zorn |
| 1126 | 56 open zorn O _⊂_ PO |
| 574 | 57 |
| 1158 | 58 |
| 59 -- all filter contains F | |
| 60 F⊆X : { L P : HOD } (LP : L ⊆ Power P) → Filter {L} {P} LP → HOD | |
| 61 F⊆X {L} {P} LP F = record { od = record { def = λ x → IsFilter {L} {P} LP x ∧ ( filter F ⊆ * x) } ; odmax = osuc (& L) | |
| 62 ; <odmax = λ {x} lt → fx00 lt } where | |
| 63 fx00 : {x : Ordinal } → IsFilter LP x ∧ filter F ⊆ * x → x o< osuc (& L) | |
| 64 fx00 {x} lt = subst (λ k → k o< osuc (& L)) &iso ( ⊆→o≤ (IsFilter.f⊆L (proj1 lt )) ) | |
| 65 | |
| 1155 | 66 F→Maximum : {L P : HOD} (LP : L ⊆ Power P) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) |
| 1136 | 67 → (F : Filter {L} {P} LP) → o∅ o< & L → {y : Ordinal } → odef (filter F) y → (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP F |
| 1155 | 68 F→Maximum {L} {P} LP CAP F 0<L {y} 0<F Fprop = record { mf = mf ; F⊆mf = subst (λ k → filter F ⊆ k ) (sym *iso) mf52 |
| 1140 | 69 ; proper = subst (λ k → ¬ ( odef (filter mf ) k)) (sym ord-od∅) ( IsFilter.proper imf) ; is-maximum = mf50 } where |
| 1133 | 70 FX : HOD |
| 71 FX = F⊆X {L} {P} LP F | |
| 1137 | 72 oF = & (filter F) |
| 73 mf11 : { p q : Ordinal } → odef L q → odef (* oF) p → (* p) ⊆ (* q) → odef (* oF) q | |
| 74 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) | |
| 75 (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp) p⊆q ) | |
| 76 mf12 : { p q : Ordinal } → odef (* oF) p → odef (* oF) q → odef L (& ((* p) ∩ (* q))) → odef (* oF) (& ((* p) ∩ (* q))) | |
| 77 mf12 {p} {q} Fp Fq Lpq = subst (λ k → odef k (& ((* p) ∩ (* q))) ) (sym *iso) | |
| 78 ( filter2 F (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp) (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fq) Lpq) | |
| 1138 | 79 FX∋F : odef FX (& (filter F)) |
| 1137 | 80 FX∋F = ⟪ record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) (f⊆L F) ; filter1 = mf11 ; filter2 = mf12 |
| 81 ; proper = subst₂ (λ j k → ¬ (odef j k) ) (sym *iso) ord-od∅ Fprop } | |
| 82 , subst (λ k → filter F ⊆ k ) (sym *iso) ( λ x → x ) ⟫ | |
| 1139 | 83 -- |
| 84 -- if filter B (which contains F) is transitive, Union B is also a filter which contains F | |
| 85 -- and this is a SUP | |
| 86 -- | |
| 1133 | 87 SUP⊆ : (B : HOD) → B ⊆ FX → IsTotalOrderSet B → SUP FX B |
| 1138 | 88 SUP⊆ B B⊆FX OB with trio< (& B) o∅ |
| 89 ... | tri< a ¬b ¬c = ⊥-elim (¬x<0 a ) | |
| 90 ... | tri≈ ¬a b ¬c = record { sup = filter F ; isSUP = record { ax = FX∋F ; x≤sup = λ {y} zy → ⊥-elim (o<¬≡ (sym b) (∈∅< zy)) } } | |
| 1140 | 91 ... | tri> ¬a ¬b 0<B = record { sup = Union B ; isSUP = record { ax = mf13 ; x≤sup = mf40 } } where |
| 1138 | 92 mf20 : HOD |
| 93 mf20 = ODC.minimal O B (λ eq → (o<¬≡ (cong (&) (sym (==→o≡ eq))) (subst (λ k → k o< & B) (sym ord-od∅) 0<B ))) | |
| 94 mf18 : odef B (& mf20 ) | |
| 95 mf18 = ODC.x∋minimal O B (λ eq → (o<¬≡ (cong (&) (sym (==→o≡ eq))) (subst (λ k → k o< & B) (sym ord-od∅) 0<B ))) | |
| 1137 | 96 mf16 : Union B ⊆ L |
| 1138 | 97 mf16 record { owner = b ; ao = Bb ; ox = bx } = IsFilter.f⊆L ( proj1 ( B⊆FX Bb )) bx |
| 1137 | 98 mf17 : {p q : Ordinal} → odef L q → odef (* (& (Union B))) p → * p ⊆ * q → odef (* (& (Union B))) q |
| 99 mf17 {p} {q} Lq bp p⊆q with subst (λ k → odef k p ) *iso bp | |
| 100 ... | record { owner = owner ; ao = ao ; ox = ox } = subst (λ k → odef k q) (sym *iso) | |
| 1138 | 101 record { owner = owner ; ao = ao ; ox = IsFilter.filter1 mf30 Lq ox p⊆q } where |
| 102 mf30 : IsFilter {L} {P} LP owner | |
| 103 mf30 = proj1 ( B⊆FX ao ) | |
| 104 mf31 : {p q : Ordinal} → odef (* (& (Union B))) p → odef (* (& (Union B))) q → odef L (& ((* p) ∩ (* q))) → odef (* (& (Union B))) (& ((* p) ∩ (* q))) | |
| 105 mf31 {p} {q} bp bq Lpq with subst (λ k → odef k p ) *iso bp | subst (λ k → odef k q ) *iso bq | |
| 106 ... | record { owner = bp ; ao = Bbp ; ox = bbp } | record { owner = bq ; ao = Bbq ; ox = bbq } | |
| 107 with OB (subst (λ k → odef B k) (sym &iso) Bbp) (subst (λ k → odef B k) (sym &iso) Bbq) | |
| 1140 | 108 ... | tri< bp⊂bq ¬b ¬c = subst₂ (λ j k → odef j k ) (sym *iso) refl record { owner = bq ; ao = Bbq ; ox = mf36 } where |
| 109 mf36 : odef (* bq) (& ((* p) ∩ (* q))) | |
| 110 mf36 = IsFilter.filter2 mf30 (proj2 bp⊂bq bbp) bbq Lpq where | |
| 111 mf30 : IsFilter {L} {P} LP bq | |
| 112 mf30 = proj1 ( B⊆FX Bbq ) | |
| 113 ... | tri≈ ¬a bq=bp ¬c = subst₂ (λ j k → odef j k ) (sym *iso) refl record { owner = bp ; ao = Bbp ; ox = mf36 } where | |
| 114 mf36 : odef (* bp) (& ((* p) ∩ (* q))) | |
| 115 mf36 = IsFilter.filter2 mf30 bbp (subst (λ k → odef k q) (sym bq=bp) bbq) Lpq where | |
| 116 mf30 : IsFilter {L} {P} LP bp | |
| 117 mf30 = proj1 ( B⊆FX Bbp ) | |
| 118 ... | tri> ¬a ¬b bq⊂bp = subst₂ (λ j k → odef j k ) (sym *iso) refl record { owner = bp ; ao = Bbp ; ox = mf36 } where | |
| 119 mf36 : odef (* bp) (& ((* p) ∩ (* q))) | |
| 120 mf36 = IsFilter.filter2 mf30 bbp (proj2 bq⊂bp bbq) Lpq where | |
| 121 mf30 : IsFilter {L} {P} LP bp | |
| 122 mf30 = proj1 ( B⊆FX Bbp ) | |
| 1139 | 123 mf32 : ¬ odef (Union B) o∅ |
| 124 mf32 record { owner = owner ; ao = bo ; ox = o0 } with proj1 ( B⊆FX bo ) | |
| 125 ... | record { f⊆L = f⊆L ; filter1 = filter1 ; filter2 = filter2 ; proper = proper } = ⊥-elim ( proper o0 ) | |
| 1138 | 126 mf14 : IsFilter LP (& (Union B)) |
| 1139 | 127 mf14 = record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) mf16 ; filter1 = mf17 ; filter2 = mf31 ; proper = subst (λ k → ¬ odef k o∅) (sym *iso) mf32 } |
| 1137 | 128 mf15 : filter F ⊆ Union B |
| 1138 | 129 mf15 {x} Fx = record { owner = & mf20 ; ao = mf18 ; ox = subst (λ k → odef k x) (sym *iso) (mf22 Fx) } where |
| 130 mf22 : odef (filter F) x → odef mf20 x | |
| 131 mf22 Fx = subst (λ k → odef k x) *iso ( proj2 (B⊆FX mf18) Fx ) | |
| 1137 | 132 mf13 : odef FX (& (Union B)) |
| 133 mf13 = ⟪ mf14 , subst (λ k → filter F ⊆ k ) (sym *iso) mf15 ⟫ | |
| 1140 | 134 mf42 : {z : Ordinal} → odef B z → * z ⊆ Union B |
| 135 mf42 {z} Bz {x} zx = record { owner = _ ; ao = Bz ; ox = zx } | |
| 136 mf40 : {z : Ordinal} → odef B z → (z ≡ & (Union B)) ∨ ( * z ⊂ * (& (Union B)) ) | |
| 137 mf40 {z} Bz with B⊆FX Bz | |
| 138 ... | ⟪ filterz , F⊆z ⟫ with osuc-≡< ( ⊆→o≤ {* z} {Union B} (mf42 Bz) ) | |
| 139 ... | case1 eq = case1 (trans (sym &iso) eq ) | |
| 140 ... | case2 lt = case2 ⟪ subst₂ (λ j k → j o< & k ) refl (sym *iso) lt , subst (λ k → * z ⊆ k) (sym *iso) (mf42 Bz) ⟫ | |
| 1134 | 141 mx : Maximal FX |
| 142 mx = Zorn-lemma (∈∅< FX∋F) SUP⊆ | |
| 1138 | 143 imf : IsFilter {L} {P} LP (& (Maximal.maximal mx)) |
| 1134 | 144 imf = proj1 (Maximal.as mx) |
| 145 mf00 : (* (& (Maximal.maximal mx))) ⊆ L | |
| 1138 | 146 mf00 = IsFilter.f⊆L imf |
| 1134 | 147 mf01 : { p q : HOD } → L ∋ q → (* (& (Maximal.maximal mx))) ∋ p → p ⊆ q → (* (& (Maximal.maximal mx))) ∋ q |
| 1138 | 148 mf01 {p} {q} Lq Fq p⊆q = IsFilter.filter1 imf Lq Fq |
| 1134 | 149 (λ {x} lt → subst (λ k → odef k x) (sym *iso) ( p⊆q (subst (λ k → odef k x) *iso lt ) )) |
| 150 mf02 : { p q : HOD } → (* (& (Maximal.maximal mx))) ∋ p → (* (& (Maximal.maximal mx))) ∋ q → L ∋ (p ∩ q) | |
| 151 → (* (& (Maximal.maximal mx))) ∋ (p ∩ q) | |
| 152 mf02 {p} {q} Fp Fq Lpq = subst₂ (λ j k → odef (* (& (Maximal.maximal mx))) (& (j ∩ k ))) *iso *iso ( | |
| 1138 | 153 IsFilter.filter2 imf Fp Fq (subst₂ (λ j k → odef L (& (j ∩ k ))) (sym *iso) (sym *iso) Lpq )) |
| 1134 | 154 mf : Filter {L} {P} LP |
| 155 mf = record { filter = * (& (Maximal.maximal mx)) ; f⊆L = mf00 | |
| 156 ; filter1 = mf01 | |
| 157 ; filter2 = mf02 } | |
|
1141
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
158 mf52 : filter F ⊆ Maximal.maximal mx |
|
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
159 mf52 = subst (λ k → filter F ⊆ k ) *iso (proj2 mf53) where |
|
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
160 mf53 : FX ∋ Maximal.maximal mx |
|
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
161 mf53 = Maximal.as mx |
| 1140 | 162 mf50 : (f : Filter LP) → ¬ (filter f ∋ od∅) → filter F ⊆ filter f → ¬ (* (& (zorn.Maximal.maximal mx)) ⊂ filter f) |
| 163 mf50 f proper F⊆f = subst (λ k → ¬ ( k ⊂ filter f )) (sym *iso) (Maximal.¬maximal<x mx ⟪ Filter-is-Filter {L} {P} LP f proper , mf51 ⟫ ) where | |
| 164 mf51 : filter F ⊆ * (& (filter f)) | |
|
1141
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
165 mf51 = subst (λ k → filter F ⊆ k ) (sym *iso) F⊆f |
| 1134 | 166 |
| 1155 | 167 F→ultra : {L P : HOD} (LP : L ⊆ Power P) → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) |
| 1136 | 168 → (F : Filter {L} {P} LP) → (0<L : o∅ o< & L) → {y : Ordinal} → (0<F : odef (filter F) y) → (proper : ¬ (filter F ∋ od∅)) |
| 1155 | 169 → ultra-filter ( MaximumFilter.mf (F→Maximum {L} {P} LP CAP F 0<L 0<F proper )) |
| 170 F→ultra {L} {P} LP CAP F 0<L 0<F proper = max→ultra {L} {P} LP CAP F 0<F (F→Maximum {L} {P} LP CAP F 0<L 0<F proper ) | |
| 481 | 171 |
| 172 |