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

changeset 453:e5f0ac638c01

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
P should be an order structure not Power Ser definition of dense is wrong
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 15 Mar 2022 14:09:20 +0900
parents 76aba34438f2
children 0d3d72dba75b
files src/generic-filter.agda
diffstat 1 files changed, 30 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Mon Mar 14 23:37:18 2022 +0900
+++ b/src/generic-filter.agda	Tue Mar 15 14:09:20 2022 +0900
@@ -54,15 +54,14 @@
 import OPair
 open OPair O
 
-record CountableModel (P : HOD) : Set (suc (suc n)) where
+record CountableModel : Set (suc (suc n)) where
    field
        ctl-M : Ordinal
        ctl→ : Nat → Ordinal
-       ctl← : (x : Ordinal )→  x o< ctl-M → Nat
-       ctl<M : (x : Nat) → ctl→ x o< ctl-M
-       ctl-iso→ : { x : Ordinal } → (lt : x o< ctl-M)  → ctl→ (ctl← x lt ) ≡ x 
+       ctl<M : (x : Nat) → odef (* ctl-M) (ctl→ x) 
+       ctl← : (x : Ordinal )→  odef (* ctl-M ) x → Nat
+       ctl-iso→ : { x : Ordinal } → (lt : odef (* ctl-M) x )  → ctl→ (ctl← x lt ) ≡ x 
        ctl-iso← : { x : Nat }  →  ctl← (ctl→ x ) (ctl<M x)  ≡ x
-       ctl-P∈M : Power P ∈ * ctl-M
 --
 -- almmost universe
 -- find-p contains ∃ x : Ordinal → x o< & M → ∀ r ∈ M → ∈ Ord x
@@ -76,7 +75,7 @@
 --   a(n) ∈ M
 --   ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q    
 --
-PGHOD :  (i : Nat) (P : HOD) (C : CountableModel P) → (p : Ordinal) → HOD
+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 ) }
    ; odmax = odmax (Power P)  ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) }  
@@ -84,7 +83,7 @@
 ---
 --   p(n+1) = if (f n) != ∅ then (f n) otherwise p(n)
 --  
-find-p :  (P : HOD ) (C : CountableModel P)  (i : Nat) → (x : Ordinal) → Ordinal
+find-p :  (P : HOD ) (C : CountableModel )  (i : Nat) → (x : Ordinal) → Ordinal
 find-p P C Zero x = x
 find-p P C (Suc i) x with is-o∅ ( & ( PGHOD i P C (find-p P C i x)) )
 ... | yes y  = find-p P C i x
@@ -93,7 +92,7 @@
 ---
 -- G = { r ∈ Power P | ∃ n → p(n) ⊆ r }
 --
-record PDN  (P p : HOD ) (C : CountableModel P)  (x : Ordinal) : Set n where
+record PDN  (P p : HOD ) (C : CountableModel )  (x : Ordinal) : Set n where
    field
        gr : Nat
        pn<gr : (y : Ordinal) → odef (* (find-p P C gr (& p))) y → odef (* x) y 
@@ -104,7 +103,7 @@
 ---
 -- G as a HOD
 --
-PDHOD :  (P p : HOD ) (C : CountableModel P ) → HOD
+PDHOD :  (P p : HOD ) (C : CountableModel  ) → HOD
 PDHOD P p C  = record { od = record { def = λ x →  PDN P p C x }
     ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt)  } 
 
@@ -128,7 +127,7 @@
 open import nat
 open _⊆_
 
-p-monotonic1 :  (P p : HOD ) (C : CountableModel P ) → {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 n (& p))) ⊆ (* (find-p P C (Suc 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
@@ -137,7 +136,7 @@
     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 P ) → {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 n (& p))) ⊆ (* (find-p P C m (& 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 {Suc n} {Suc m} (s≤s n≤m) with <-cmp n m
@@ -145,7 +144,7 @@
 ... | tri≈ ¬a refl ¬c = refl-⊆
 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c )
 
-P-GenericFilter : (P p0 : HOD ) → Power P ∋ p0 → (C : CountableModel P) → GenericFilter P
+P-GenericFilter : (P p0 : HOD ) → Power P ∋ p0 → (C : CountableModel ) → GenericFilter P
 P-GenericFilter P p0 Pp0 C = record {
       genf = record { filter = PDHOD P p0 C ; f⊆PL =  f⊆PL ; filter1 = f1 ; filter2 = f2 }
     ; generic = fdense
@@ -208,12 +207,12 @@
       p⊆r :  p ⊆ r 
       incompatible : ∀ ( s : HOD ) → s ⊆ P → (¬ ( q ⊆ s  )) ∨ (¬ ( r ⊆ s ))
 
-lemma725 : (P p : HOD ) (C : CountableModel P) 
-    →  (pp0 : Power P ∋ p )
+lemma725 : (P p : HOD ) (C : CountableModel ) 
+    →  (PP∋p : Power P ∋ p )
     →  * (ctl-M C) ∋ (Power P ∩  * (ctl-M C))                -- M is a Model of ZF
-    →  * (ctl-M C) ∋ ( (Power P ∩  * (ctl-M C))  ＼ filter ( genf ( P-GenericFilter P p pp0 C)) )      -- M ∋ G and M is a Model of ZF 
+    →  * (ctl-M C) ∋ ( (Power P ∩  * (ctl-M C))  ＼ filter ( genf ( P-GenericFilter P p PP∋p C)) )      -- M ∋ G and M is a Model of ZF 
     →  ((p : HOD) → (PP∋p : p  ⊆ P ) → Incompatible P p PP∋p )
-    → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter P p pp0 C )))
+    → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter P p PP∋p C )))
 lemma725 P p C PP∋p M∋PM M∋D I M∋G = D∩G≠∅ D∩G=∅ where
     G = filter ( genf ( P-GenericFilter P p PP∋p C ))
     M = * (ctl-M C)
