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

changeset 647:7629714b4d07

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... zc1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Jun 2022 08:01:11 +0900
parents c2446d7d24c0
children 3821048a8552
files src/zorn.agda
diffstat 1 files changed, 37 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jun 27 03:23:44 2022 +0900
+++ b/src/zorn.agda	Mon Jun 27 08:01:11 2022 +0900
@@ -550,33 +550,57 @@
          u-chain∋x :  odef Uz y
          u-chain∋x = case2 ( init ay )
          
-     record ZChain1 ( f : Ordinal → Ordinal )  ( y z : Ordinal ) : Set (Level.suc n) where
-      inductive
+     record ZChain1 (y : Ordinal) ( f : Ordinal → Ordinal )  ( z : Ordinal ) : Set (Level.suc n) where
       field
-         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 {x} (ordtrans≤-< x≤y y<z))  ⊆' ZChain.chain (zc y<z ) 
-         f-total : {x : Ordinal} → (x<z : x o< z ) → IsTotalOrderSet (ZChain.chain (zc x<z ) )
+         zc : { x : Ordinal } → x o< z → HOD
+         chain-mono : {x y : Ordinal} → (x≤y : x o≤ y) → (y<z : y o< z ) →  zc {x} (ordtrans≤-< x≤y y<z)  ⊆' zc y<z  
+         f-total : {x : Ordinal} → (x<z : x o< z ) → IsTotalOrderSet (zc x<z ) 
 
      SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y)
-         → (z : Ordinal) → ZChain1 f y z
-     SZ1 f mf {y} ay z = TransFinite {λ w → ZChain1 f y w } indp z where
+         → (z : Ordinal) → ZChain1 y f z
+     SZ1 f mf {y} ay z = TransFinite {λ w → ZChain1 y f w } indp z where
          open ZChain
          open ZChain1
-         indp :  (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 f y y₁) → ZChain1 f y x
+         indp :  (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 y f y₁) → ZChain1 y f x
          indp x prev with Oprev-p x
          ... | yes op  = sz02 where
              px = Oprev.oprev op
-             zc1 : ZChain1 f y (Oprev.oprev op)
+             zc1 : ZChain1 y f (Oprev.oprev op)
              zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )
-             sz02 : ZChain1 f y x
+             px<x : px o< x
+             px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc 
+             sz02 : ZChain1 y f x
              sz02 with ODC.∋-p O A (* x)
              ... | no noax = record { zc = ? ;  chain-mono = ? ; f-total = ? }
-             ... | yes noax = {!!}
+             ... | yes ax with ODC.p∨¬p O ( HasPrev A (zc zc1 ? ) ax f ) 
+             ... | case1 pr = record { zc = ? ;  chain-mono = ? ; f-total = ? } where
+             ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (zc zc1 ? ) ax )
+             ... | case1 is-sup = ? where -- x is a sup of zc 1
+                sup0 : SUP A (zc zc1 ? ) 
+                sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
+                        x21 :  {y : HOD} → (zc zc1 ?) ∋ 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 
+                x=sup : x ≡ & sp 
+                x=sup = sym &iso 
+                chain0 = zc zc1 ?
+                sc<A : {y : Ordinal} → odef chain0 y ∨ FClosure A f (& sp) y → y o< & A
+                sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< ? )
+                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  }
+             ... | case2 ¬x=sup =  ?
          ... | no  ¬ox  with trio< x y
          ... | tri< a ¬b ¬c = {!!}
          ... | tri≈ ¬a b ¬c = {!!}
          ... | tri> ¬a ¬b y<x = {!!}
 
+     zc1=zc : { f : Ordinal → Ordinal } {y : Ordinal} →  ZChain1  y f (osuc (& A)) → ZChain A y f (& A)
+     zc1=zc = ?
+
      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
@@ -587,13 +611,13 @@
          zorn01  = proj1  zorn03  
          zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
          zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
-     ... | yes ¬Maximal = ⊥-elim ( z04 nmx (ZChain1.zc zc0 <-osuc ) (ZChain1.f-total zc0 <-osuc) ) where
+     ... | yes ¬Maximal = ⊥-elim ( z04 nmx (zc1=zc zc0) (ZChain1.f-total zc0 <-osuc) ) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A 
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
               zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) 
               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) ) ⟫
-         zc0 : ZChain1  (cf nmx) (& s) (osuc (& A))
+         zc0 : ZChain1 (& s) (cf nmx)  (osuc (& A))
          zc0 = SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) (osuc (& A))
 
 -- usage (see filter.agda )