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

changeset 576:59c11152f604

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 Sun, 05 Jun 2022 22:49:04 +0900
parents 3abf55c8e295
children cfb26091e806
files src/zorn.agda
diffstat 1 files changed, 25 insertions(+), 56 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Jun 05 19:50:18 2022 +0900
+++ b/src/zorn.agda	Sun Jun 05 22:49:04 2022 +0900
@@ -243,7 +243,6 @@
       chain∋x : odef chain x
       initial : {y : Ordinal } → odef chain y → * x ≤ * y
       f-total : IsTotalOrderSet chain 
-      f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
           → HasPrev A chain ab f ∨  IsSup A chain ab  
@@ -272,10 +271,6 @@
 Zorn-lemma {A}  0<A supP = zorn00 where
      supO : (C : HOD ) → C ⊆' A → IsTotalOrderSet C → Ordinal
      supO C C⊆A TC = & ( SUP.sup ( supP  C  C⊆A TC ))
-     postulate
-        --- irrelevance of ⊆' and compare
-        sup== : {C C1 : HOD } → C ≡ C1 → {c  : C ⊆' A } {c1 : C1 ⊆' A } → {t  : IsTotalOrderSet C } {t1 : IsTotalOrderSet C1 }
-         → SUP.sup ( supP  C c t )  ≡  SUP.sup ( supP  C1 c1 t1 )
      <-irr0 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
      <-irr0 {a} {b} A∋a A∋b = <-irr
      z07 :   {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -359,8 +354,10 @@
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
                    ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
                    -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ?  (SUP.x<sup sp1 ? ) }
+           z21 : { x : Ordinal } → odef chain x → odef chain (f x)
+           z21 {x} cx = ZChain.is-max zc cx {!!} {!!} (case1 record {y = x ; ay = cx ; x=fy = refl }) {!!}
            z14 :  f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc))
-           z14 with ZChain.f-total zc  (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
+           z14 with ZChain.f-total zc  (subst (λ k → odef chain k) (sym &iso) (z21 z12)) z12 
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
                z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
@@ -369,7 +366,7 @@
            ... | 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 ))
+               z15  = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (z21 z12)) 
                z17 : ⊥
                z17 with z15
                ... | case1 eq = ¬b eq
@@ -408,7 +405,7 @@
           zc4 with ODC.∋-p O A (* x)
           ... | no noax =  -- ¬ A ∋ p, just skip
                  record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 
-                     ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
+                     ; f-total = ZChain.f-total zc0 
                      ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = zc12 }  where
                      -- no extention
                 zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
@@ -431,19 +428,19 @@
                             * a < * b → odef (ZChain.chain zc0) b
                 zc17 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b
-                ... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
+                ... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) {!!}
                 zc10 : {a : Ordinal} → a o< osuc x → (ca : odef (ZChain.chain zc0) a) →
                     IsSup A (ZChain.chain zc0) (ZChain.chain⊆A zc0 ca) ∨ HasPrev A (ZChain.chain zc0) (ZChain.chain⊆A zc0 ca) f 
                 zc10 {a} a<x ca with osuc-≡< a<x
                 ... | case2 lt = ZChain.fc∨sup zc0  (zc0-b<x a lt)  ca
                 ... | case1 refl = case2 record { y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (sym &iso) (HasPrev.x=fy pr) }
                 zc9 :  ZChain A ay f mf supO x
-                zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 -- no extention
+                zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0  
                      ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17
                      ; fc∨sup = zc10 } 
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
           ... | case1 is-sup = -- x is a sup of zc0 
-                record { chain = schain ; chain⊆A = s⊆A  ; f-total = scmp ; f-next = scnext 
+                record { chain = schain ; chain⊆A = s⊆A  ; f-total = scmp 
                      ; initial = scinit ; f-immediate =  simm ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax ; fc∨sup = zc19 } where 
                 sup0 : SUP A (ZChain.chain zc0) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
@@ -456,21 +453,20 @@
                 x=sup : x ≡ & sp 
                 x=sup = sym &iso 
                 chain = ZChain.chain zc0
-                sc<A : {y : Ordinal} → odef chain y ∨ FClosure A f (& sp) y → y o< & A
+                sc<A : {y : Ordinal} → odef chain y ∨ (& sp ≡ y) → y o< & A
                 sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A zc0 (subst (λ k → odef chain k) (sym &iso) zx )))
-                sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) )
+                sc<A {y} (case2 fx) = {!!}
                 schain : HOD
