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

changeset 668:f40388701930

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
new data Chain
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 05 Jul 2022 05:10:27 +0900
parents c6cd972b468c
children 7d227d624aad
files src/zorn.agda
diffstat 1 files changed, 22 insertions(+), 91 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jul 04 21:58:07 2022 +0900
+++ b/src/zorn.agda	Tue Jul 05 05:10:27 2022 +0900
@@ -253,41 +253,16 @@
 UnionCF : (A : HOD) (x : Ordinal) (chainf : (z : Ordinal ) → z o< x → HOD ) → HOD
 UnionCF A x chainf = record { od = record { def = λ z → odef A z ∧ UChain x chainf z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
-data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) : Ordinal →  HOD  → Set (Level.suc n) where
-    ch-init    : (x : Ordinal) → x ≡ o∅ → Chain A f mf  ay x  record { od = record { def = λ z → FClosure A f y z  } ; odmax = & A ; <odmax = λ {y} sy → ? }
-    ch-noax    : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (noax : ¬ odef A x ) (c : Chain A f mf  ay (Oprev.oprev op) chain) → Chain A f mf  ay x chain
-    ch-hasprev : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (ax : odef A x ) 
-        ( c : Chain A f mf ay (Oprev.oprev op) chain) ( h :  HasPrev A chain ax f ) → Chain A f mf ay x chain
-    ch-is-sup : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x ) 
-        ( c : Chain A f mf ay (Oprev.oprev op) chain) ( nh :  ¬ HasPrev A chain  ax f ) ( sup : IsSup A chain   ax ) → Chain A f mf ay x 
-            record { od = record { def = λ z → odef A z ∧ (odef chain z ∨ (FClosure A f x z)) } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
-    ch-skip : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x ) 
-        ( c : Chain A f mf ay (Oprev.oprev op) chain) ( nh : ¬  HasPrev A chain ax f ) ( nsup : ¬ IsSup A chain ax ) → Chain A f mf ay x chain
-    ch-noax-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( noax : ¬ odef A x ) 
-         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x ))
-         → Chain A f mf ay x (UnionCF A x chainf )
-    ch-hasprev-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x ) 
-         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x ))
-         → ( h :   HasPrev A (UnionCF A x chainf)  ax f ) 
-         → Chain A f mf ay x (UnionCF A x chainf )
-    ch-is-sup-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x ) 
-         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x ))
-         →  ( nh :  ¬ HasPrev A (UnionCF A x chainf) ax f ) ( sup : IsSup A (UnionCF A x chainf) ax ) 
-         → Chain A f mf ay x 
-             record { od = record { def = λ z → odef A z ∧ (UChain x chainf z ∨ FClosure A f x z ) } 
-                ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
-    ch-skip-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x ) 
-         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x ))
-         →  (nh : ¬ HasPrev A (UnionCF A x chainf) ax f ) (nsup :  ¬ IsSup A (UnionCF A x chainf) ax ) 
-         → Chain A f mf ay x (UnionCF A x chainf) 
-
-ChainF : (A : HOD) →  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) → (chain : HOD ) → Chain A f mf ay (& A) chain → (x : Ordinal) → x o< & A →  HOD
-ChainF A f mf {y} ay chain Ch x x<a = {!!}
+data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) : Ordinal →  Ordinal → Set n where
+    ch-init    : (x z : Ordinal) → x ≡ o∅ → FClosure A f y z  → Chain A f mf  ay x z 
+    ch-is-sup : {x z : Ordinal }  ( ax : odef A x ) 
+         → ( is-sup : (x1 w : Ordinal) → x1 o< x → Chain A f mf ay x1 w → w << x )  → ( fc : FClosure A f x z ) → Chain A f mf ay x z
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) ( z : Ordinal )  : Set (Level.suc n) where
+   chain : HOD
+   chain = record { od = record { def = λ x →  Chain A f mf ay z x } ; odmax = (& A) ; <odmax = ? }
    field
-      chain : HOD
-      chain-uniq : Chain A f mf ay z chain 
+      chainf : (w : Ordinal) → Chain A f mf ay z w 
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
@@ -432,53 +407,6 @@
      -- create all ZChains under o< x
      --
 
