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

changeset 642:b46a0a2b32e5

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, 26 Jun 2022 20:11:28 +0900
parents 4f48fe1b884a
children a7e538a7c87f
files src/ordinal.agda src/zorn.agda
diffstat 2 files changed, 36 insertions(+), 124 deletions(-) [+]
line wrap: on
line diff
--- a/src/ordinal.agda	Sat Jun 25 13:30:17 2022 +0900
+++ b/src/ordinal.agda	Sun Jun 26 20:11:28 2022 +0900
@@ -221,11 +221,11 @@
             ψ (record { lv = lx ; ord = OSuc lx x₁ })
         caseOSuc lx ox prev = ind (ordinal lx (OSuc lx ox)) prev 
 
-TP : {n m l : Level} → {Q : Ordinal {suc n} → Set m} {P : { x y : Ordinal {suc n} } → Q x → Q y → Set l}  
-    → ( ind : (x : Ordinal {suc n})  → ( (y : Ordinal  {suc n} ) → y o< x → Q y ) → Q x )                                                                 
-    → ( (x : Ordinal {suc n} )  → ( prev : (y : Ordinal {suc n} ) → y o< x → Q y ) → {y : Ordinal {suc n}} → (y<x : y o< x)  → P (prev y y<x) (ind x prev)  )  
-    →  {x z : Ordinal {suc n} } → (z≤x : z o< osuc x ) → P (TransFinite3 {n} {m} { λ x → Q x } ind z  )  (TransFinite3 {n} {m} { λ x → Q x } ind x  )
-TP {n} {m} {l} {Q} {P} ind indP {x} {z} z≤x = ?
+-- TP : {n m l : Level} → {Q : Ordinal {suc n} → Set m} {P : { x y : Ordinal {suc n} } → Q x → Q y → Set l}  
+--     → ( ind : (x : Ordinal {suc n})  → ( (y : Ordinal  {suc n} ) → y o< x → Q y ) → Q x )                                                                 
+--     → ( (x : Ordinal {suc n} )  → ( prev : (y : Ordinal {suc n} ) → y o< x → Q y ) → {y : Ordinal {suc n}} → (y<x : y o< x)  → P (prev y y<x) (ind x prev)  )  
+--     →  {x z : Ordinal {suc n} } → (z≤x : z o< osuc x ) → P (TransFinite3 {n} {m} { λ x → Q x } {!!} x  )  {!!} -- P (TransFinite {?} ind z) (TransFinite {?} ind x )
+-- TP = ?
  
 
 open import Ordinals 
--- a/src/zorn.agda	Sat Jun 25 13:30:17 2022 +0900
+++ b/src/zorn.agda	Sun Jun 26 20:11:28 2022 +0900
@@ -235,13 +235,9 @@
 
 record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
    field
-      supf : Ordinal → HOD
-   chain : HOD
-   chain = supf z 
-   field
+      chain : HOD
       chain⊆A : chain ⊆' A
       chain∋x : odef chain x
-      mono : {y : Ordinal} → y o≤ z →  supf y ⊆' supf z 
       initial : {y : Ordinal } → odef chain y → * x ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
@@ -393,57 +389,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⊆A = λ fx →  A∋fc y f mf fx
-                     ; f-next = λ {x} sx → fsuc x sx  ; supf = λ _ → ys ay f mf  ; mono = ? 
-                     ; initial = {!!} ; chain∋x  = init ay ; is-max = is-max } where
+                     ; f-next = λ {x} sx → fsuc x sx  ; supf = λ _ → ys ay f mf  ; chain = ys ay f mf
+                     ; initial = initial ; 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 = {!!}
+               is-max {a} {b} yca b≤x ab P a<b = ?
                initial : {i : Ordinal} → odef (ys ay f mf) i → * y ≤ * i
                initial {i} (init ai) = case1 refl
                initial .{f x} (fsuc x lt) = {!!}
 
