Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1245:11049e3168ad
dense done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 14 Mar 2023 11:58:15 +0900 |
| parents | a7dfcbbd07ff |
| children | dd3debafba2d |
| files | src/generic-filter.agda |
| diffstat | 1 files changed, 76 insertions(+), 16 deletions(-) [+] |
line wrap: on
line diff
--- a/src/generic-filter.agda Tue Mar 14 09:50:23 2023 +0900 +++ b/src/generic-filter.agda Tue Mar 14 11:58:15 2023 +0900 @@ -161,7 +161,7 @@ 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 + dense-p : { p : HOD} → (lt : L ∋ p) → p ⊆ dense-f lt record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (Level.suc n) where field @@ -170,10 +170,8 @@ rgen : HOD rgen = Replace (Filter.filter genf) (λ x → P ＼ x ) --- ＼-⊆ - P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0 - → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )) -- L is Boolean Algebra + → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )) -- L is a Boolean Algebra → (UNI : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q )) → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P ＼ p))) → (C : CountableModel ) → GenericFilter {L} {P} LP ( ctl-M C ) @@ -291,25 +289,87 @@ gf21 : {z : Ordinal } → odef (* x) z → odef P z gf21 {z} lt = L⊆PP ( PDN.x∈PP pdx ) z lt fdense : (D : Dense {L} {P} L⊆PP ) → (ctl-M C ) ∋ Dense.dense D → ¬ (Dense.dense D ∩ (PDHOD L p0 C)) ≡ od∅ - fdense D MD eq0 = ? where + fdense D MD eq0 = ⊥-elim ( ∅< {Dense.dense D ∩ PDHOD L p0 C} fd01 (≡od∅→=od∅ eq0 )) where open Dense + fd09 : (i : ℕ ) → 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 : ℕ + 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 fd21 ) ) where + L∋pn : L ∋ * (find-p L C an (& p0)) + L∋pn = subst (λ k → odef L k) (sym &iso) (fd09 an ) + L∋df : L ∋ ( dense-f D L∋pn ) + L∋df = (d⊆P D) ( dense-d D L∋pn ) + pn∋df : (* (ctl→ C an)) ∋ ( dense-f D L∋pn ) + pn∋df = subst (λ k → odef k (& ( dense-f D L∋pn ) )) d=an ( dense-d D L∋pn ) + pn⊆df : (y : Ordinal) → odef (* (find-p L C an (& p0))) y → odef (* (& (dense-f D L∋pn))) y + pn⊆df y py = subst (λ k → odef k y ) (sym *iso) (dense-p D L∋pn py) + fd21 : odef (PGHOD an L C (find-p L C an (& p0)) ) (& (dense-f D L∋pn)) + fd21 = ⟪ L∋df , ⟪ pn∋df , pn⊆df ⟫ ⟫ + 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 -record NonAtomic (L a : HOD ) (L∋a : L ∋ a ) : Set (Level.suc (Level.suc n)) where +record NotCompatible (L p : HOD ) (L∋a : L ∋ p ) : Set (Level.suc (Level.suc n)) where field - b : HOD - 0<b : ¬ o∅ ≡ & b - b<a : b ⊆ a + q r : HOD + Lq : L ∋ q + Lr : L ∋ r + p⊆q : p ⊆ q + p⊆r : p ⊆ r + ¬compat : (s : HOD) → ¬ ( (q ⊆ s) ∧ (r ⊆ s) ) -lemma232 : (P L p : HOD ) (C : CountableModel ) - → (LP : L ⊆ Power P ) → (Lp0 : L ∋ p ) ( NEG : {p : HOD} → L ∋ p → L ∋ ( P ＼ p)) - → ( {q : HOD} → (Lq : L ∋ q ) → NonAtomic L q Lq ) - → ¬ ( (ctl-M C) ∋ rgen ( P-GenericFilter P L p LP Lp0 ? ? NEG C )) -lemma232 P L p C LP Lp0 NEG NA MG = {!!} where - D : HOD -- P - G - D = ? +lemma232 : (P L p0 : HOD ) → (LP : L ⊆ Power P) → (Lp0 : L ∋ p0 ) + → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )) -- L is a Boolean Algebra + → (UNI : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q )) + → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P ＼ p))) + → (C : CountableModel ) + → ( MP : ctl-M C ∋ P ) + → ( {p : HOD} → (Lp : L ∋ p ) → NotCompatible L p Lp ) + → ¬ ( ctl-M C ∋ rgen ( P-GenericFilter P L p0 LP Lp0 CAP UNI NEG C )) +lemma232 P L p0 LP Lp0 CAP UNI NEG C MP NC M∋gf = ¬gf∩D=0 record { eq→ = λ {x} gf∩D → ⊥-elim( proj2 (proj2 gf∩D) (proj1 gf∩D)) + ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where + gf = rgen ( P-GenericFilter P L p0 LP Lp0 CAP UNI NEG C ) + M = ctl-M C + D : HOD + D = L ＼ gf + M∋D : M ∋ D + M∋D = ? + ¬gf∩D=0 : ¬ ( (gf ∩ D) =h= od∅ ) + ¬gf∩D=0 = ? + gf∩D∋x : (gf ∩ D) ∋ ? + gf∩D∋x = ? -- -- P-Generic Filter defines a countable model D ⊂ C from P