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

changeset 628:0b5ff1c7032c

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 Mon, 20 Jun 2022 15:39:40 +0900
parents 35d8aca1a2b7
children 5b7b54fa4cf7
files src/zorn.agda
diffstat 1 files changed, 53 insertions(+), 76 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jun 20 13:47:06 2022 +0900
+++ b/src/zorn.agda	Mon Jun 20 15:39:40 2022 +0900
@@ -236,8 +236,6 @@
 record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
    field
       supf : Ordinal → HOD
-      chain-mono : {x y : Ordinal} → x o≤ y → y o≤ z →  supf x ⊆' supf y 
-      f-total : {x y : Ordinal} → x o≤ z → IsTotalOrderSet (supf x) 
    chain : HOD
    chain = supf z 
    field
@@ -250,9 +248,12 @@
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
 
+--      chain-mono : {x y : Ordinal} → x o≤ y → y o≤ z →  supf x ⊆' supf y 
+--      f-total : {x y : Ordinal} → x o≤ z → IsTotalOrderSet (supf x) 
+
 ZChainSupUnique : ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) ( a b : Ordinal )
-   → ( za : ZChain A x f a ) → (zb : ZChain A x f b ) → a o< b → i o≤ a → ZChain.supf za i ≡ ZChain.supf zb i
-ZChainSupUnique = ?
+   → ( za : ZChain A x f a ) → (zb : ZChain A x f b ) → {i : Ordinal } → a o< b → i o≤ a → ZChain.supf za i ≡ ZChain.supf zb i
+ZChainSupUnique = {!!}
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -326,12 +327,12 @@
      cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
 
      zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc : ZChain A (& s) f (& A) ) → SUP A  (ZChain.chain zc) 
-     zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc {& A} {& A} o≤-refl )   
+     zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) {!!}   
      A∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A (& s) (cf nmx)  (& A) ) 
         →  A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc )))
      A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal  (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )
      sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f  (& A) ) → SUP A (ZChain.chain zc)
-     sp0 f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain.f-total zc {& A} {& A} o≤-refl )   
+     sp0 f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) {!!}   
      zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P
      zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y)
 
@@ -366,20 +367,21 @@
                    ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
                    -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ?  (SUP.x<sup sp1 ? ) }
            z14 :  f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc))
-           z14 with ZChain.f-total zc {& A} {& A} o≤-refl (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
-           ... | tri< a ¬b ¬c = ⊥-elim z16 where
-               z16 : ⊥
-               z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
-               ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
-               ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
-           ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
-           ... | tri> ¬a ¬b c = ⊥-elim z17 where
-               z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) <  SUP.sup sp1)
-               z15  = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
-               z17 : ⊥
-               z17 with z15
-               ... | case1 eq = ¬b eq
-               ... | case2 lt = ¬a lt
+           z14 = {!!}
+           -- with ZChain.f-total zc {& A} {& A} o≤-refl (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
+           -- ... | tri< a ¬b ¬c = ⊥-elim z16 where
+           --     z16 : ⊥
+           --     z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
+           --     ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
+           --     ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
+           -- ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
+           -- ... | tri> ¬a ¬b c = ⊥-elim z17 where
+           --     z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) <  SUP.sup sp1)
+           --     z15  = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
+           --     z17 : ⊥
+           --     z17 with z15
+           --     ... | case1 eq = ¬b eq
+           --     ... | case2 lt = ¬a lt
 
      -- ZChain contradicts ¬ Maximal
      --
@@ -398,18 +400,18 @@
      -- create all ZChains under o< x
      --
 
-     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x → { y₁ : Ordinal} (ay : odef A y₁)
-         → ZChain A y₁ f y) → {y : Ordinal} (ay : odef A y) → ZChain A y f x
-     ind f mf x prev {y} ay with Oprev-p x
+     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
+         → ((z : Ordinal) → z o< x → ZChain A y f z) → ZChain A y f x
+     ind f mf {y} ay x prev with Oprev-p x
      ... | yes op = zc4 where
           --
           -- we have previous ordinal to use induction
           --
           px = Oprev.oprev op
           supf : Ordinal → HOD
-          supf = ZChain.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay)
+          supf = ZChain.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) )
           zc : ZChain A y f (Oprev.oprev op)
-          zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay 
+          zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
           zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
           zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
           px<x : px o< x
@@ -426,8 +428,7 @@
                      ; f-immediate =  subst (λ k →  {x₁ : Ordinal} {y₁ : Ordinal} → odef k x₁ → odef k y₁ →
                             ¬ (* x₁ < * y₁) ∧ (* y₁ < * (f x₁)) ) seq (ZChain.f-immediate zc) ; chain∋x  = subst (λ k → odef k y ) seq (ZChain.chain∋x  zc)
                              ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) →