-     sind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
-         → ((z : Ordinal) → z o< x → HOD ) → HOD
-     sind f mf {y} ay x prev  with Oprev-p x
-     ... | yes op = sc4 where
-          px = Oprev.oprev op
-          sc : HOD
-          sc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
-
-          sc4 : HOD
-          sc4 with ODC.∋-p O A (* x)
-          ... | no noax = {!!}
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A sc ax f )   
-          ... | case1 pr = sc
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A sc ax )
-          ... | case1 is-sup =  schain where
-                -- A∋sc -- x is a sup of zc 
-                sup0 : SUP A sc 
-                sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
-                        x21 :  {y : HOD} → sc ∋ y → (y ≡ * x) ∨ (y < * x)
-                        x21 {y} zy with IsSup.x<sup is-sup zy 
-                        ... | case1 y=x = case1 ( subst₂ (λ j k → j ≡ * k  ) *iso &iso ( cong (*) y=x)  )
-                        ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x  )
-                sp : HOD
-                sp = SUP.sup sup0 
-                schain : HOD
-                schain = record { od = record { def = λ x → odef sc x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
-          ... | case2 ¬x=sup =  sc
-     ... | no ¬ox with trio< x y
-     ... | tri< a ¬b ¬c = {!!}
-     ... | tri≈ ¬a b ¬c = {!!}
-     ... | tri> ¬a ¬b y<x = Uz where
-         record Usup (z : Ordinal) : Set n where -- Union of supf from y which has maximality o< x
-            field
-               u : Ordinal
-               u<x : u o< x
-               chain∋z : odef (prev u u<x ) z
-         Uz : HOD
-         Uz = record { od = record { def = λ y → Usup y } ; odmax = & A
-             ; <odmax = {!!} } -- λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) }
 
 
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
@@ -454,8 +411,6 @@
           -- 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 ) )
           zc : ZChain A y f (Oprev.oprev op)
           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
@@ -468,27 +423,12 @@
           no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc) ab f ∨  IsSup A (ZChain.chain zc) ab →
                             * a < * b → odef (ZChain.chain zc) b ) → ZChain A y f x
-          no-extenion is-max = record { supf = supf0 ;  chain⊆A = subst (λ k → k ⊆' A ) seq (ZChain.chain⊆A zc)
-                     ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) seq (ZChain.initial zc)
-                     ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) seq (ZChain.f-next zc)  ; mono = ? 
-                     ; chain∋x  = subst (λ k → odef k y ) seq (ZChain.chain∋x  zc)
+          no-extenion is-max = record { chain⊆A = subst (λ k → k ⊆' A ) ? (ZChain.chain⊆A zc)
+                     ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) ? (ZChain.initial zc)
+                     ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) ? (ZChain.f-next zc)  ; chain  = ZChain.chain zc 
+                     ; chain∋x  = subst (λ k → odef k y ) ? (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 } where
-                supf0 : Ordinal → HOD
-                supf0 z with trio< z x
-                ... | tri< a ¬b ¬c = supf z
-                ... | tri≈ ¬a b ¬c = ZChain.chain zc
-                ... | tri> ¬a ¬b c = ZChain.chain zc 
-                seq : ZChain.chain zc ≡ supf0 x 
-                seq with trio< x x
-                ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
-                ... | tri≈ ¬a b ¬c = refl 
-                ... | tri> ¬a ¬b c = refl 
-                seq<x : {b : Ordinal } → b o< x →  supf b  ≡ supf0 b
-                seq<x {b} b<x with trio< b x
-                ... | tri< a ¬b ¬c = refl
-                ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
-                ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
+                                 HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) ? is-max } 
 
           zc4 : ZChain A y f x 
           zc4 with ODC.∋-p O A (* x)
@@ -510,8 +450,8 @@
                 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
           ... | 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 = {!!}  ; mono = ?
-                     ; initial = {!!} ; chain∋x  = {!!} ; is-max = {!!}   ; supf = supf0 } where
+                record {  chain⊆A = {!!} ; f-next = {!!}  ; chain = schain
+                     ; initial = {!!} ; chain∋x  = {!!} ; is-max = {!!}   } 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)
@@ -528,11 +468,6 @@
                 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 )) )
                 schain : HOD
                 schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
-                supf0 : Ordinal → HOD
-                supf0 z with trio< z x
-                ... | tri< a ¬b ¬c = supf z
-                ... | tri≈ ¬a b ¬c = schain 
-                ... | tri> ¬a ¬b c = schain
                 A∋schain : {x : HOD } → schain ∋ x → A ∋ x
                 A∋schain (case1 zx ) = ZChain.chain⊆A zc zx 
                 A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx 
@@ -598,18 +533,6 @@
                      z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋x zc )
                      ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋x zc )
                      ... | case2 y<b  = ZChain.is-max zc (ZChain.chain∋x zc ) (zc-b<x b b<x) ab (case2 (z24 p)) y<b
