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

changeset 652:8a4c3d68c6c2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use previous version
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Jun 2022 08:13:53 +0900
parents 18357e4bddba
children
files src/zorn.agda
diffstat 1 files changed, 17 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jun 27 18:17:09 2022 +0900
+++ b/src/zorn.agda	Tue Jun 28 08:13:53 2022 +0900
@@ -246,7 +246,6 @@
 
 record UZFChain ( A : HOD )  ( f : Ordinal → Ordinal ) (x y  : Ordinal) (prev : (z : Ordinal) → z o< x → ZChain A y f z) (z : Ordinal) : Set n where 
    -- Union of ZFChain from y which has maximality o< x
-   inductive
    field
       u : Ordinal
       u<x : u o< x
@@ -554,11 +553,10 @@
          u-chain∋x = case2 ( init ay )
          
      record ZChain1 (y : Ordinal) ( f : Ordinal → Ordinal )  ( z : Ordinal ) : Set (Level.suc n) where
-      inductive
       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 y f z
@@ -572,20 +570,20 @@
              zc1 : ZChain1 y f px
              zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )
              zc0 : ZChain A y f px
-             zc0 = ind f mf ay px (λ w w<px → zc zc1 (o<→≤ w<px) )
+             zc0 = ind f mf ay px (λ w w<px → {!!} )
              px<x : px o< x
              px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc 
-             no-extrention1 : ( {a b : Ordinal} → odef (chain zc0) a → b o< osuc x → (ab : odef A b) →
-                     HasPrev A (chain zc0) ab f ∨  IsSup A (chain zc0) ab →
-                             * a < * b → odef (ZChain.chain zc0) b ) → ZChain1 y f x
-             no-extrention1 imx = record { zc = sz00  ; chain-mono = {!!} ; f-total = {!!}  } where
-                  sz00 : {z : Ordinal} → z o≤ x → ZChain A y f z 
-                  sz00 {z} z≤x = {!!}
+             no-extrention1 : ZChain1 y f x 
+             no-extrention1 = record { zc = ? ; chain-mono = ? ; f-total = ? } where
+                 sz04 : { z : Ordinal } → z o≤ x → HOD
+                 sz04 {z} z≤x with osuc-≡< z≤x
+                 ... | case1 eq = zc zc1 <-osuc 
+                 ... | case2 z<x = zc zc1 (subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x )
              sz02 : ZChain1 y f x
              sz02 with ODC.∋-p O A (* x)
-             ... | no noax = no-extrention1 {!!}
+             ... | no noax = no-extrention1 
              ... | yes ax with ODC.p∨¬p O ( HasPrev A (chain zc0) ax f ) 
-             ... | case1 pr = record { zc = {!!} ;  chain-mono = {!!} ; f-total = {!!} } where
+             ... | case1 pr = no-extrention1
              ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (chain zc0) ax )
              ... | case1 is-sup = {!!} where -- x is a sup of zc 1
                 sup0 : SUP A (chain zc0) 
@@ -604,10 +602,10 @@
                 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  = record { zc = zcu ; chain-mono = sz03 ; f-total = {!!} } where
+             ... | case2 ¬x=sup =  no-extrention1
+         ... | no  ¬ox  = record { zc = {!!}  ; chain-mono = sz03 ; f-total = {!!} } where
               pzc :  (z : Ordinal) → z o< x → ZChain A y f z
-              pzc z z<x = ind f mf ay z (λ w w<px → zc (prev z z<x) (o<→≤ w<px) )
+              pzc z z<x = ind f mf ay z (λ w w<px → {!!} )
               Uz⊆A : {z : Ordinal} → UZFChain A f x y pzc z ∨ FClosure A f y z → odef A z
               Uz⊆A {z} (case1 u) = ZChain.chain⊆A ( pzc (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u)
               Uz⊆A (case2 lt) = A∋fc _ f mf lt 
@@ -623,7 +621,7 @@
               zcu : { z : Ordinal } → z o≤ x → ZChain A y f z
               zcu {z} z≤x with osuc-≡< z≤x                                                                                                                                
               ... | case1 z=x = record { chain = Uz }
-              ... | case2 z<x = ind f mf ay z (λ w w<px → zc (prev z z<x ) (o<→≤ w<px) )
+              ... | case2 z<x = ind f mf ay z (λ w w<px → {!!} )
               sz03 : {a b : Ordinal} → (a≤b : a o≤ b) → (b≤x : b o≤ x ) →  chain (zcu {a} (OrdTrans a≤b b≤x))  ⊆' chain (zcu b≤x ) 
               sz03 {a} {b} a≤b b≤x {i} ai with osuc-≡< (OrdTrans a≤b b≤x) | osuc-≡< b≤x
               ... | case1 a=x | case1 b=x = {!!}
@@ -643,7 +641,7 @@
          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 o≤-refl ) (ZChain1.f-total zc0 o≤-refl ) ) where
+     ... | yes ¬Maximal = ⊥-elim ( z04 nmx {!!} {!!} ) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A 
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where