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

comparison src/generic-filter.agda @ 455:d5909d3c725a

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 Thu, 17 Mar 2022 14:04:25 +0900
parents e5f0ac638c01
children 5f8243d1d41b
comparison
equal deleted inserted replaced
454:0d3d72dba75b 455:d5909d3c725a
71 71
72 open CountableModel 72 open CountableModel
73 73
74 ---- 74 ----
75 -- a(n) ∈ M 75 -- a(n) ∈ M
76 -- ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q 76 -- ∃ q ∈ Power P → q ∈ a(n) ∧ q ⊆ p(n)
77 -- 77 --
78 PGHOD : (i : Nat) (P : HOD) (C : CountableModel ) → (p : Ordinal) → HOD 78 PGHOD : (i : Nat) (P : HOD) (C : CountableModel ) → (p : Ordinal) → HOD
79 PGHOD i P C p = record { od = record { def = λ x → 79 PGHOD i P C p = record { od = record { def = λ x →
80 odef (Power P) x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* p) y → odef (* x) y ) } 80 odef (Power P) x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* x) y → odef (* p) y ) }
81 ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) } 81 ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) }
82 82
83 --- 83 ---
84 -- p(n+1) = if (f n) != ∅ then (f n) otherwise p(n) 84 -- p(n+1) = if (f n) != ∅ then (f n) otherwise p(n)
85 -- 85 --
125 125
126 open import Data.Nat.Properties 126 open import Data.Nat.Properties
127 open import nat 127 open import nat
128 open _⊆_ 128 open _⊆_
129 129
130 p-monotonic1 : (P p : HOD ) (C : CountableModel ) → {n : Nat} → (* (find-p P C n (& p))) ⊆ (* (find-p P C (Suc n) (& p))) 130 p-monotonic1 : (P p : HOD ) (C : CountableModel ) → {n : Nat} → (* (find-p P C (Suc n) (& p))) ⊆ (* (find-p P C n (& p)))
131 p-monotonic1 P p C {n} with is-o∅ (& (PGHOD n P C (find-p P C n (& p)))) 131 p-monotonic1 P p C {n} with is-o∅ (& (PGHOD n P C (find-p P C n (& p))))
132 ... | yes y = refl-⊆ 132 ... | yes y = refl-⊆
133 ... | no not = record { incl = λ {x} lt → proj2 (proj2 fmin∈PGHOD) (& x) lt } where 133 ... | no not = record { incl = λ {x} lt → proj2 (proj2 fmin∈PGHOD) (& x) lt } where
134 fmin : HOD 134 fmin : HOD
135 fmin = ODC.minimal O (PGHOD n P C (find-p P C n (& p))) (λ eq → not (=od∅→≡o∅ eq)) 135 fmin = ODC.minimal O (PGHOD n P C (find-p P C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
136 fmin∈PGHOD : PGHOD n P C (find-p P C n (& p)) ∋ fmin 136 fmin∈PGHOD : PGHOD n P C (find-p P C n (& p)) ∋ fmin
137 fmin∈PGHOD = ODC.x∋minimal O (PGHOD n P C (find-p P C n (& p))) (λ eq → not (=od∅→≡o∅ eq)) 137 fmin∈PGHOD = ODC.x∋minimal O (PGHOD n P C (find-p P C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
138 138
139 p-monotonic : (P p : HOD ) (C : CountableModel ) → {n m : Nat} → n ≤ m → (* (find-p P C n (& p))) ⊆ (* (find-p P C m (& p))) 139 p-monotonic : (P p : HOD ) (C : CountableModel ) → {n m : Nat} → n ≤ m → (* (find-p P C m (& p))) ⊆ (* (find-p P C n (& p)))
140 p-monotonic P p C {Zero} {Zero} n≤m = refl-⊆ 140 p-monotonic P p C {Zero} {Zero} n≤m = refl-⊆
141 p-monotonic P p C {Zero} {Suc m} z≤n = trans-⊆ (p-monotonic P p C {Zero} {m} z≤n ) (p-monotonic1 P p C {m} ) 141 p-monotonic P p C {Zero} {Suc m} z≤n = trans-⊆ (p-monotonic1 P p C {m} ) (p-monotonic P p C {Zero} {m} z≤n )
142 p-monotonic P p C {Suc n} {Suc m} (s≤s n≤m) with <-cmp n m 142 p-monotonic P p C {Suc n} {Suc m} (s≤s n≤m) with <-cmp n m
143 ... | tri< a ¬b ¬c = trans-⊆ (p-monotonic P p C {Suc n} {m} a) (p-monotonic1 P p C {m} ) 143 ... | tri< a ¬b ¬c = trans-⊆ (p-monotonic1 P p C {m}) (p-monotonic P p C {Suc n} {m} a)
144 ... | tri≈ ¬a refl ¬c = refl-⊆ 144 ... | tri≈ ¬a refl ¬c = refl-⊆
145 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c ) 145 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c )
146 146
147 P-GenericFilter : (P p0 : HOD ) → Power P ∋ p0 → (C : CountableModel ) → GenericFilter P 147 P-GenericFilter : (P p0 : HOD ) → Power P ∋ p0 → (C : CountableModel ) → GenericFilter P
148 P-GenericFilter P p0 Pp0 C = record { 148 P-GenericFilter P p0 Pp0 C = record {
157 f1 {p} {q} q⊆P PD∋p p⊆q = record { gr = gr PD∋p ; pn<gr = f04 ; x∈PP = power← _ _ (incl q⊆P) } where 157 f1 {p} {q} q⊆P PD∋p p⊆q = record { gr = gr PD∋p ; pn<gr = f04 ; x∈PP = power← _ _ (incl q⊆P) } where
158 f04 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y 158 f04 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y
159 f04 y lt1 = subst₂ (λ j k → odef j k ) (sym *iso) &iso (incl p⊆q (subst₂ (λ j k → odef k j ) (sym &iso) *iso ( pn<gr PD∋p y lt1 ))) 159 f04 y lt1 = subst₂ (λ j k → odef j k ) (sym *iso) &iso (incl p⊆q (subst₂ (λ j k → odef k j ) (sym &iso) *iso ( pn<gr PD∋p y lt1 )))
160 -- odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y 160 -- odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y
161 f2 : {p q : HOD} → PDHOD P p0 C ∋ p → PDHOD P p0 C ∋ q → PDHOD P p0 C ∋ (p ∩ q) 161 f2 : {p q : HOD} → PDHOD P p0 C ∋ p → PDHOD P p0 C ∋ q → PDHOD P p0 C ∋ (p ∩ q)
162 f2 {p} {q} PD∋p PD∋q with <-cmp (gr PD∋p) (gr PD∋q) 162 f2 {p} {q} PD∋p PD∋q with <-cmp (gr PD∋q) (gr PD∋p)
163 ... | tri< a ¬b ¬c = record { gr = gr PD∋p ; pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f3 y lt); x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q) } where 163 ... | tri< a ¬b ¬c = record { gr = gr PD∋p ; pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f3 y lt); x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q) } where
164 f3 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (p ∩ q) y 164 f3 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (p ∩ q) y
165 f3 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y (f5 lt)) ⟫ where 165 f3 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y (f5 lt)) ⟫ where
166 f5 : odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (find-p P C (gr PD∋q) (& p0))) y 166 f5 : odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (find-p P C (gr PD∋q) (& p0))) y
167 f5 lt = subst (λ k → odef (* (find-p P C (gr PD∋q) (& p0))) k ) &iso ( incl (p-monotonic P p0 C {gr PD∋p} {gr PD∋q} (<to≤ a)) 167 f5 lt = subst (λ k → odef (* (find-p P C (gr PD∋q) (& p0))) k ) &iso ( incl (p-monotonic P p0 C {gr PD∋q} {gr PD∋p} (<to≤ a))
168 (subst (λ k → odef (* (find-p P C (gr PD∋p) (& p0))) k ) (sym &iso) lt) ) 168 (subst (λ k → odef (* (find-p P C (gr PD∋p) (& p0))) k ) (sym &iso) lt) )
169 ... | tri≈ ¬a refl ¬c = record { gr = gr PD∋p ; pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f4 y lt); x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q) } where 169 ... | tri≈ ¬a refl ¬c = record { gr = gr PD∋p ; pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f4 y lt); x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q) } where
170 f4 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (p ∩ q) y 170 f4 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (p ∩ q) y
171 f4 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫ 171 f4 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫
172 ... | tri> ¬a ¬b c = record { gr = gr PD∋q ; pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f3 y lt) ; x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q) } where 172 ... | tri> ¬a ¬b c = record { gr = gr PD∋q ; pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f3 y lt) ; x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q) } where
173 f3 : (y : Ordinal) → odef (* (find-p P C (gr PD∋q) (& p0))) y → odef (p ∩ q) y 173 f3 : (y : Ordinal) → odef (* (find-p P C (gr PD∋q) (& p0))) y → odef (p ∩ q) y
174 f3 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y (f5 lt)) , subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫ where 174 f3 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y (f5 lt)) , subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫ where
175 f5 : odef (* (find-p P C (gr PD∋q) (& p0))) y → odef (* (find-p P C (gr PD∋p) (& p0))) y 175 f5 : odef (* (find-p P C (gr PD∋q) (& p0))) y → odef (* (find-p P C (gr PD∋p) (& p0))) y
176 f5 lt = subst (λ k → odef (* (find-p P C (gr PD∋p) (& p0))) k ) &iso ( incl (p-monotonic P p0 C {gr PD∋q} {gr PD∋p} (<to≤ c)) 176 f5 lt = subst (λ k → odef (* (find-p P C (gr PD∋p) (& p0))) k ) &iso ( incl (p-monotonic P p0 C {gr PD∋p} {gr PD∋q} (<to≤ c))
177 (subst (λ k → odef (* (find-p P C (gr PD∋q) (& p0))) k ) (sym &iso) lt) ) 177 (subst (λ k → odef (* (find-p P C (gr PD∋q) (& p0))) k ) (sym &iso) lt) )
178 fdense : (D : Dense P ) → ¬ (filter.Dense.dense D ∩ PDHOD P p0 C) ≡ od∅ 178 fdense : (D : Dense P ) → ¬ (filter.Dense.dense D ∩ PDHOD P p0 C) ≡ od∅
179 fdense D eq0 = ⊥-elim ( ∅< {Dense.dense D ∩ PDHOD P p0 C} fd01 (≡od∅→=od∅ eq0 )) where 179 fdense D eq0 = ⊥-elim ( ∅< {Dense.dense D ∩ PDHOD P p0 C} fd01 (≡od∅→=od∅ eq0 )) where
180 open Dense 180 open Dense
181 p0⊆P : p0 ⊆ P 181 p0⊆P : p0 ⊆ P
189 fd02 : dense D ∋ dense-f D p0⊆P 189 fd02 : dense D ∋ dense-f D p0⊆P
190 fd02 = dense-d D p0⊆P 190 fd02 = dense-d D p0⊆P
191 fd04 : dense-f D p0⊆P ⊆ P 191 fd04 : dense-f D p0⊆P ⊆ P
192 fd04 = ODC.power→⊆ O _ _ ( incl PP∋D fd02 ) 192 fd04 = ODC.power→⊆ O _ _ ( incl PP∋D fd02 )
193 fd03 : PDHOD P p0 C ∋ dense-f D p0⊆P 193 fd03 : PDHOD P p0 C ∋ dense-f D p0⊆P
194 fd03 = f1 {p0} {dense-f D p0⊆P} fd04 fd00 ( dense-p D (ODC.power→⊆ O _ _ Pp0 ) ) 194 fd03 = {!!}
195 -- f1 {p0} {dense-f D p0⊆P} fd04 fd00 ( dense-p D (ODC.power→⊆ O _ _ Pp0 ) )
195 fd01 : (dense D ∩ PDHOD P p0 C) ∋ fd 196 fd01 : (dense D ∩ PDHOD P p0 C) ∋ fd
196 fd01 = ⟪ fd02 , fd03 ⟫ 197 fd01 = ⟪ fd02 , fd03 ⟫
197 198
198 open GenericFilter 199 open GenericFilter
199 open Filter 200 open Filter
244 D-Dense = record { 245 D-Dense = record {
245 dense = D 246 dense = D
246 ; d⊆P = record { incl = λ {x} lt → proj1 lt } 247 ; d⊆P = record { incl = λ {x} lt → proj1 lt }
247 ; dense-f = df 248 ; dense-f = df
248 ; dense-d = df-d 249 ; dense-d = df-d
249 ; dense-p = df-p 250 ; dense-p = {!!}
250 } 251 }
251 D∩G=∅ : ( D ∩ G ) =h= od∅ 252 D∩G=∅ : ( D ∩ G ) =h= od∅
252 D∩G=∅ = ≡od∅→=od∅ ([a-b]∩b=0 {Power P} {G}) 253 D∩G=∅ = ≡od∅→=od∅ ([a-b]∩b=0 {Power P} {G})
253 D∩G≠∅ : ¬ (( D ∩ G ) =h= od∅ ) 254 D∩G≠∅ : ¬ (( D ∩ G ) =h= od∅ )
254 D∩G≠∅ eq = generic (P-GenericFilter P p PP∋p C) D-Dense ( ==→o≡ eq ) 255 D∩G≠∅ eq = generic (P-GenericFilter P p PP∋p C) D-Dense ( ==→o≡ eq )
262 263
263 lemma725-1 : (p : HOD) → (PP∋p : p ⊆ HODω2 ) → Incompatible HODω2 p PP∋p 264 lemma725-1 : (p : HOD) → (PP∋p : p ⊆ HODω2 ) → Incompatible HODω2 p PP∋p
264 lemma725-1 = {!!} 265 lemma725-1 = {!!}
265 266
266 lemma726 : (C : CountableModel ) 267 lemma726 : (C : CountableModel )
267 → Union ( Replace' (Power HODω2) (λ p lt → filter ( genf ( P-GenericFilter HODω2 p lt C )))) =h= ω→2 -- HODω2 ∋ p 268 → Union ( Replace' (Power (ω→2 ＼ HODω2)) (λ p lt → filter ( genf ( P-GenericFilter (ω→2 ＼ HODω2) p lt C )))) =h= ω→2 -- HODω2 ∋ p
268 lemma726 = {!!} 269 lemma726 = {!!}
269 270
270 -- 271 --
271 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > } 272 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
272 -- 273 --