-                seq : schain ≡ supf0 x 
-                seq with trio< x x
-                ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
-                ... | tri≈ ¬a b ¬c = refl
-                ... | tri> ¬a ¬b c = refl
-                seq<x : {b : Ordinal } → b o< x →  supf b  ≡ supf0 b
-                seq<x {b} b<x with trio< b x
-                ... | 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 = {!!}
 
           ... | case2 ¬x=sup =  no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
                 z18 :  {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
@@ -624,7 +547,7 @@
      ... | no ¬ox with trio< x y
      ... | tri< a ¬b ¬c = init-chain ay f mf {!!}
      ... | tri≈ ¬a b ¬c = init-chain ay f mf {!!}
-     ... | tri> ¬a ¬b y<x = record { supf = supf0 ; chain⊆A = {!!} ; f-next = {!!} ; mono = ?
+     ... | tri> ¬a ¬b y<x = record { chain⊆A = {!!} ; f-next = {!!} ; chain = Uz
                      ; initial = {!!} ; 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
@@ -644,33 +567,18 @@
          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 ) }
-         supf0 : Ordinal → HOD
-         supf0 z with trio< z x
-         ... | tri< a ¬b ¬c = ZChain.supf (prev z a ) z
-         ... | tri≈ ¬a b ¬c = Uz 
-         ... | tri> ¬a ¬b c = Uz
-         seq : Uz ≡ supf0 x
-         seq with trio< x x
-         ... | 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 ) b  ≡ supf0 b
-         seq<x {b} b<x with trio< b x
-         ... | 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
          ord≤< {x} {y} {z} x<z z≤y  with  osuc-≡< z≤y
          ... | case1 z=y  = subst (λ k → x o< k ) z=y x<z
          ... | case2 z<y  = ordtrans x<z z<y
-         u-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w
+         u-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → ? ⊆' ? 
          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 ) z) i → odef  (ZChain.supf (prev w a₁ ) w) i 
-             um00 = {!!}
-             um01 : odef  (ZChain.supf (prev z a ) z) i → odef  (ZChain.supf (prev z {!!} ) w) i 
-             um01 = ? -- ZChain.mono (prev z a ) ?  ?
-         ... | 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₁ = ? -- um00 where -- ZChain.chain-mono (prev w ? ay) ? ? lt
+             -- 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 ) z) i → odef  (ZChain.supf (prev z {!!} ) w) i 
+             -- um01 = ? -- ZChain.mono (prev z a ) ?  ?
+         ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = λ lt → record { u = z ; u<x = a ; chain∋z = ? }
          ... | 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 
@@ -685,20 +593,21 @@
           → (ind :  (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : Ordinal)  →   ind  x (λ y _ → TransFinite ind  y )  ≡ TransFinite ind  x
 
-     record ZChain1 (supf : (z : Ordinal ) → HOD ) ( z : Ordinal ) : Set (Level.suc n) where
+     record ZChain1 ( f : Ordinal → Ordinal )  ( y z : Ordinal ) : Set (Level.suc n) where
       field
-         chain-mono : {x y : Ordinal} → x o≤ y → y o≤ z →  supf x ⊆' supf y 
-         f-total : {x : Ordinal} → x o≤ z → IsTotalOrderSet (supf x) 
+         zc : { x : Ordinal } → x o< z → ZChain A y f x
+         chain-mono : {x y : Ordinal} → (x≤y : x o≤ y) → (y<z : y o< z ) →  ZChain.chain (zc ?)  ⊆' ZChain.chain (zc y<z ) 
+         f-total : {x : Ordinal} → (x<z : x o< z ) → IsTotalOrderSet (ZChain.chain (zc x<z ) )
 
      SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y)
-         → (z : Ordinal) → ZChain1 ( λ y → ZChain.chain (TransFinite (ind f mf ay ) y) ) z
+         → (z : Ordinal) → ZChain1 f y z
      SZ1 f mf {y} ay z = TransFinite {λ w → {!!} w} {!!} z where
          indp :  (x : Ordinal) →
-            ((y₁ : Ordinal) → y₁ o< x → ZChain1 (λ y₂ → ZChain.chain (TransFinite (ind f mf ay) y₂)) y₁) →
-            ZChain1 (λ y₁ → ZChain.chain (TransFinite (ind f mf ay) y₁)) x
+            ((y₁ : Ordinal) → y₁ o< x → ZChain1 f y y₁) →
+            ZChain1 f y x
          indp x prev with Oprev-p x
          ... | yes op  = sz02 where
-             sz02 : ZChain1 (λ y₁ → ZChain.chain (TransFinite (ind f mf ay) y₁)) x
+             sz02 : ZChain1 f y ?
              sz02 with ODC.∋-p O A (* x)
              ... | no noax = {!!}
              ... | yes noax = {!!}
@@ -732,7 +641,10 @@
               zc5 = ⟪  Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫
          zorn04 : ZChain A (& s) (cf nmx) (& A)
          zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
-         zc1 =  (ZChain1.f-total (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) (& A)) o≤-refl )
+         zc0 : ZChain1  (cf nmx) (& s) (osuc (& A))
+         zc0 = SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) (osuc (& A))
+         zc1 :  IsTotalOrderSet ( ZChain.chain (ZChain1.zc zc0 <-osuc ) )
+         zc1 =  ZChain1.f-total zc0 <-osuc 
 
 -- usage (see filter.agda )
 --