-                                 HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) seq is-max 
-                     ; chain-mono = mono ; f-total = {!!} } where
+                                 HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) seq is-max } where
                 supf0 : Ordinal → HOD
                 supf0 z with trio< z x
                 ... | tri< a ¬b ¬c = supf z
@@ -443,30 +444,6 @@
                 ... | tri< a ¬b ¬c = refl
                 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
                 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
-                mono : {a b  : Ordinal}  → a o≤ b → b o< osuc x →
-                    supf0 a  ⊆' supf0 b 
-                mono {a} {b} a≤b b<ox with osuc-≡< a≤b
-                ... | case1 refl = λ x → x
-                ... | case2 a<b with osuc-≡< b<ox 
-                ... | case1 b=x = subst₂ (λ j k → j ⊆' k ) (seq<x a<x) nc00 ( ZChain.chain-mono zc a≤px <-osuc  ) where
-                     a<x : a o< x
-                     a<x with  osuc-≡< b<ox
-                     ... | case1 b=x = subst (λ k → a o< k ) b=x a<b
-                     ... | case2 b<x = ordtrans a<b b<x
-                     a≤px : a o≤  px
-                     a≤px = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) a<x
-                     nc00 : supf px  ≡ supf0 b
-                     nc00 with trio< b x
-                     ... | tri< a ¬b ¬c = ⊥-elim ( ¬b b=x )
-                     ... | tri≈ ¬a b ¬c = refl
-                     ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b=x )
-                ... | case2 b<x = subst₂ (λ j k → j ⊆' k ) (seq<x a<x ) (seq<x b<x )
-                            ( ZChain.chain-mono zc a≤b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) b<x ) )
-                   where
-                     a<x : a o< x
-                     a<x with  osuc-≡< b<ox
-                     ... | case1 b=x = subst (λ k → a o< k ) b=x a<b
-                     ... | case2 b<x = ordtrans a<b b<x
 
           zc4 : ZChain A y f x 
           zc4 with ODC.∋-p O A (* x)
@@ -489,7 +466,7 @@
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc) ax )
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  chain⊆A = {!!} ; f-next = {!!} 
-                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!}   ; supf = supf0 ; chain-mono = mono ; f-total = {!!} } where 
+                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!}   ; supf = supf0 } where
                 sup0 : SUP A (ZChain.chain zc) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
                         x21 :  {y : HOD} → ZChain.chain zc ∋ y → (y ≡ * x) ∨ (y < * x)
@@ -527,7 +504,7 @@
                         a<b : a < b
                         a<b = ptrans  (subst (λ k → a < k ) (sym *iso) a<sp ) ( subst₂ (λ j k → j < k ) refl *iso sp<b )
                 scmp : {a b : HOD} → odef schain (& a) → odef schain (& b) → Tri (a < b) (a ≡ b) (b < a )
-                scmp {a} {b} (case1 za) (case1 zb) = ZChain.f-total zc {px} {px} o≤-refl za zb
+                scmp {a} {b} (case1 za) (case1 zb) = {!!} -- ZChain.f-total zc {px} {px} o≤-refl za zb
                 scmp {a} {b} (case1 za) (case2 fb) = cmp za fb 
                 scmp  (case2 fa) (case1 zb) with  cmp zb fa
                 ... | tri< a ¬b ¬c = tri> ¬c (λ eq → ¬b (sym eq))  a
@@ -616,18 +593,17 @@
                 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
-     ... | no ¬ox = record { supf = supf0 ; chain-mono = u-mono ; f-total = u-total
-              ; chain⊆A = {!!} ; f-next = {!!} 
+     ... | no ¬ox = record { supf = supf0 ; chain⊆A = {!!} ; f-next = {!!} 
                      ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} }   where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
             field
                u : Ordinal
                u<x : u o< x
-               chain∋z : odef (ZChain.chain (prev u u<x {y} ay )) z
+               chain∋z : odef (ZChain.chain (prev u u<x  )) z
          Uz⊆A : {z : Ordinal} → UZFChain z → odef A z
-         Uz⊆A {z} u = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) {y} ay ) (UZFChain.chain∋z u)
+         Uz⊆A {z} u = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u)
          uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f (UZFChain.u u)
-         uzc {z} u =  prev (UZFChain.u u) (UZFChain.u<x u) {y} ay
+         uzc {z} u =  prev (UZFChain.u u) (UZFChain.u<x u) 
          Uz : HOD
          Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A
              ; <odmax = λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) }
@@ -636,10 +612,10 @@
          u-initial :  {z : Ordinal} → odef Uz z → * y ≤ * z 
          u-initial {z} u = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
          u-chain∋x :  odef Uz y
