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

changeset 1301:9e26c9abfafb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix PFOD
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 05 Jun 2023 11:33:27 +0900
parents 47d3cc596d68
children c97660e19535
files src/ODUtil.agda src/PFOD.agda
diffstat 2 files changed, 73 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/src/ODUtil.agda	Sun Jun 04 16:58:39 2023 +0900
+++ b/src/ODUtil.agda	Mon Jun 05 11:33:27 2023 +0900
@@ -179,18 +179,24 @@
           (* x , * x ) ∎ ) &iso uy ) ⟩  -- (* x , * x ) ∋ * y
         y ∎ ) x<y)  where open ≡-Reasoning
 
-ω-prev-eq : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → x ≡ y
+ω-prev-eq : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → y ≡ x
 ω-prev-eq {x} {y} eq with trio< x y
 ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a)
-ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b
+ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = (sym b)
 ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)
 
+ω-inject : {x y : HOD} →  Union ( y , ( y ,  y)) ≡ Union ( x , ( x ,  x)) → y ≡ x
+ω-inject {x} {y} eq = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ( ω-prev-eq (cong (&) (subst₂ (λ j k →  Union (j , (j , j)) ≡ Union (k , (k , k))) (sym *iso) (sym *iso) eq ))))
+
 ω-∈s : (x : HOD) →  Union ( x , (x , x)) ∋ x
 ω-∈s x = record { owner = & ( x , x ) ; ao = case2 refl  ; ox = subst₂ (λ j k → odef j k ) (sym *iso) refl (case2 refl) }
 
 ωs≠0 : (x : HOD) →  ¬ ( Union ( x , (x , x)) ≡ od∅ )
 ωs≠0 y eq =  ⊥-elim ( ¬x<0 (subst (λ k → & y  o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) )
 
+ωs0 : o∅ ≡ & (nat→ω 0)
+ωs0 = trans (sym ord-od∅) (cong (&) refl ) 
+
 nat→ω-iso : {i : HOD} → (lt : Omega ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
 nat→ω-iso {i} = ε-induction {λ i →  (lt : Omega ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
      ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : Omega ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
@@ -217,8 +223,8 @@
                lemma3 iφ iφ refl = HE.refl
                lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) )))
                lemma3 (isuc {y} ltd)  iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) )))
-               lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
-               ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (ω-prev-eq eq)) t
+               lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (eq))
+               ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (ω-prev-eq (sym eq))) t
                lemma2 : {x y : Ordinal} → (ltd : Omega-d x ) (ltd1 : Omega-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
                lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq)  where
                    lemma6 : {x y : Ordinal} → {ltd : Omega-d x } {ltd1 : Omega-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1
@@ -234,12 +240,18 @@
 ω→nat-iso0 (Suc i) (isuc {x} ltd) eq = cong Suc ( ω→nat-iso0 i ltd (lemma1 eq) ) where
        lemma1 :  * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i
        lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k)
-            ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym
-                (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq ))))))
+            (sym ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym
+                (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq )))))))
 
 ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
 ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) *iso
 
+nat→ω-inject : {i j : Nat} → nat→ω i ≡  nat→ω j → i ≡ j
+nat→ω-inject {Zero} {Zero} eq = refl
+nat→ω-inject {Zero} {Suc j} eq = ⊥-elim ( ¬0=ux (trans (trans (sym ord-od∅) (cong (&) eq)) refl ))
+nat→ω-inject {Suc i} {Zero} eq = ⊥-elim ( ¬0=ux (trans (trans (sym ord-od∅) (cong (&) (sym eq))) refl ))
+nat→ω-inject {Suc i} {Suc j} eq = cong Suc (nat→ω-inject {i} {j} ( ω-inject (eq) ))
+
 Repl⊆ : {A B : HOD} (A⊆B : A ⊆ B) → { ψa : ( x : HOD) → A ∋ x → HOD } { ψb : ( x : HOD) → B ∋ x → HOD }
    →  {Ca : HOD} → {rca : RXCod A Ca ψa }
    →  {Cb : HOD} → {rcb : RXCod B Cb ψb }
