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

changeset 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 0d3d72dba75b
children 9207b0c3cfe9
files src/filter.agda src/generic-filter.agda
diffstat 2 files changed, 15 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/src/filter.agda	Tue Mar 15 15:46:39 2022 +0900
+++ b/src/filter.agda	Thu Mar 17 14:04:25 2022 +0900
@@ -126,7 +126,7 @@
        d⊆P :  dense ⊆ Power P 
        dense-f : {p : HOD} → p ⊆ P → HOD
        dense-d :  { p : HOD} → (lt : p ⊆ P) → dense ∋ dense-f lt
-       dense-p :  { p : HOD} → (lt : p ⊆ P) → p ⊆ (dense-f lt) 
+       dense-p :  { p : HOD} → (lt : p ⊆ P) → (dense-f lt) ⊆ p  
 
 record Ideal  ( L : HOD  ) : Set (suc n) where
    field
@@ -182,7 +182,7 @@
        d⊆P :  PL dense 
        dense-f : {p : L}  → PL (λ x → p ⊆ x ) → L 
        dense-d :  { p : L} → (lt : PL (λ x → p ⊆ x )) → dense ( dense-f lt  )
-       dense-p :  { p : L} → (lt : PL (λ x → p ⊆ x )) → p ⊆ (dense-f lt) 
+       dense-p :  { p : L} → (lt : PL (λ x → p ⊆ x )) → (dense-f lt) ⊆ p
 
 Dense-is-F : {L : HOD} → (f : Dense L ) → F-Dense HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
 Dense-is-F {L} f = record {
--- a/src/generic-filter.agda	Tue Mar 15 15:46:39 2022 +0900
+++ b/src/generic-filter.agda	Thu Mar 17 14:04:25 2022 +0900
@@ -73,11 +73,11 @@
 
 ----
 --   a(n) ∈ M
---   ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q    
+--   ∃ q ∈ Power P → q ∈ a(n) ∧ q ⊆ p(n)    
 --
 PGHOD :  (i : Nat) (P : HOD) (C : CountableModel ) → (p : Ordinal) → HOD
 PGHOD i P C p = record { od = record { def = λ x  →
-       odef (Power P) x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* p) y →  odef (* x) y ) }
+       odef (Power P) x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* x) y →  odef (* p) y ) }
    ; odmax = odmax (Power P)  ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) }  
 
 ---
@@ -127,7 +127,7 @@
 open import nat
 open _⊆_
 
-p-monotonic1 :  (P p : HOD ) (C : CountableModel  ) → {n : Nat} → (* (find-p P C n (& p))) ⊆ (* (find-p P C (Suc n) (& p)))
+p-monotonic1 :  (P p : HOD ) (C : CountableModel  ) → {n : Nat} → (* (find-p P C (Suc n) (& p))) ⊆ (* (find-p P C n (& p)))
 p-monotonic1 P p C {n} with is-o∅ (& (PGHOD n P C (find-p P C n (& p))))
 ... | yes y =   refl-⊆
 ... | no not = record { incl = λ {x} lt → proj2 (proj2 fmin∈PGHOD) (& x) lt  } where
@@ -136,11 +136,11 @@
     fmin∈PGHOD : PGHOD n P C (find-p P C n (& p)) ∋ fmin
     fmin∈PGHOD = ODC.x∋minimal O (PGHOD n P C (find-p P C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
 
-p-monotonic :  (P p : HOD ) (C : CountableModel  ) → {n m : Nat} → n ≤ m → (* (find-p P C n (& p))) ⊆ (* (find-p P C m (& p)))
+p-monotonic :  (P p : HOD ) (C : CountableModel  ) → {n m : Nat} → n ≤ m → (* (find-p P C m (& p))) ⊆ (* (find-p P C n (& p)))
 p-monotonic P p C {Zero} {Zero} n≤m = refl-⊆
-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} )  
+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 ) 
 p-monotonic P p C {Suc n} {Suc m} (s≤s n≤m) with <-cmp n m
-... | tri< a ¬b ¬c = trans-⊆ (p-monotonic P p C {Suc n} {m} a) (p-monotonic1 P p C {m} )  
+... | tri< a ¬b ¬c = trans-⊆ (p-monotonic1 P p C {m}) (p-monotonic P p C {Suc n} {m} a)   
 ... | tri≈ ¬a refl ¬c = refl-⊆
 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c )
 
@@ -159,12 +159,12 @@
            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 )))
                -- odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y
         f2 : {p q : HOD} → PDHOD P p0 C ∋ p → PDHOD P p0 C ∋ q → PDHOD P p0 C ∋ (p ∩ q)
-        f2 {p} {q} PD∋p PD∋q with <-cmp (gr PD∋p) (gr PD∋q)
+        f2 {p} {q} PD∋p PD∋q 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 = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q)   }  where
             f3 : (y : Ordinal) → odef (* (find-p P 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 P C (gr PD∋p) (& p0))) y → odef (* (find-p P C (gr PD∋q) (& p0))) y
-               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))
+               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))
                    (subst (λ k → odef (* (find-p P 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 = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q)   }  where
             f4 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (p ∩ q) y
@@ -173,7 +173,7 @@
             f3 : (y : Ordinal) → odef (* (find-p P 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 P C (gr PD∋q) (& p0))) y → odef (* (find-p P C (gr PD∋p) (& p0))) y
-               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))
+               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))
                    (subst (λ k → odef (* (find-p P C (gr PD∋q) (& p0))) k ) (sym &iso) lt) )
         fdense : (D : Dense P ) → ¬ (filter.Dense.dense D ∩ PDHOD P p0 C) ≡ od∅
         fdense D eq0  = ⊥-elim (  ∅< {Dense.dense D ∩ PDHOD P p0 C} fd01 (≡od∅→=od∅ eq0 )) where
@@ -191,7 +191,8 @@
            fd04 : dense-f D p0⊆P ⊆ P
            fd04 = ODC.power→⊆ O _ _ ( incl PP∋D fd02 )
            fd03 : PDHOD P p0 C  ∋ dense-f D p0⊆P
-           fd03 = f1 {p0} {dense-f D p0⊆P} fd04 fd00 ( dense-p D (ODC.power→⊆ O _ _ Pp0 ) )
+           fd03 = {!!}
+           -- f1 {p0} {dense-f D p0⊆P} fd04 fd00 ( dense-p D (ODC.power→⊆ O _ _ Pp0 ) )
            fd01 : (dense D ∩ PDHOD P p0 C) ∋ fd
            fd01 = ⟪ fd02 , fd03 ⟫ 
 
@@ -246,7 +247,7 @@
        ;   d⊆P = record { incl = λ {x} lt → proj1 lt }
        ;   dense-f = df
        ;   dense-d = df-d
-       ;   dense-p = df-p
+       ;   dense-p = {!!}
      }
     D∩G=∅ : ( D ∩ G ) =h= od∅ 
     D∩G=∅ = ≡od∅→=od∅ ([a-b]∩b=0 {Power P} {G})
@@ -264,7 +265,7 @@
 lemma725-1 = {!!}
 
 lemma726 :  (C : CountableModel ) 
-    →  Union ( Replace' (Power HODω2) (λ p lt → filter ( genf ( P-GenericFilter HODω2 p lt C )))) =h= ω→2 -- HODω2 ∋ p
+    →  Union ( Replace' (Power (ω→2 ＼ HODω2)) (λ p lt → filter ( genf ( P-GenericFilter (ω→2 ＼ HODω2) p lt C )))) =h= ω→2 -- HODω2 ∋ p
 lemma726 = {!!}
 
 --