Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1239:5223f0b40d91
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 12 Mar 2023 11:58:55 +0900 |
| parents | 01fe64d3a17a |
| children | fbe072447243 |
| files | src/Tychonoff.agda src/filter.agda src/generic-filter.agda |
| diffstat | 3 files changed, 34 insertions(+), 92 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Tychonoff.agda Thu Mar 09 12:31:32 2023 +0900 +++ b/src/Tychonoff.agda Sun Mar 12 11:58:55 2023 +0900 @@ -172,7 +172,7 @@ fp00 b _ b<X (g∩ {y} {z} sy sz ) = g∩ (fp00 _ _ b<X sy) (fp00 _ _ b<X sz) -- -- then we have maximum ultra filter ( Zorn lemma ) - -- to debug this file, commet out to include maaximum filter + -- to debug this file, commet out the maximum filter and open import -- otherwise the check requires a minute -- maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
--- a/src/filter.agda Thu Mar 09 12:31:32 2023 +0900 +++ b/src/filter.agda Sun Mar 12 11:58:55 2023 +0900 @@ -151,14 +151,6 @@ lemma : (p : HOD) → p ⊆ P → filter F ∋ (p ∪ (P ＼ p)) lemma p p⊆P = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 {p} p⊆P)) f∋P -record Dense {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where - field - dense : HOD - d⊆P : dense ⊆ L - dense-f : {p : HOD} → L ∋ p → HOD - dense-d : { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt - dense-p : { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p - record Ideal {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where field ideal : HOD @@ -176,11 +168,6 @@ open import Relation.Binary.Definitions -record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (suc n) where - field - genf : Filter {L} {P} LP - generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ ) - record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) (F : Filter {L} {P} LP) : Set (suc n) where field mf : Filter {L} {P} LP
--- a/src/generic-filter.agda Thu Mar 09 12:31:32 2023 +0900 +++ b/src/generic-filter.agda Sun Mar 12 11:58:55 2023 +0900 @@ -74,15 +74,15 @@ ---- -- a(n) ∈ M --- ∃ q ∈ L ⊆ Power P → q ∈ a(n) ∧ q ⊆ p(n) +-- ∃ q ∈ L ⊆ Power P → q ∈ a(n) ∧ p(n) ⊆ q -- PGHOD : (i : Nat) (L : HOD) (C : CountableModel ) → (p : Ordinal) → HOD PGHOD i L C p = record { od = record { def = λ x → - odef L x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* x) y → odef (* p) y ) } + odef L x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* p) y → odef (* x) y ) } ; odmax = odmax L ; <odmax = λ {y} lt → <odmax L (proj1 lt) } --- --- p(n+1) = if ({q | q ∈ a(n) ∧ q ⊆ p(n))} != ∅ then q otherwise p(n) +-- p(n+1) = if ({q | q ∈ a(n) ∧ p(n) ⊆ q)} != ∅ then q otherwise p(n) -- find-p : (L : HOD ) (C : CountableModel ) (i : Nat) → (x : Ordinal) → Ordinal find-p L C Zero x = x @@ -91,12 +91,12 @@ ... | no not = & (ODC.minimal O ( PGHOD i L C (find-p L C i x)) (λ eq → not (=od∅→≡o∅ eq))) -- axiom of choice --- --- G = { r ∈ L ⊆ Power P | ∃ n → p(n) ⊆ r } +-- G = { r ∈ L ⊆ Power P | ∃ n → r ⊆ p(n) } -- record PDN (L p : HOD ) (C : CountableModel ) (x : Ordinal) : Set n where field gr : Nat - pn<gr : (y : Ordinal) → odef (* (find-p L C gr (& p))) y → odef (* x) y + pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p L C gr (& p))) y x∈PP : odef L x open PDN @@ -130,7 +130,7 @@ p-monotonic1 : (L p : HOD ) (C : CountableModel ) → {n : Nat} → (* (find-p L C (Suc n) (& p))) ⊆ (* (find-p L C n (& p))) p-monotonic1 L p C {n} {x} with is-o∅ (& (PGHOD n L C (find-p L C n (& p)))) ... | yes y = refl-⊆ {* (find-p L C n (& p))} -... | no not = λ lt → proj2 (proj2 fmin∈PGHOD) _ lt where +... | no not = ? where -- λ lt → proj2 (proj2 fmin∈PGHOD) _ ? where fmin : HOD fmin = ODC.minimal O (PGHOD n L C (find-p L C n (& p))) (λ eq → not (=od∅→≡o∅ eq)) fmin∈PGHOD : PGHOD n L C (find-p L C n (& p)) ∋ fmin @@ -144,85 +144,40 @@ ... | tri≈ ¬a refl ¬c = λ x → x ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c ) +record Dense {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where + field + dense : HOD + d⊆P : dense ⊆ L + dense-f : {p : HOD} → L ∋ p → HOD + dense-d : { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt + dense-p : { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p + +record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (suc n) where + field + genf : Filter {L} {P} LP + generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Replace (Filter.filter genf) (λ x → P ＼ x )) ≡ od∅ ) + rgen : HOD + rgen = Replace (Filter.filter genf) (λ x → P ＼ x ) + P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0 → (C : CountableModel ) → GenericFilter {L} {P} LP ( ctl-M C ) P-GenericFilter P L p0 L⊆PP Lp0 C = record { - genf = record { filter = PDHOD L p0 C ; f⊆L = f⊆PL ; filter1 = λ L∋q PD∋p p⊆q → f1 L∋q PD∋p p⊆q ; filter2 = f2 } - ; generic = fdense + genf = record { filter = Replace (PDHOD L p0 C) (λ x → P ＼ x) ; f⊆L = ? ; filter1 = ? ; filter2 = ? } + ; generic = ? } where f⊆PL : PDHOD L p0 C ⊆ L f⊆PL lt = x∈PP lt f1 : {p q : HOD} → L ∋ q → PDHOD L p0 C ∋ p → p ⊆ q → PDHOD L p0 C ∋ q - f1 {p} {q} L∋q PD∋p p⊆q = record { gr = gr PD∋p ; pn<gr = f04 ; x∈PP = L∋q } where - f04 : (y : Ordinal) → odef (* (find-p L C (gr PD∋p) (& p0))) y → odef (* (& q)) y - f04 y lt1 = subst₂ (λ j k → odef j k ) (sym *iso) &iso (p⊆q (subst₂ (λ j k → odef k j ) (sym &iso) *iso ( pn<gr PD∋p y lt1 ))) - -- odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y - f2 : {p q : HOD} → PDHOD L p0 C ∋ p → PDHOD L p0 C ∋ q → L ∋ (p ∩ q) → PDHOD L p0 C ∋ (p ∩ q) + f1 {p} {q} L∋q PD∋p p⊆q = ? + f2 : {p q : HOD} → ? ∋ p → ? ∋ q → L ∋ (p ∩ q) → ? ∋ (p ∩ q) f2 {p} {q} PD∋p PD∋q L∋pq with <-cmp (gr PD∋q) (gr PD∋p) - ... | 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 = L∋pq } where - f3 : (y : Ordinal) → odef (* (find-p L C (gr PD∋p) (& p0))) y → odef (p ∩ q) y - 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 - f5 : odef (* (find-p L C (gr PD∋p) (& p0))) y → odef (* (find-p L C (gr PD∋q) (& p0))) y - f5 lt = subst (λ k → odef (* (find-p L C (gr PD∋q) (& p0))) k ) &iso ( (p-monotonic L p0 C {gr PD∋q} {gr PD∋p} (<to≤ a)) - (subst (λ k → odef (* (find-p L C (gr PD∋p) (& p0))) k ) (sym &iso) lt) ) - ... | 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 = L∋pq } where - f4 : (y : Ordinal) → odef (* (find-p L C (gr PD∋p) (& p0))) y → odef (p ∩ q) y - 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) ⟫ - ... | 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 = L∋pq } where - f3 : (y : Ordinal) → odef (* (find-p L C (gr PD∋q) (& p0))) y → odef (p ∩ q) y - 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 - f5 : odef (* (find-p L C (gr PD∋q) (& p0))) y → odef (* (find-p L C (gr PD∋p) (& p0))) y - f5 lt = subst (λ k → odef (* (find-p L C (gr PD∋p) (& p0))) k ) &iso ( (p-monotonic L p0 C {gr PD∋p} {gr PD∋q} (<to≤ c)) - (subst (λ k → odef (* (find-p L C (gr PD∋q) (& p0))) k ) (sym &iso) lt) ) - fdense : (D : Dense L⊆PP ) → (ctl-M C ) ∋ Dense.dense D → ¬ (filter.Dense.dense D ∩ PDHOD L p0 C) ≡ od∅ - fdense D MD eq0 = ⊥-elim ( ∅< {Dense.dense D ∩ PDHOD L p0 C} fd01 (≡od∅→=od∅ eq0 )) where + ... | tri< a ¬b ¬c = ? + ... | tri≈ ¬a eq ¬c = ? + ... | tri> ¬a ¬b c = ? + gf : HOD + gf = Replace (Replace (PDHOD L p0 C) (λ x → P ＼ x)) (_＼_ P) + fdense : (D : Dense {L} {P} L⊆PP ) → (ctl-M C ) ∋ Dense.dense D → ¬ (Dense.dense D ∩ gf ) ≡ od∅ + fdense D MD eq0 = ? where open Dense - fd09 : (i : Nat ) → odef L (find-p L C i (& p0)) - fd09 Zero = Lp0 - fd09 (Suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) ) - ... | yes _ = fd09 i - ... | no not = fd17 where - fd19 = ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq)) - fd18 : PGHOD i L C (find-p L C i (& p0)) ∋ fd19 - fd18 = ODC.x∋minimal O (PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq)) - fd17 : odef L ( & (ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))) ) - fd17 = proj1 fd18 - an : Nat - an = ctl← C (& (dense D)) MD - pn : Ordinal - pn = find-p L C an (& p0) - pn+1 : Ordinal - pn+1 = find-p L C (Suc an) (& p0) - d=an : dense D ≡ * (ctl→ C an) - d=an = begin dense D ≡⟨ sym *iso ⟩ - * ( & (dense D)) ≡⟨ cong (*) (sym (ctl-iso→ C MD )) ⟩ - * (ctl→ C an) ∎ where open ≡-Reasoning - fd07 : odef (dense D) pn+1 - fd07 with is-o∅ ( & ( PGHOD an L C (find-p L C an (& p0))) ) - ... | yes y = ⊥-elim ( ¬x<0 ( _==_.eq→ fd10 ⟪ fd13 , ⟪ fd14 , fd15 ⟫ ⟫ ) ) where - fd12 : L ∋ * (find-p L C an (& p0)) - fd12 = subst (λ k → odef L k) (sym &iso) (fd09 an ) - fd11 : Ordinal - fd11 = & ( dense-f D fd12 ) - fd13 : L ∋ ( dense-f D fd12 ) - fd13 = (d⊆P D) ( dense-d D fd12 ) - fd14 : (* (ctl→ C an)) ∋ ( dense-f D fd12 ) - fd14 = subst (λ k → odef k (& ( dense-f D fd12 ) )) d=an ( dense-d D fd12 ) - fd15 : (y : Ordinal) → odef (* (& (dense-f D fd12))) y → odef (* (find-p L C an (& p0))) y - fd15 y lt = subst (λ k → odef (* (find-p L C an (& p0))) k ) &iso ( (dense-p D fd12 ) fd16 ) where - fd16 : odef (dense-f D fd12) (& ( * y)) - fd16 = subst₂ (λ j k → odef j k ) (*iso) (sym &iso) lt - fd10 : PGHOD an L C (find-p L C an (& p0)) =h= od∅ - fd10 = ≡o∅→=od∅ y - ... | no not = fd27 where - fd29 = ODC.minimal O ( PGHOD an L C (find-p L C an (& p0))) (λ eq → not (=od∅→≡o∅ eq)) - fd28 : PGHOD an L C (find-p L C an (& p0)) ∋ fd29 - fd28 = ODC.x∋minimal O (PGHOD an L C (find-p L C an (& p0))) (λ eq → not (=od∅→≡o∅ eq)) - fd27 : odef (dense D) (& fd29) - fd27 = subst (λ k → odef k (& fd29)) (sym d=an) (proj1 (proj2 fd28)) - fd03 : odef (PDHOD L p0 C) pn+1 - fd03 = record { gr = Suc an ; pn<gr = λ y lt → lt ; x∈PP = fd09 (Suc an)} - fd01 : (dense D ∩ PDHOD L p0 C) ∋ (* pn+1) - fd01 = ⟪ subst (λ k → odef (dense D) k ) (sym &iso) fd07 , subst (λ k → odef (PDHOD L p0 C) k) (sym &iso) fd03 ⟫ open GenericFilter open Filter @@ -236,7 +191,7 @@ lemma232 : (P L p : HOD ) (C : CountableModel ) → (LP : L ⊆ Power P ) → (Lp0 : L ∋ p ) → ( {q : HOD} → (Lq : L ∋ q ) → NonAtomic L q Lq ) - → ¬ ( (ctl-M C) ∋ filter ( genf ( P-GenericFilter P L p LP Lp0 C )) ) + → ¬ ( (ctl-M C) ∋ rgen ( P-GenericFilter P L p LP Lp0 C )) lemma232 P L p C LP Lp0 NA MG = {!!} where D : HOD -- P - G D = ?