--- a/src/PFOD.agda	Sun Jun 04 16:58:39 2023 +0900
+++ b/src/PFOD.agda	Mon Jun 05 11:33:27 2023 +0900
@@ -56,7 +56,9 @@
 data Hω2 :  (i : Nat) ( x : Ordinal  ) → Set n where
   hφ :  Hω2 0 o∅
   h0 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
-    Hω2 (Suc i) (& (Union ((nat→ω i , nat→ω i) ,  * x )))
+    Hω2 (Suc i) (& (Union (< nat→ω i , od∅ >  ,  * x )))
+  h1 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
+    Hω2 (Suc i) (& (Union (< nat→ω i , nat→ω 1 > ,  * x )))
   he : {i : Nat} {x : Ordinal  } → Hω2 i x  →
     Hω2 (Suc i) x
 
@@ -67,33 +69,60 @@
 
 open Hω2r
 
-hw⊆POmega :  {y : Ordinal} → Hω2r y → odef (Power Omega) y
-hw⊆POmega {y} r = odmax1 (Hω2r.count r) (Hω2r.hω2 r) where
-    odmax1 : {y : Ordinal} (i : Nat)  →  Hω2 i y → odef (Power Omega) y
+hw⊆POmega :  {x : Ordinal} → Hω2r x → odef (Power (Power Omega )) x
+hw⊆POmega {x} r = odmax1 (Hω2r.count r) (Hω2r.hω2 r) where
+    odmax1 : {y : Ordinal} (i : Nat)  →  Hω2 i y → odef (Power (Power Omega )) y
     odmax1 0 hφ z xz = ⊥-elim ( ¬x<0 (subst (λ k → odef k z) o∅≡od∅  xz ))
     odmax1 (Suc i) (h0 {_} {y} hw) = pf01 where
-        pf00 : odef ( Power Omega) y
+        pf00 : odef ( Power (Power Omega)) y
         pf00 = odmax1 i hw
-        pf01 : odef (Power Omega) (& (Union ((nat→ω i , nat→ω i ) , * y)))
+        pf01 : odef (Power (Power Omega)) (& (Union (< nat→ω i , nat→ω 0 > , * y)))
         pf01 z xz with subst (λ k → odef k z ) *iso xz
         ... | record { owner = owner ; ao = case1 refl ; ox = ox } = pf02 where
-             pf02 : Omega-d z
-             pf02 with subst (λ k → odef k z) *iso ox
+             pf02 : (w : Ordinal) → odef (* z) w → Omega-d w
+             pf02 w zw with subst (λ k → odef k z) *iso ox  
+             ... | case2 refl with subst (λ k → odef k w) *iso zw
+             ... | case1 refl = ω∋nat→ω {i}
+             ... | case2 refl = ω∋nat→ω {0}
+             pf02 w zw | case1 refl with subst (λ k → odef k w) *iso zw
+             ... | case1 refl = ω∋nat→ω {i}
+             ... | case2 refl = ω∋nat→ω {i} 
+        ... | record { owner = owner ; ao = case2 refl ; ox = ox } = pf02 where
+             pf03 : odef ( Power (Power Omega)) y
+             pf03 = odmax1 i hw
+             pf02 : (w : Ordinal) → odef (* z) w → Omega-d w
+             pf02 w zw = odmax1 i hw _ (subst (λ k → odef (* k) z) (&iso) ox)  _ zw
+    odmax1 (Suc i) (h1 {_} {y} hw) = pf01 where
+        pf00 : odef ( Power (Power Omega)) y
+        pf00 = odmax1 i hw
+        pf01 : odef (Power (Power Omega)) (& (Union (< nat→ω i , nat→ω 1 > , * y)))
+        pf01 z xz with subst (λ k → odef k z ) *iso xz
+        ... | record { owner = owner ; ao = case1 refl ; ox = ox } = pf02 where
+             pf02 : (w : Ordinal) → odef (* z) w → Omega-d w
+             pf02 w zw with subst (λ k → odef k z) *iso ox  
+             ... | case2 refl with subst (λ k → odef k w) *iso zw
+             ... | case1 refl = ω∋nat→ω {i}
+             ... | case2 refl = ω∋nat→ω {1}
+             pf02 w zw | case1 refl with subst (λ k → odef k w) *iso zw
              ... | case1 refl = ω∋nat→ω {i}
              ... | case2 refl = ω∋nat→ω {i}