@@ -222,25 +221,25 @@
     p⊆P : p ⊆ P
     p⊆P =  ODC.power→⊆ O _ _ PP∋p
     df : {x : HOD} → x ⊆ P → HOD
-    df {x} PP∋x with Incompatible.incompatible (I x PP∋x) x PP∋x
-    ... | case1 q = Incompatible.q (I x PP∋x)
-    ... | case2 r = Incompatible.r (I x PP∋x)
-    df¬⊆ : {x : HOD} → (lt : x ⊆ P) → ¬ ( df lt  ⊆ x )
-    df¬⊆ {x} PP∋x with Incompatible.incompatible (I x PP∋x) x PP∋x
-    ... | case1 q = q
-    ... | case2 r = r
+    df {x} PP∋x with ODC.∋-p O G ( Incompatible.r (I x PP∋x) )
+    ... | yes y = Incompatible.q (I x PP∋x) 
+    ... | no n  = Incompatible.r (I x PP∋x) 
     df¬⊆P : {x : HOD} → (lt : x ⊆ P) → df lt  ⊆ P 
-    df¬⊆P {x} PP∋x with Incompatible.incompatible (I x PP∋x) x PP∋x
-    ... | case1 q = Incompatible.PP∋q (I x PP∋x)
-    ... | case2 r = Incompatible.PP∋r (I x PP∋x)
+    df¬⊆P {x} PP∋x with ODC.∋-p O G ( Incompatible.r (I x PP∋x) )
+    ... | yes _ = Incompatible.PP∋q (I x PP∋x)
+    ... | no _  = Incompatible.PP∋r (I x PP∋x)
     ¬G∋df : {x : HOD} → (lt : x ⊆ P) → ¬ G ∋ (df lt ) 
-    ¬G∋df {x} lt g = {!!}
+    ¬G∋df {x} lt with ODC.∋-p O G ( Incompatible.r (I x lt ) )
+    ... | no n = n
+    ... | yes y with Incompatible.incompatible (I x lt ) (Incompatible.q (I x lt )) (Incompatible.PP∋q  (I x lt ))
+    ... | case1 ¬q⊆pn = λ _ → ¬q⊆pn refl-⊆
+    ... | case2 ¬r⊆pn = {!!}
     df-d : {x : HOD} → (lt : x ⊆ P) → D ∋ df lt
     df-d {x} lt = ⟪  power← P _ (incl (df¬⊆P lt)) , ¬G∋df lt ⟫
     df-p : {x : HOD} → (lt : x ⊆ P) → x ⊆ df lt
-    df-p {x} lt with Incompatible.incompatible (I x lt) x lt
-    ... | case1 q = Incompatible.p⊆q (I x lt) 
-    ... | case2 r = Incompatible.p⊆r (I x lt) 
+    df-p {x} lt with ODC.∋-p O G ( Incompatible.r (I x lt) )
+    ... | yes _ = Incompatible.p⊆q (I x lt) 
+    ... | no _ = Incompatible.p⊆r (I x lt) 
     D-Dense : Dense P
     D-Dense = record {
            dense = D
@@ -264,7 +263,7 @@
 lemma725-1 :  (p : HOD) → (PP∋p : p  ⊆ HODω2 ) → Incompatible HODω2 p PP∋p
 lemma725-1 = {!!}
 
-lemma726 :  (C : CountableModel HODω2) 
+lemma726 :  (C : CountableModel ) 
     →  Union ( Replace' (Power HODω2) (λ p lt → filter ( genf ( P-GenericFilter HODω2 p lt C )))) =h= ω→2 -- HODω2 ∋ p
 lemma726 = {!!}