Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/filter.agda @ 458:882c24efdc3f
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 18 Mar 2022 20:36:42 +0900 |
| parents | 5f8243d1d41b |
| children | 3d84389cc43f |
| rev | line source |
|---|---|
| 457 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 2 | |
| 431 | 3 open import Level |
| 4 open import Ordinals | |
| 5 module filter {n : Level } (O : Ordinals {n}) where | |
| 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 | |
| 15 import BAlgbra | |
| 16 | |
| 17 open BAlgbra O | |
| 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 | |
| 40 -- Kunen p.76 and p.53, we use ⊆ | |
| 458 | 41 record Filter { L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where |
| 431 | 42 field |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
43 filter : HOD |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
44 f⊆L : filter ⊆ L |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
45 filter1 : { p q : HOD } → L ∋ q → filter ∋ p → p ⊆ q → filter ∋ q |
| 431 | 46 filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) |
| 47 | |
| 48 open Filter | |
| 49 | |
| 458 | 50 record prime-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter LP) : Set (suc (suc n)) where |
| 431 | 51 field |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
52 proper : ¬ (filter F ∋ od∅) |
| 458 | 53 prime : {p q : HOD } → L ∋ p → L ∋ q → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q ) |
| 431 | 54 |
| 458 | 55 record ultra-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter LP) : Set (suc (suc n)) where |
| 431 | 56 field |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
57 proper : ¬ (filter F ∋ od∅) |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
58 ultra : {p : HOD } → L ∋ p → ( filter F ∋ p ) ∨ ( filter F ∋ ( P ＼ p) ) |
| 431 | 59 |
| 60 open _⊆_ | |
| 61 | |
| 458 | 62 ∈-filter : {L P p : HOD} → {LP : L ⊆ Power P} → (F : Filter LP ) → filter F ∋ p → L ∋ p |
| 63 ∈-filter {L} {p} {LP} F lt = incl ( f⊆L F) lt | |
| 64 | |
| 65 ⊆-filter : {L P p q : HOD } → {LP : L ⊆ Power P } → (F : Filter LP) → L ∋ q → q ⊆ P | |
| 66 ⊆-filter {L} {P} {p} {q} {LP} F lt = power→⊆ P q ( incl LP lt ) | |
| 431 | 67 |
| 68 ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L | |
| 69 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) } | |
| 70 | |
| 71 ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L | |
| 72 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) } | |
| 73 | |
| 74 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q | |
| 75 q∩q⊆q = record { incl = λ lt → proj1 lt } | |
| 76 | |
| 77 open HOD | |
| 78 | |
| 79 ----- | |
| 80 -- | |
| 81 -- ultra filter is prime | |
| 82 -- | |
| 83 | |
| 458 | 84 filter-lemma1 : {P L : HOD} → (LP : L ⊆ Power P) → (F : Filter LP) → ∀ {p q : HOD } → ultra-filter F → prime-filter F |
| 85 filter-lemma1 {P} {L} LP F u = record { | |
| 431 | 86 proper = ultra-filter.proper u |
| 87 ; prime = lemma3 | |
| 88 } where | |
| 458 | 89 lemma3 : {p q : HOD} → L ∋ p → L ∋ q → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q ) |
| 90 lemma3 {p} {q} Lp Lq lt with ultra-filter.ultra u Lp | |
| 91 ... | case1 p∈P = case1 p∈P | |
| 92 ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (P ＼ p)} Lq lemma7 lemma8) where | |
| 93 lemma5 : ((p ∪ q ) ∩ (P ＼ p)) =h= (q ∩ (P ＼ p)) | |
| 431 | 94 lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt ⟫ |
| 95 ; eq← = λ {x} lt → ⟪ case2 (proj1 lt) , proj2 lt ⟫ | |
| 96 } where | |
| 458 | 97 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (P ＼ p)) x → odef q x |
| 431 | 98 lemma4 x lt with proj1 lt |
| 99 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) | |
| 100 lemma4 x lt | case2 qx = qx | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
101 lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p)) |
| 458 | 102 lemma6 = filter2 F lt ¬p∈P |
| 103 lemma7 : filter F ∋ (q ∩ (P ＼ p)) | |
| 104 lemma7 = subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) lemma6 | |
| 105 lemma8 : (q ∩ (P ＼ p)) ⊆ q | |
| 431 | 106 lemma8 = q∩q⊆q |
| 107 | |
| 108 ----- | |
| 109 -- | |
| 110 -- if Filter contains L, prime filter is ultra | |
| 111 -- | |
| 112 | |
| 458 | 113 filter-lemma2 : {P L : HOD} → (LP : L ⊆ Power P) → (F : Filter LP) → filter F ∋ L → prime-filter F → ultra-filter F |
| 114 filter-lemma2 {P} {L} LP F f∋L prime = record { | |
| 115 proper = prime-filter.proper prime | |
| 116 ; ultra = λ {p} p⊆L → prime-filter.prime prime {!!} {!!} {!!} -- (lemma p p⊆L) | |
| 431 | 117 } where |
| 118 open _==_ | |
| 458 | 119 p+1-p=1 : {p : HOD} → p ⊆ P → P =h= (p ∪ (P ＼ p)) |
| 431 | 120 eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x) |
| 121 eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x | |
| 122 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫ | |
| 458 | 123 eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef P k ) &iso (incl p⊆L ( subst (λ k → odef p k) (sym &iso) p∋x )) |
| 431 | 124 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p |
| 458 | 125 lemma : (p : HOD) → p ⊆ P → filter F ∋ (p ∪ (P ＼ p)) |
| 126 lemma p p⊆L = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) {!!} -- f∋L | |
| 431 | 127 |
| 458 | 128 ----- |
| 129 -- | |
| 130 -- if there is a filter , there is a ultra filter under the axiom of choise | |
| 131 -- | |
| 132 | |
| 133 filter→ultra : {P L : HOD} → (LP : L ⊆ Power P) → (F : Filter LP) → ultra-filter F | |
| 134 filter→ultra {P} {L} LP F = ? | |
| 135 | |
| 136 record Dense {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where | |
| 431 | 137 field |
| 138 dense : HOD | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
139 d⊆P : dense ⊆ L |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
140 dense-f : {p : HOD} → L ∋ p → HOD |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
141 dense-d : { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
142 dense-p : { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p |
| 431 | 143 |
| 458 | 144 record Ideal {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where |
| 431 | 145 field |
| 146 ideal : HOD | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
147 i⊆L : ideal ⊆ L |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
148 ideal1 : { p q : HOD } → L ∋ q → ideal ∋ p → q ⊆ p → ideal ∋ q |
| 431 | 149 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) |
| 150 | |
| 151 open Ideal | |
| 152 | |
| 458 | 153 proper-ideal : {L P : HOD} → (LP : L ⊆ Power P) → (P : Ideal LP ) → {p : HOD} → Set n |
| 154 proper-ideal {L} {P} LP I = ideal I ∋ od∅ | |
| 431 | 155 |
| 458 | 156 prime-ideal : {L P : HOD} → (LP : L ⊆ Power P) → Ideal LP → ∀ {p q : HOD } → Set n |
| 157 prime-ideal {L} {P} LP I {p} {q} = ideal I ∋ ( p ∩ q) → ( ideal I ∋ p ) ∨ ( ideal I ∋ q ) | |
| 431 | 158 |
| 159 | |
| 458 | 160 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) : Set (suc n) where |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
161 field |
| 458 | 162 genf : Filter LP |
| 163 generic : (D : Dense LP ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ ) | |
| 431 | 164 |