Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/filter.agda @ 458:882c24efdc3f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 18 Mar 2022 20:36:42 +0900
parents 5f8243d1d41b
children 3d84389cc43f
comparison
equal deleted inserted replaced
457:5f8243d1d41b 458:882c24efdc3f
36 open _∧_ 36 open _∧_
37 open _∨_ 37 open _∨_
38 open Bool 38 open Bool
39 39
40 -- Kunen p.76 and p.53, we use ⊆ 40 -- Kunen p.76 and p.53, we use ⊆
41 record Filter ( L : HOD ) : Set (suc n) where 41 record Filter { L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where
42 field 42 field
43 filter : HOD 43 filter : HOD
44 f⊆L : filter ⊆ L 44 f⊆L : filter ⊆ L
45 filter1 : { p q : HOD } → L ∋ q → filter ∋ p → p ⊆ q → filter ∋ q 45 filter1 : { p q : HOD } → L ∋ q → filter ∋ p → p ⊆ q → filter ∋ q
46 filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) 46 filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
47 47
48 open Filter 48 open Filter
49 49
50 record prime-filter { L : HOD } (F : Filter L) : Set (suc (suc n)) where 50 record prime-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter LP) : Set (suc (suc n)) where
51 field 51 field
52 proper : ¬ (filter F ∋ od∅) 52 proper : ¬ (filter F ∋ od∅)
53 prime : {p q : HOD } → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q ) 53 prime : {p q : HOD } → L ∋ p → L ∋ q → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
54 54
55 record ultra-filter { L : HOD } (P : HOD ) (F : Filter L) : Set (suc (suc n)) where 55 record ultra-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter LP) : Set (suc (suc n)) where
56 field 56 field
57 L⊆PP : L ⊆ Power P
58 proper : ¬ (filter F ∋ od∅) 57 proper : ¬ (filter F ∋ od∅)
59 ultra : {p : HOD } → L ∋ p → ( filter F ∋ p ) ∨ ( filter F ∋ ( P ＼ p) ) 58 ultra : {p : HOD } → L ∋ p → ( filter F ∋ p ) ∨ ( filter F ∋ ( P ＼ p) )
60 59
61 open _⊆_ 60 open _⊆_
62 61
63 ∈-filter : {L p : HOD} → (F : Filter L ) → filter F ∋ p → L ∋ p 62 ∈-filter : {L P p : HOD} → {LP : L ⊆ Power P} → (F : Filter LP ) → filter F ∋ p → L ∋ p
64 ∈-filter {L} {p} F lt = incl ( f⊆L F) lt 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 )
65 67
66 ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L 68 ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L
67 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) } 69 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
68 70
69 ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L 71 ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L
70 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) } 72 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
71
72 ∪-lemma3 : {L P p q : HOD } → L ⊆ Power P → L ∋ (p ∪ q) → L ∋ p
73 ∪-lemma3 = {!!}
74
75 ∪-lemma4 : {L P p q : HOD } → L ⊆ Power P → L ∋ (p ∪ q) → L ∋ q
76 ∪-lemma4 = {!!}
77 73
78 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 74 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q
79 q∩q⊆q = record { incl = λ lt → proj1 lt } 75 q∩q⊆q = record { incl = λ lt → proj1 lt }
80 76
81 open HOD 77 open HOD
83 ----- 79 -----
84 -- 80 --
85 -- ultra filter is prime 81 -- ultra filter is prime
86 -- 82 --
87 83
88 filter-lemma1 : {P L : HOD} → (F : Filter L) → ∀ {p q : HOD } → ultra-filter P F → prime-filter F 84 filter-lemma1 : {P L : HOD} → (LP : L ⊆ Power P) → (F : Filter LP) → ∀ {p q : HOD } → ultra-filter F → prime-filter F
89 filter-lemma1 {P} {L} F u = record { 85 filter-lemma1 {P} {L} LP F u = record {
90 proper = ultra-filter.proper u 86 proper = ultra-filter.proper u
91 ; prime = lemma3 87 ; prime = lemma3
92 } where 88 } where
93 lemma3 : {p q : HOD} → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q ) 89 lemma3 : {p q : HOD} → L ∋ p → L ∋ q → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
94 lemma3 {p} {q} lt with ultra-filter.ultra u (∈-filter F lt) 90 lemma3 {p} {q} Lp Lq lt with ultra-filter.ultra u Lp
95 ... | case1 p∈P = case1 {!!} -- (∪-lemma3 (ultra-filter.L⊆PP u) ? ) -- : OD.def (od (filter F)) (& p) 91 ... | case1 p∈P = case1 p∈P
96 ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (L ＼ p)} {!!} lemma7 lemma8) where 92 ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (P ＼ p)} Lq lemma7 lemma8) where
97 lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h= (q ∩ (L ＼ p)) 93 lemma5 : ((p ∪ q ) ∩ (P ＼ p)) =h= (q ∩ (P ＼ p))
98 lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt ⟫ 94 lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt ⟫
99 ; eq← = λ {x} lt → ⟪ case2 (proj1 lt) , proj2 lt ⟫ 95 ; eq← = λ {x} lt → ⟪ case2 (proj1 lt) , proj2 lt ⟫
100 } where 96 } where
101 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x 97 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (P ＼ p)) x → odef q x
102 lemma4 x lt with proj1 lt 98 lemma4 x lt with proj1 lt
103 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) 99 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
104 lemma4 x lt | case2 qx = qx 100 lemma4 x lt | case2 qx = qx
105 lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p)) 101 lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p))
106 lemma6 = {!!} -- filter2 F lt ¬p∈P 102 lemma6 = filter2 F lt ¬p∈P
107 lemma7 : filter F ∋ (q ∩ (L ＼ p)) 103 lemma7 : filter F ∋ (q ∩ (P ＼ p))
108 lemma7 = subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) {!!} 104 lemma7 = subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) lemma6
109 lemma8 : (q ∩ (L ＼ p)) ⊆ q 105 lemma8 : (q ∩ (P ＼ p)) ⊆ q
110 lemma8 = q∩q⊆q 106 lemma8 = q∩q⊆q
111 107
112 ----- 108 -----
113 -- 109 --
114 -- if Filter contains L, prime filter is ultra 110 -- if Filter contains L, prime filter is ultra
115 -- 111 --
116 112
117 filter-lemma2 : {P L : HOD} → (F : Filter L) → filter F ∋ L → prime-filter F → ultra-filter P F 113 filter-lemma2 : {P L : HOD} → (LP : L ⊆ Power P) → (F : Filter LP) → filter F ∋ L → prime-filter F → ultra-filter F
118 filter-lemma2 {P} {L} F f∋L prime = record { 114 filter-lemma2 {P} {L} LP F f∋L prime = record {
119 L⊆PP = {!!} 115 proper = prime-filter.proper prime
120 ; proper = prime-filter.proper prime 116 ; ultra = λ {p} p⊆L → prime-filter.prime prime {!!} {!!} {!!} -- (lemma p p⊆L)
121 ; ultra = λ {p} p⊆L → prime-filter.prime prime {!!} -- (lemma p p⊆L)
122 } where 117 } where
123 open _==_ 118 open _==_
124 p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) 119 p+1-p=1 : {p : HOD} → p ⊆ P → P =h= (p ∪ (P ＼ p))
125 eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x) 120 eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x)
126 eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x 121 eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
127 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫ 122 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫
128 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 )) 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 ))
129 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p 124 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p
130 lemma : (p : HOD) → p ⊆ L → filter F ∋ (p ∪ (P ＼ p)) 125 lemma : (p : HOD) → p ⊆ P → filter F ∋ (p ∪ (P ＼ p))
131 lemma p p⊆L = {!!} -- subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L 126 lemma p p⊆L = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) {!!} -- f∋L
132 127
133 record Dense (L : HOD ) : Set (suc n) where 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
134 field 137 field
135 dense : HOD 138 dense : HOD
136 d⊆P : dense ⊆ L 139 d⊆P : dense ⊆ L
137 dense-f : {p : HOD} → L ∋ p → HOD 140 dense-f : {p : HOD} → L ∋ p → HOD
138 dense-d : { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt 141 dense-d : { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt
139 dense-p : { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p 142 dense-p : { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p
140 143
141 record Ideal ( L : HOD ) : Set (suc n) where 144 record Ideal {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where
142 field 145 field
143 ideal : HOD 146 ideal : HOD
144 i⊆L : ideal ⊆ L 147 i⊆L : ideal ⊆ L
145 ideal1 : { p q : HOD } → L ∋ q → ideal ∋ p → q ⊆ p → ideal ∋ q 148 ideal1 : { p q : HOD } → L ∋ q → ideal ∋ p → q ⊆ p → ideal ∋ q
146 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) 149 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q)
147 150
148 open Ideal 151 open Ideal
149 152
150 proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n 153 proper-ideal : {L P : HOD} → (LP : L ⊆ Power P) → (P : Ideal LP ) → {p : HOD} → Set n
151 proper-ideal {L} P {p} = ideal P ∋ od∅ 154 proper-ideal {L} {P} LP I = ideal I ∋ od∅
152 155
153 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n 156 prime-ideal : {L P : HOD} → (LP : L ⊆ Power P) → Ideal LP → ∀ {p q : HOD } → Set n
154 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q ) 157 prime-ideal {L} {P} LP I {p} {q} = ideal I ∋ ( p ∩ q) → ( ideal I ∋ p ) ∨ ( ideal I ∋ q )
155 158
156 159
157 record GenericFilter (L : HOD) : Set (suc n) where 160 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) : Set (suc n) where
158 field 161 field
159 genf : Filter L 162 genf : Filter LP
160 generic : (D : Dense L ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ ) 163 generic : (D : Dense LP ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
161 164