-         u-chain∋x = record { u = y ; u<x = {!!} ; chain∋z = ZChain.chain∋x (prev y {!!} ay ) }
+         u-chain∋x = record { u = y ; u<x = {!!} ; chain∋z = ZChain.chain∋x (prev y {!!} ) }
          supf0 : Ordinal → HOD
          supf0 z with trio< z x
-         ... | tri< a ¬b ¬c = ZChain.supf (prev z a {y} ay) z
+         ... | tri< a ¬b ¬c = ZChain.supf (prev z a ) z
          ... | tri≈ ¬a b ¬c = Uz 
          ... | tri> ¬a ¬b c = Uz
          seq : Uz ≡ supf0 x
@@ -647,9 +623,9 @@
          ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
          ... | tri≈ ¬a b ¬c = refl
          ... | tri> ¬a ¬b c = refl
-         seq<x : {b : Ordinal } → (b<x : b o< x ) →  ZChain.supf (prev b b<x {y} ay) b  ≡ supf0 b
+         seq<x : {b : Ordinal } → (b<x : b o< x ) →  ZChain.supf (prev b b<x ) b  ≡ supf0 b
          seq<x {b} b<x with trio< b x
-         ... | tri< a ¬b ¬c = cong (λ k → ZChain.supf (prev b k {y} ay) b) o<-irr --  b<x ≡ a
+         ... | tri< a ¬b ¬c = cong (λ k → ZChain.supf (prev b k ) b) o<-irr --  b<x ≡ a
          ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
          ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
          ord≤< : {x y z : Ordinal} → x o< z → z o≤ y → x o< y
@@ -659,29 +635,30 @@
          u-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w
          u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
          ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = um00 where -- ZChain.chain-mono (prev w ? ay) ? ? lt
-             um00 : odef  (ZChain.supf (prev z a ay) z) i → odef  (ZChain.supf (prev w a₁ ay) w) i 
+             um00 : odef  (ZChain.supf (prev z a ) z) i → odef  (ZChain.supf (prev w a₁ ) w) i 
              um00 = {!!}
-             um01 : odef  (ZChain.supf (prev z a ay) z) i → odef  (ZChain.supf (prev z {!!} ay) w) i 
-             um01 = ZChain.chain-mono (prev z a ay) {!!} {!!}
+             um01 : odef  (ZChain.supf (prev z a ) z) i → odef  (ZChain.supf (prev z {!!} ) w) i 
+             um01 = {!!} -- ZChain.chain-mono (prev z a ay) {!!} {!!}
          ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = λ lt → record { u = z ; u<x = a ; chain∋z = lt }
          ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim ( osuc-< w≤x c )
          ... | tri≈ ¬a z=x ¬c | tri< w<x ¬b ¬c₁ = ⊥-elim ( osuc-< z≤w (subst (λ k → w o< k ) (sym z=x) w<x ) )
          ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = λ lt → lt 
          ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim ( osuc-< w≤x c ) -- o<> c ( ord≤< w≤x )) -- z≡w x o< w
          ... | tri> ¬a ¬b c | t = ⊥-elim ( osuc-< w≤x (ord≤< c  z≤w ) ) -- x o< z → x o< w 
-         u-total : {z : Ordinal}  → z o≤ x → IsTotalOrderSet (supf0 z)
-         u-total {z}  z<x ux uy  with trio< z x
-         ... | t = {!!}
-         -- with trio< (UZFChain.u ux) (UZFChain.u uy)
-         -- ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) {!!} (u-mono (UZFChain.u ux) (UZFChain.u uy)
-         --    (UZFChain.u<x uy) (ordtrans a <-osuc ) (uzc ux) (uzc uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
-         -- ... | tri≈ ¬a b ¬c = ZChain.f-total (uzc ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
-         --    (UZFChain.u<x ux) (subst (λ k → k o< osuc (UZFChain.u ux)) b <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy))
-         -- ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
-         --    (UZFChain.u<x ux) (ordtrans c <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) 
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain A y f (& A)
-     SZ f mf = TransFinite {λ z → {y : Ordinal } → (ay : odef A y ) → ZChain A y f z  } (ind f mf) (& A)
+     SZ f mf {y} ay = TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) (& A)
+
+     ind-mono : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) { y : Ordinal} (ay : odef A y) → (x : Ordinal)
+         → (prev : (z : Ordinal) → z o< x → ZChain A y f z) 
+         → (z : Ordinal) → (z<x : z o< x) → ZChain.chain  (prev z z<x )  ⊆'  ZChain.chain ( ind f mf ay x prev )
+     ind-mono f mf ay x prev z z<x = {!!}
+
+     SZ-mono : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y)
+o        {a b : Ordinal } → a o< b →
+         ZChain.chain (TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) a )  ⊆' 
+         ZChain.chain (TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) b )
+     SZ-mono f mf {y} ay = ?
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM