Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/filter.agda @ 456:9207b0c3cfe9
fix filter on subset of Power P
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 17 Mar 2022 15:36:24 +0900 |
| parents | d5909d3c725a |
| children | 5f8243d1d41b |
| rev | line source |
|---|---|
| 431 | 1 open import Level |
| 2 open import Ordinals | |
| 3 module filter {n : Level } (O : Ordinals {n}) where | |
| 4 | |
| 5 open import zf | |
| 6 open import logic | |
| 7 import OD | |
| 8 | |
| 9 open import Relation.Nullary | |
| 10 open import Data.Empty | |
| 11 open import Relation.Binary.Core | |
| 12 open import Relation.Binary.PropositionalEquality | |
| 13 import BAlgbra | |
| 14 | |
| 15 open BAlgbra O | |
| 16 | |
| 17 open inOrdinal O | |
| 18 open OD O | |
| 19 open OD.OD | |
| 20 open ODAxiom odAxiom | |
| 21 | |
| 22 import OrdUtil | |
| 23 import ODUtil | |
| 24 open Ordinals.Ordinals O | |
| 25 open Ordinals.IsOrdinals isOrdinal | |
| 26 open Ordinals.IsNext isNext | |
| 27 open OrdUtil O | |
| 28 open ODUtil O | |
| 29 | |
| 30 | |
| 31 import ODC | |
| 32 open ODC O | |
| 33 | |
| 34 open _∧_ | |
| 35 open _∨_ | |
| 36 open Bool | |
| 37 | |
| 38 -- Kunen p.76 and p.53, we use ⊆ | |
| 39 record Filter ( L : HOD ) : Set (suc n) where | |
| 40 field | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
41 filter : HOD |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
42 f⊆L : filter ⊆ L |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
43 filter1 : { p q : HOD } → L ∋ q → filter ∋ p → p ⊆ q → filter ∋ q |
| 431 | 44 filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) |
| 45 | |
| 46 open Filter | |
| 47 | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
48 record prime-filter { L : HOD } (F : Filter L) : Set (suc (suc n)) where |
| 431 | 49 field |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
50 proper : ¬ (filter F ∋ od∅) |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
51 prime : {p q : HOD } → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q ) |
| 431 | 52 |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
53 record ultra-filter { L : HOD } (P : HOD ) (F : Filter L) : Set (suc (suc n)) where |
| 431 | 54 field |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
55 L⊆PP : L ⊆ Power P |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
56 proper : ¬ (filter F ∋ od∅) |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
57 ultra : {p : HOD } → L ∋ p → ( filter F ∋ p ) ∨ ( filter F ∋ ( P ＼ p) ) |
| 431 | 58 |
| 59 open _⊆_ | |
| 60 | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
61 ∈-filter : {L p : HOD} → (F : Filter L ) → filter F ∋ p → L ∋ p |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
62 ∈-filter {L} {p} F lt = {!!} -- power→⊆ L p ( incl ? lt ) |
| 431 | 63 |
| 64 ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L | |
| 65 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) } | |
| 66 | |
| 67 ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L | |
| 68 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) } | |
| 69 | |
| 70 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q | |
| 71 q∩q⊆q = record { incl = λ lt → proj1 lt } | |
| 72 | |
| 73 open HOD | |
| 74 | |
| 75 ----- | |
| 76 -- | |
| 77 -- ultra filter is prime | |
| 78 -- | |
| 79 | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
80 filter-lemma1 : {P L : HOD} → (F : Filter L) → ∀ {p q : HOD } → ultra-filter P F → prime-filter F |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
81 filter-lemma1 {P} {L} F u = record { |
| 431 | 82 proper = ultra-filter.proper u |
| 83 ; prime = lemma3 | |
| 84 } where | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
85 lemma3 : {p q : HOD} → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q ) |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
86 lemma3 {p} {q} lt with ultra-filter.ultra u {!!} -- (∪-lemma1 (∈-filter P lt) ) |
| 431 | 87 ... | case1 p∈P = case1 p∈P |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
88 ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (L ＼ p)} {!!} lemma7 lemma8) where |
| 431 | 89 lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h= (q ∩ (L ＼ p)) |
| 90 lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt ⟫ | |
| 91 ; eq← = λ {x} lt → ⟪ case2 (proj1 lt) , proj2 lt ⟫ | |
| 92 } where | |
| 93 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x | |
| 94 lemma4 x lt with proj1 lt | |
| 95 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) | |
| 96 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
|
97 lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p)) |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
98 lemma6 = filter2 F lt ¬p∈P |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
99 lemma7 : filter F ∋ (q ∩ (L ＼ p)) |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
100 lemma7 = subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) {!!} |
| 431 | 101 lemma8 : (q ∩ (L ＼ p)) ⊆ q |
| 102 lemma8 = q∩q⊆q | |
| 103 | |
| 104 ----- | |
| 105 -- | |
| 106 -- if Filter contains L, prime filter is ultra | |
| 107 -- | |
| 108 | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
109 filter-lemma2 : {P L : HOD} → (F : Filter L) → filter F ∋ L → prime-filter F → ultra-filter P F |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
110 filter-lemma2 {P} {L} F f∋L prime = record { |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
111 L⊆PP = {!!} |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
112 ; proper = prime-filter.proper prime |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
113 ; ultra = λ {p} p⊆L → prime-filter.prime prime {!!} -- (lemma p p⊆L) |
| 431 | 114 } where |
| 115 open _==_ | |
| 116 p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) | |
| 117 eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x) | |
| 118 eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x | |
| 119 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫ | |
| 120 eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) &iso (incl p⊆L ( subst (λ k → odef p k) (sym &iso) p∋x )) | |
| 121 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
122 lemma : (p : HOD) → p ⊆ L → filter F ∋ (p ∪ (P ＼ p)) |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
123 lemma p p⊆L = {!!} -- subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L |
| 431 | 124 |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
125 record Dense (L : HOD ) : Set (suc n) where |
| 431 | 126 field |
| 127 dense : HOD | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
128 d⊆P : dense ⊆ L |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
129 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
|
130 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
|
131 dense-p : { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p |
| 431 | 132 |
| 133 record Ideal ( L : HOD ) : Set (suc n) where | |
| 134 field | |
| 135 ideal : HOD | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
136 i⊆L : ideal ⊆ L |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
137 ideal1 : { p q : HOD } → L ∋ q → ideal ∋ p → q ⊆ p → ideal ∋ q |
| 431 | 138 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) |
| 139 | |
| 140 open Ideal | |
| 141 | |
| 142 proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n | |
| 143 proper-ideal {L} P {p} = ideal P ∋ od∅ | |
| 144 | |
| 145 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n | |
| 146 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q ) | |
| 147 | |
| 148 | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
149 record GenericFilter (L : HOD) : Set (suc n) where |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
150 field |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
151 genf : Filter L |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
152 generic : (D : Dense L ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ ) |
| 431 | 153 |