-                schain = record { od = record { def = λ x → odef chain x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
+                schain = record { od = record { def = λ x → odef chain x ∨ (& sp ≡ x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
                 A∋schain : {x : HOD } → schain ∋ x → A ∋ x
                 A∋schain (case1 zx ) = ZChain.chain⊆A zc0 zx 
-                A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx 
+                A∋schain {y} (case2 fx ) = {!!}
                 s⊆A : schain ⊆' A
                 s⊆A {x} (case1 zx) = ZChain.chain⊆A zc0 zx
-                s⊆A {x} (case2 fx) = A∋fc (& sp) f mf fx 
+                s⊆A {x} (case2 fx) = {!!}
                 zc19 :  {a : Ordinal} → a o< osuc x → (sa : odef schain a) →
                     IsSup A schain (s⊆A sa) ∨ HasPrev A schain (s⊆A sa) f 
-                zc19 a<x (case2 (init asp)) = case1 {!!} 
-                zc19 a<x (case2 (fsuc y fc)) = case2 record { y = y ; ay = case2 fc ; x=fy = refl }
+                zc19 a<x (case2 eq) = case1 {!!} 
                 zc19 {a} a<x (case1 ca) with osuc-≡< a<x
                 ... | case1 refl = case1 record { x<sup = {!!} }   -- a ≡ x
                 ... | case2 lt with ZChain.fc∨sup zc0 (zc0-b<x a lt) ca
@@ -494,59 +490,34 @@
                         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 (case1 za) (case1 zb) = ZChain.f-total zc0 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
-                ... | tri≈ ¬a b ¬c = tri≈ ¬c (sym b) ¬a
-                ... | tri> ¬a ¬b c = tri< c (λ eq → ¬b (sym eq))  ¬a
-                scmp (case2 fa) (case2 fb) = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp (& sp) f mf fa fb)
-                scnext : {a : Ordinal} → odef schain a → odef schain (f a)
-                scnext {x} (case1 zx) = case1 (ZChain.f-next zc0 zx)
-                scnext {x} (case2 sx) = case2 ( fsuc x sx )
+                scmp {a} {b} (case1 za) (case2 fb) = {!!}
+                scmp (case2 fa) (case2 fb) = {!!}
+                scmp _ _ = {!!}
                 scinit :  {x : Ordinal} → odef schain x → * y ≤ * x
                 scinit {x} (case1 zx) = ZChain.initial zc0 zx
-                scinit {x} (case2 sx) with  (s≤fc (& sp) f mf sx ) |  SUP.x<sup sup0 (subst (λ k → odef chain k ) (sym &iso) ( ZChain.chain∋x zc0 ) )
-                ... | case1 sp=x | case1 y=sp = case1 (trans y=sp (subst (λ k → k ≡ * x ) *iso sp=x ) )
-                ... | case1 sp=x | case2 y<sp = case2 (subst (λ k → * y < k ) (trans (sym *iso) sp=x) y<sp )
-                ... | case2 sp<x | case1 y=sp = case2 (subst (λ k → k < * x ) (trans *iso (sym y=sp )) sp<x )
-                ... | case2 sp<x | case2 y<sp = case2 (ptrans y<sp (subst (λ k → k < * x ) *iso sp<x) )
+                scinit {x} (case2 sx) = {!!}
                 A∋za : {a : Ordinal } → odef chain a → odef A a
                 A∋za za = ZChain.chain⊆A zc0 za 
                 za<sup :  {a : Ordinal } → odef chain a → ( * a ≡ sp ) ∨  ( * a < sp )
                 za<sup za =  SUP.x<sup sup0 (subst (λ k → odef chain k ) (sym &iso) za )
                 simm : {a b : Ordinal}  → odef schain a → odef schain b → ¬ (* a < * b) ∧ (* b < * (f a))
-                simm {a} {b} (case1 za) (case1 zb) = ZChain.f-immediate zc0 za zb
-                simm {a} {b} (case1 za) (case2 sb) p with  proj1 (mf a (A∋za za) )
-                ... | case1 eq = <-irr (case2  (subst (λ k → * b < k ) (sym eq) (proj2 p))) (proj1 p) 
-                ... | case2 a<fa with za<sup  ( ZChain.f-next zc0 za ) | s≤fc (& sp) f mf sb
-                ... | case1 fa=sp | case1 sp=b = <-irr (case1 (trans fa=sp (trans (sym *iso) sp=b )) ) ( proj2 p )
-                ... | case2 fa<sp | case1 sp=b = <-irr (case2 fa<sp) (subst (λ k → k < * (f a) ) (trans (sym sp=b) *iso) (proj2 p ) )
-                ... | case1 fa=sp | case2 sp<b = <-irr (case2 (proj2 p )) (subst  (λ k → k < * b) (sym fa=sp) (subst (λ k → k < * b ) *iso sp<b ) )
-                ... | case2 fa<sp | case2 sp<b = <-irr (case2 (proj2 p )) (ptrans fa<sp (subst (λ k → k < * b ) *iso sp<b ) )
-                simm {a} {b} (case2 sa) (case1 zb) p with  proj1 (mf a ( subst (λ k → odef A k) &iso ( A∋schain (case2 (subst (λ k → FClosure A f (& sp) k ) (sym &iso) sa) )) ) )
-                ... | case1 eq = <-irr (case2  (subst (λ k → * b < k ) (sym eq) (proj2 p))) (proj1 p) 
-                ... | case2 b<fb with  s≤fc (& sp) f mf sa | za<sup zb
-                ... | case1 sp=a | case1 b=sp = <-irr (case1 (trans b=sp (trans (sym *iso) sp=a )) ) (proj1 p )
-                ... | case1 sp=a | case2 b<sp = <-irr (case2 (subst (λ k → * b < k ) (trans (sym *iso) sp=a)  b<sp ) ) (proj1 p )
-                ... | case2 sp<a | case1 b=sp = <-irr (case2 (subst ( λ  k → k < * a ) (trans *iso (sym b=sp)) sp<a  )) (proj1 p )
-                ... | case2 sp<a | case2 b<sp = <-irr (case2 (ptrans b<sp (subst (λ k → k < * a) *iso sp<a ))) (proj1 p )
-                simm {a} {b} (case2 sa) (case2 sb) p = fcn-imm {A} (& sp) {a} {b} f mf sa sb p
+                simm = {!!}
                 s-ismax : {a b : Ordinal} → odef schain a → b o< osuc x → (ab : odef A b)
                     → HasPrev A schain ab f ∨ IsSup A schain ab   
                     → * a < * b → odef schain b
                 s-ismax {a} {b} sa b<ox ab p a<b with osuc-≡< b<ox -- b is x?
-                ... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) (sym (trans b=x x=sup )) (init (SUP.A∋maximal sup0) ))
+                ... | case1 b=x = {!!}
                 s-ismax {a} {b} (case1 za) b<ox ab (case1 p) a<b | case2 b<x = z21 p where   -- has previous
                      z21 : HasPrev A schain ab f → odef schain b
                      z21 record { y = y ; ay = (case1 zy) ; x=fy = x=fy } = 
                            case1 (ZChain.is-max zc0 za (zc0-b<x b b<x) ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b )
-                     z21 record { y = y ; ay = (case2 sy) ; x=fy = x=fy } = subst (λ k → odef schain k) (sym x=fy) (case2 (fsuc y sy) )
+                     z21 record { y = y ; ay = (case2 sy) ; x=fy = x=fy } = {!!}
                 s-ismax {a} {b} (case1 za) b<ox ab (case2 p) a<b | case2 b<x = case1 (ZChain.is-max zc0 za (zc0-b<x b b<x) ab (case2 z22) a<b ) where -- previous sup
                      z22 : IsSup A (ZChain.chain zc0)   ab 
                      z22 = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
                 s-ismax {a} {b} (case2 sa) b<ox ab (case1 p)  a<b | case2 b<x with HasPrev.ay p
-                ... | case1 zy = case1 (subst (λ k → odef chain k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc0 zy ))               -- in previous closure of f
-                ... | case2 sy = case2 (subst (λ k → FClosure A f (& (* x)) k ) (sym (HasPrev.x=fy p)) (fsuc (HasPrev.y p) sy ))  -- in current  closure of f
+                ... | case1 zy = case1 (subst (λ k → odef chain k ) (sym (HasPrev.x=fy p)) {!!})               -- in previous closure of f
+                ... | case2 sy = {!!}
                 s-ismax {a} {b} (case2 sa) b<ox ab (case2 p)  a<b | case2 b<x = case1 z23 where -- sup o< x is already in zc0
                      z24 : IsSup A schain ab → IsSup A (ZChain.chain zc0) ab 
                      z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
@@ -555,7 +526,7 @@
                      ... | case1 y=b  = subst (λ k → odef chain k )  y=b ( ZChain.chain∋x zc0 )
                      ... | case2 y<b  = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b
           ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
-                   record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
+                   record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 
                      ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 ; fc∨sup = {!!} }  where
                       -- no extention
                 z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
@@ -569,7 +540,7 @@
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
      ... | no ¬ox = UnionZ where
        UnionZ : ZChain A ay f mf supO x
-       UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next
+       UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  
                      ; initial = u-initial ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
             field
@@ -583,8 +554,6 @@
          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))) }
-         u-next : {z : Ordinal} → odef Uz z → odef Uz (f z)
-         u-next {z} u = record { u = UZFChain.u u ; u<x = UZFChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UZFChain.chain∋z u)  }
          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