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

changeset 617:50999e72f19f

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 Sat, 18 Jun 2022 00:41:37 +0900
parents fae0fa6184d5
children b726eedf9041
files src/zorn.agda
diffstat 1 files changed, 40 insertions(+), 77 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Jun 18 00:07:25 2022 +0900
+++ b/src/zorn.agda	Sat Jun 18 00:41:37 2022 +0900
@@ -233,21 +233,6 @@
    field
       x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
-record FChain ( A : HOD ) ( f : Ordinal → Ordinal ) (p c z : Ordinal)   ( x : Ordinal ) : Set n where
-   field
-      fc∨sup :  FClosure A f p x
-      chain∋p : odef (* c) p 
-
-record FSup ( A : HOD ) ( f : Ordinal → Ordinal ) (p c z : Ordinal)   ( x : Ordinal ) : Set n where
-   field
-      sup :  (z : Ordinal) → FClosure A f p z → * z < * x 
-      chain∋p : odef (* c) p 
-
-data Fc∨sup (A : HOD) {y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) (c z : Ordinal) : (x : Ordinal) → Set n where
-      Finit :  {i : Ordinal} → i ≡ y  → Fc∨sup A ay f c z i
-      Fsup  :  {p x : Ordinal} → p o< x → Fc∨sup A ay f c z p → FSup   A f p c z x → x o< osuc z  →  Fc∨sup A ay f c z x
-      Fc    :  {p x : Ordinal} → p o< x → Fc∨sup A ay f c z p → FChain A f p c z x →  Fc∨sup A ay f c z x
-
 record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
    field
       chain : HOD
@@ -260,9 +245,6 @@
       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  
           → * a < * b  → odef chain b
-      chain∋sup : (s : HOD) → s ⊆' chain → {b : Ordinal} (ab : odef A b) → b o< osuc z  → IsSup A s ab → odef chain b
-      fc∨sup :  {c : Ordinal } → ( ca : odef chain c )  → Fc∨sup A (chain⊆A chain∋x) f (& chain) z c
-
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -406,22 +388,18 @@
      ys {y} ay f mf = record { od = record { def = λ x →  FClosure A f y x  } ; odmax = & A ; <odmax = {!!} }
      init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain A y f x
      init-chain {y} {x} ay f mf x≤y = record { chain = ys ay f mf ; chain⊆A = λ fx →  A∋fc y f mf fx
-                     ; f-total = i-total ; f-next = λ {x} sx → fsuc x sx ; chain∋sup = {!!}
-                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = init ay ; is-max = is-max ; fc∨sup = it01 } where
+                     ; f-total = i-total ; f-next = λ {x} sx → fsuc x sx 
+                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = init ay ; is-max = is-max } where
                i-total : IsTotalOrderSet (ys ay f mf )
                i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb)
                is-max : {a b : Ordinal} → odef (ys ay f mf) a →
                     b o< osuc x → (ab : odef A b) → HasPrev A (ys ay f mf) ab f ∨ IsSup A (ys ay f mf) ab →
                     * a < * b → odef (ys ay f mf) b
                is-max {a} {b} yca b≤x ab P a<b = {!!}
-               it01 : {c : Ordinal} → odef (ys ay f mf) c → Fc∨sup A (A∋fc y f mf (init ay)) f (& (ys ay f mf)) x c
-               it01 {c} cc = Fsup {!!} (Finit refl) record { fc∨sup = {!!} ; chain∋p = {!!} } {!!}
                initial : {i : Ordinal} → odef (ys ay f mf) i → * y ≤ * i
                initial {i} (init ai) = case1 refl
                initial .{f x} (fsuc x lt) = {!!}
 
-     chain-mono :  {x y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) { a b : Ordinal }
-         → (zx : ZChain A y f a ) → (zy : ZChain A y f b)  → a o≤ b → b o< osuc x →  ZChain.chain zx ⊆' ZChain.chain zy
 
      --
      -- create all ZChains under o< x
@@ -443,23 +421,12 @@
           px<x : px o< x
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
 