-        ... | record { owner = owner ; ao = case2 refl ; ox = ox } = pf00 _ (subst (λ k → odef k z) *iso ox)
+        ... | record { owner = owner ; ao = case2 refl ; ox = ox } = pf02 where
+             pf03 : odef ( Power (Power Omega)) y
+             pf03 = odmax1 i hw
+             pf02 : (w : Ordinal) → odef (* z) w → Omega-d w
+             pf02 w zw = odmax1 i hw _ (subst (λ k → odef (* k) z) (&iso) ox)  _ zw
     odmax1 (Suc i) (he {_} {y} hw) = pf00 where
-        pf00 : odef ( Power Omega) y
+        pf00 : odef ( Power (Power Omega)) y
         pf00 = odmax1 i hw
 
 --
 -- Set of limited partial function of Omega
 --
 HODω2 :  HOD
-HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = & (Power Omega)
+HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = & (Power (Power Omega))
   ; <odmax = λ lt → odef< (hw⊆POmega  lt) } 
 
-HODω2⊆Omega : {x : HOD} → HODω2 ∋ x → x ⊆ Omega 
+HODω2⊆Omega : {x : HOD} → HODω2 ∋ x → x ⊆ Power  Omega 
 HODω2⊆Omega {x} hx {z} wz = hw⊆POmega hx _ (subst (λ k → odef k z) (sym *iso) wz)
 
 record HwStep : Set n where
@@ -102,23 +131,29 @@
      i : Nat
      isHw : Hω2 i x
 
-3→Hω2 : List Two → HOD
+3→Hω2 : List (Maybe Two) → HOD
 3→Hω2 t = * (HwStep.x (list→hod t))  where
-   list→hod : List Two → HwStep
+   list→hod : List (Maybe Two) → HwStep
    list→hod []  = record { x = o∅ ; i = 0 ; isHw = hφ }
-   list→hod (i0 ∷ t)  = record { x = & (Union ( (nat→ω (HwStep.i pf01) , nat→ω (HwStep.i pf01))  , * x )) 
+   list→hod (just i0 ∷ t)  = record { x = & (Union ( < nat→ω (HwStep.i pf01) , od∅ >  , * x )) 
             ; i = Suc (HwStep.i pf01) ; isHw = h0 (HwStep.isHw pf01) } where 
         pf01 : HwStep
         pf01 = list→hod t 
         x = HwStep.x pf01
-   list→hod (i1 ∷ t)  = list→hod t 
+   list→hod (just i1 ∷ t)  = record { x = & (Union ( < nat→ω (HwStep.i pf01) , nat→ω 1 >  , * x )) 
+            ; i = Suc (HwStep.i pf01) ; isHw = h1 (HwStep.isHw pf01) } where 
+        pf01 : HwStep
+        pf01 = list→hod t 
+        x = HwStep.x pf01
+   list→hod (nothing ∷ t)  = list→hod t 
 
-Hω2→3 : (x :  HOD) → HODω2 ∋ x → List Two 
+Hω2→3 : (x :  HOD) → HODω2 ∋ x → List (Maybe Two) 
 Hω2→3 x = lemma where
-   lemma : { y : Ordinal } →  Hω2r y → List Two
+   lemma : { y : Ordinal } →  Hω2r y → List (Maybe Two)
    lemma record { count = 0 ; hω2 = hφ } = []
-   lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = i0 ∷ lemma record { count = i ; hω2 =  hω3 }
-   lemma record { count = (Suc i) ; hω2 = (he hω3) } = i1 ∷ lemma record { count = i ; hω2 =  hω3 }
+   lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 =  hω3 }
+   lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i0 ∷ lemma record { count = i ; hω2 =  hω3 }
+   lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 =  hω3 }
 
 ω→2 : HOD
 ω→2 = Power Omega