-     sind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
-         → ((z : Ordinal) → z o< x → ZChain A f mf ay z ) → ZChain A f mf ay x
-     sind f mf {y} ay x prev  with Oprev-p x
-     ... | yes op = sc4 where
-          open ZChain
-          px = Oprev.oprev op
-          px<x : px o< x
-          px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc 
-          sc : ZChain A f mf ay px 
-          sc = prev px px<x
-          sc4 : ZChain A f mf ay x 
-          sc4 with ODC.∋-p O A (* x)
-          ... | no noax =  record { chain = ? ; chain-uniq = ch-noax op (subst (λ k → ¬ odef A k) &iso noax) ( chain-uniq sc )  }  
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain sc ) ax f )   
-          ... | case1 pr = record { chain = chain sc ; chain-uniq = ch-hasprev op (subst (λ k → odef A k) &iso ax) ( chain-uniq sc ) 
-                                       record { y = HasPrev.y pr  ; ay = HasPrev.ay pr  ; x=fy = sc6 } }  where
-                sc6 : x ≡ f (HasPrev.y pr)
-                sc6 = subst (λ k → k ≡ f (HasPrev.y pr) ) &iso  ( HasPrev.x=fy pr  )
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain sc ) ax )
-          ... | case1 is-sup =  record { chain = schain ; chain-uniq = sc9 }  where
-                schain : HOD
-                schain = record { od = record { def = λ z → odef A z ∧ ( odef (ZChain.chain sc ) z ∨ (FClosure A f x z)) } 
-                    ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
-                sc7 : ¬ HasPrev A (chain sc) (subst (λ k → odef A k) &iso ax) f
-                sc7 not = ¬fy<x record { y = HasPrev.y not ; ay = HasPrev.ay not ; x=fy = subst (λ k → k ≡ _) (sym &iso) (HasPrev.x=fy not ) }
-                sc9 : Chain A f mf ay x schain
-                sc9 = ch-is-sup op (subst (λ k → odef A k) &iso ax) (ZChain.chain-uniq sc) sc7
-                    record { x<sup = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k )) &iso (IsSup.x<sup is-sup lt) }
-          ... | case2 ¬x=sup = record { chain = chain sc ; chain-uniq = ch-skip op (subst (λ k → odef A k) &iso ax) (ZChain.chain-uniq sc) sc17 sc10 }  where
-                sc17 : ¬ HasPrev A (chain sc) (subst (λ k → odef A k) &iso ax) f
-                sc17 not = ¬fy<x record { y = HasPrev.y not ; ay = HasPrev.ay not ; x=fy = subst (λ k → k ≡ _) (sym &iso) (HasPrev.x=fy not ) }
-                sc10 : ¬ IsSup A (chain sc) (subst (λ k → odef A k) &iso ax)
-                sc10 not = ¬x=sup ( record { x<sup  = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k ) ) (sym &iso) ( IsSup.x<sup not lt ) }  )
-     ... | no ¬ox = sc4 where
-          chainf : (z : Ordinal) → z o< x → HOD
-          chainf z z<x = ZChain.chain ( prev z z<x  )
-          chainq : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x )
-          chainq z z<x = ZChain.chain-uniq (  prev z z<x )
-          sc4 : ZChain A f mf ay x 
-          sc4 with ODC.∋-p O A (* x)
-          ... | no noax =  record { chain = UnionCF A x chainf ; chain-uniq = ch-noax-union ¬ox (subst (λ k → ¬ odef A k) &iso noax) ? ? }  
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (UnionCF A x chainf) ax f )   
-          ... | case1 pr = record { chain = UnionCF A x chainf  ; chain-uniq = ch-hasprev-union ¬ox (subst (λ k → odef A k) &iso ax) ? ? ? } 
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (UnionCF A x chainf) ax )
-          ... | case1 is-sup = ?
-          ... | case2 ¬x=sup = ?
-
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
          → ((z : Ordinal) → z o< x →  ZChain A f mf ay z ) → ZChain A f mf ay x 
      ind f mf {y} ay x prev with Oprev-p x
@@ -631,8 +559,15 @@
      ... | no ¬ox = zc5 where --- limit ordinal case
           -- chainf : (zc : ZChain1 A f mf ay x ) → (z : Ordinal) → z o< x → HOD
           -- chainf zc z z<x = ?
+          -- chainf : (z : Ordinal) → z o< x → HOD
+          -- chainf z z<x = ZChain.chain ( prev z z<x  )
+          -- chainq : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x )
+          -- chainq z z<x = ZChain.chain-uniq (  prev z z<x )
           uzc : HOD
           uzc = UnionCF A x ? 
+          -- c-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → (w<x : w o< x ) → chainf z ? ⊆' chainf w w<x
+          -- c-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
+          -- ... | s | t = {!!}
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = ? where -- ¬ A ∋ p, just skip
@@ -644,25 +579,21 @@
               -- chainf0 : (zc : ZChain1 A f mf ay x ) → (z : Ordinal) → z o< x → HOD
               -- chainf0 zc z z<x with ZChain1.chain-uniq zc0
               -- ... | t = ?
-              supf : Ordinal → HOD
-              supf x = ? -- ZChain1.chain zc0 
-              Uz : HOD
-              Uz = UnionCF A x ?
-              u-next : {z : Ordinal} → odef Uz z → odef Uz (f z)
-              u-next {z} = {!!}
+              -- u-next : {z : Ordinal} → odef uzc z → odef Uz (f z)
+              -- u-next {z} = {!!}
               -- (case1 u) = case1 record { u = UChain.u u ; u<x = UChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UChain.chain∋z u)  }
               -- u-next {z} (case2 u) = case2 ( fsuc _ u )
-              u-initial :  {z : Ordinal} → odef Uz z → * y ≤ * z 
-              u-initial {z} = {!!}
+              -- u-initial :  {z : Ordinal} → odef Uz z → * y ≤ * z 
+              -- u-initial {z} = {!!}
               -- (case1 u) = ZChain.initial ( uzc u )  (UChain.chain∋z u)
               -- u-initial {z} (case2 u) = s≤fc _ f mf u
-              u-chain∋init :  odef Uz y
-              u-chain∋init = {!!} -- case2 ( init ay )
+              -- u-chain∋init :  odef Uz y
+              -- u-chain∋init = {!!} -- case2 ( init ay )
               supf0 : Ordinal → HOD
               supf0 z with trio< z x
               ... | tri< a ¬b ¬c = ? --  ZChain1.chain zc0 
-              ... | tri≈ ¬a b ¬c = Uz 
-              ... | tri> ¬a ¬b c = Uz
+              ... | tri≈ ¬a b ¬c = ? -- Uz 
+              ... | tri> ¬a ¬b c = ? -- Uz
               u-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w
               u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
               ... | s | t = {!!}