-          fcs< :  (A : HOD) {w y : Ordinal} (ay : odef A y)   (c z : Ordinal) (x : Ordinal)
-                → z o< w → Fc∨sup  A ay f c z x → Fc∨sup  A ay f c w x 
-          fcs< A ay c z x z<w (Finit x₁) = Finit x₁
-          fcs< A {w} ay c z x z<w (Fsup {p} x₁ FC x₂ x₃) = Fsup x₁ (fcs< A ay c z p z<w FC) record { sup = FSup.sup x₂  ; chain∋p =  FSup.chain∋p x₂  } 
-                 (x<ow x₃ z<w ) where
-              x<ow : x o< osuc z → z o< w → x o< osuc w
-              x<ow x<z z<w = ordtrans x<z (osucc z<w)
-          fcs< A {w} ay c z x z<w (Fc {p} x₁ FC x₂) = Fc x₁ (fcs< A ay c z p z<w FC) record { fc∨sup = FChain.fc∨sup x₂; chain∋p = FChain.chain∋p x₂} 
-
           zc4 : ZChain A y f x 
           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 ; chain∋sup = {!!}
-                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = zc12 }  where -- no extention
-                zc12 : {c : Ordinal} → odef (ZChain.chain zc0) c → Fc∨sup A (ZChain.chain⊆A zc0 (ZChain.chain∋x zc0)) f (& (ZChain.chain zc0)) x c
-                zc12 {c} cc = fcs< A (ZChain.chain⊆A zc0 (ZChain.chain∋x zc0)) (& (ZChain.chain zc0)) px c px<x (ZChain.fc∨sup zc0 cc)
+                     ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 
+                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 }  where -- no extention
                 zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc0) ab f ∨  IsSup A (ZChain.chain zc0) ab →
                             * a < * b → odef (ZChain.chain zc0) b
@@ -477,12 +444,11 @@
                 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
                 zc9 :  ZChain A y f 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
-                     ; chain∋sup = {!!}
-                     ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = {!!} } 
+                     ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 }
           ... | 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 ; chain∋sup = {!!}
-                     ; initial = scinit ; f-immediate =  simm ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax ; fc∨sup = s-fc∨sup} where 
+                record { chain = schain ; chain⊆A = s⊆A  ; f-total = scmp ; f-next = scnext 
+                     ; initial = scinit ; f-immediate =  simm ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax } where 
                 sup0 : SUP A (ZChain.chain zc0) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
                         x21 :  {y : HOD} → ZChain.chain zc0 ∋ y → (y ≡ * x) ∨ (y < * x)
@@ -505,9 +471,6 @@
                 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-fc∨sup : {c : Ordinal} → odef schain c → Fc∨sup A (s⊆A (case1 (ZChain.chain∋x zc0))) f (& schain) x c 
-                s-fc∨sup {c} (case1 cx) = {!!}
-                s-fc∨sup {c} (case2 fc) = {!!}
                 cmp  : {a b : HOD} (za : odef chain0 (& a)) (fb : FClosure A f (& sp) (& b)) → Tri (a < b) (a ≡ b) (b < a )
                 cmp {a} {b} za fb  with SUP.x<sup sup0 za | s≤fc (& sp) f mf fb  
                 ... | case1 sp=a | case1 sp=b = tri≈ (λ lt → <-irr (case1 (sym eq)) lt ) eq (λ lt → <-irr (case1 eq) lt ) where
@@ -602,8 +565,8 @@
      ... | tri≈ ¬a b ¬c = init-chain ay f mf {!!}
      ... | tri> ¬a ¬b y<x = UnionZ where
        UnionZ : ZChain A y f x
-       UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next ; chain∋sup = {!!}
-                     ; initial = u-initial ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  where --- limit ordinal case
+       UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next 
+                     ; initial = u-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
@@ -622,8 +585,38 @@
          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 = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) }
+
+         ind-mono :  {y : Ordinal } (ay : odef A y ) {a b : Ordinal } ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (zb : ZChain A y f b) →
+             (x : Ordinal)
+                → ((c : Ordinal) → c o< x → a o≤ b → b o≤ c → (za : ZChain A y f a) {i : Ordinal} → odef (ZChain.chain za) i → odef (ZChain.chain zb) i)
+                → a o≤ b → b o≤ x → (za : ZChain A y f a) {i : Ordinal} → odef (ZChain.chain za) i → odef (ZChain.chain zb) i
+         ind-mono {y} ay {a} {b} f mf zb x prev-mono a≤b b≤x za {i} zai with Oprev-p x
+         ... | yes op = mc00 where
+              open ZChain
+              px = Oprev.oprev op
+              zc0 : ZChain A y f (Oprev.oprev op)
+              zc0 = {!!} -- zfx (Oprev.oprev op) ay f mf
+              mc00 : odef (chain zb) i
+              mc00 with ODC.∋-p O A (* x)
+              ... | no noax = {!!}
+              ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax f )
+              ... | case1 pr = {!!}
+              ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
+              ... | case1 is-sup = {!!} -- x is a sup of zc0 
+              ... | case2 ¬x=sup  = {!!}
+         ... | no ¬ox with trio< x y
+         ... | tri< a ¬b ¬c = {!!}
+         ... | tri≈ ¬a b ¬c = {!!}
+         ... | tri> ¬a ¬b y<x = {!!}
+    
+         chain-mono :  {x y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) { a b : Ordinal }
+              → (zx : ZChain A y f a ) → (zy : ZChain A y f b)  → a o≤ b → b o< osuc x →  ZChain.chain zx ⊆' ZChain.chain zy
+         chain-mono {x} {y} ay f mf {a} {b} za zb a≤b b≤x = TransFinite {λ x →  
+             a o≤ b → b o≤ x  → (za : ZChain A y f a) → {i : Ordinal } → odef (ZChain.chain za) i → odef (ZChain.chain zb) i }
+             (ind-mono ay f mf zb) x a≤b b≤x za  
+
          u-mono :  ( a b : Ordinal ) → b o< osuc x → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b) → ZChain.chain za  ⊆' ZChain.chain zb
-         u-mono a b b≤x a≤b za zb {i} zai = chain-mono ay f mf za zb a≤b  b≤x zai
+         u-mono a b b≤x a≤b za zb {i} zai = {!!} -- chain-mono ay f mf za zb a≤b  b≤x zai
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy  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)
@@ -633,36 +626,6 @@
          ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
             (ordtrans (UZFChain.u<x ux) <-osuc)  (ordtrans c <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) 
 
-     zfx :  (x : Ordinal ) {y : Ordinal } (ay : odef A y ) ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → ZChain A y f x
-     zfx x ay f mf = TransFinite {λ z → {y : Ordinal } → (ay : odef A y ) → ZChain A y f z } (ind f mf) x ay
-
-     ind-mono :  (x : Ordinal ) {y : Ordinal } (ay : odef A y ) {b : Ordinal } ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (zb : ZChain A y f b) →
-             (a : Ordinal)
-                → ((c : Ordinal) → c o< a → c o≤ b → b o≤ x → (zc : ZChain A y f c) {i : Ordinal} → odef (ZChain.chain zc) i → odef (ZChain.chain zb) i)
-                → a o≤ b → b o≤ x → (za : ZChain A y f a) {i : Ordinal} → odef (ZChain.chain za) i → odef (ZChain.chain zb) i
-     ind-mono x {y} ay {b} f mf zb a prev a≤b b≤x za {i} zai with Oprev-p a
-     ... | yes op = mc00 where
-          open ZChain
-          px = Oprev.oprev op
-          zc0 : ZChain A y f (Oprev.oprev op)
-          zc0 = {!!} -- zfx (Oprev.oprev op) ay f mf
-          mc00 : odef (chain zb) i
-          mc00 with ODC.∋-p O A (* a)
-          ... | no noax = {!!}
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax f )
-          ... | case1 pr = {!!}
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
-          ... | case1 is-sup = {!!} -- x is a sup of zc0 
-          ... | case2 ¬x=sup  = {!!}
-     ... | no ¬ox with trio< x y
-     ... | tri< a ¬b ¬c = {!!}
-     ... | tri≈ ¬a b ¬c = {!!}
-     ... | tri> ¬a ¬b y<x = {!!}
-
-     chain-mono {x} {y} ay f mf {a} {b} za zb a≤b b≤x = TransFinite {λ a →  
-         a o≤ b → b o≤ x  → (za : ZChain A y f a) → {i : Ordinal } → odef (ZChain.chain za) i → odef (ZChain.chain zb) i }
-         (ind-mono x ay f mf zb) a a≤b b≤x za  
-
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
      ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where