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

changeset 694:196eff771492

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 Mon, 11 Jul 2022 14:15:17 +0900
parents a3b7f1e0ca60
children 7c0bb8ed7193
files src/zorn.agda
diffstat 1 files changed, 68 insertions(+), 90 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jul 11 11:49:11 2022 +0900
+++ b/src/zorn.agda	Mon Jul 11 14:15:17 2022 +0900
@@ -239,20 +239,6 @@
       A∋maximal : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
--- Union of supf z which o< x
---
-record UChain (x : Ordinal) (chain : (z : Ordinal ) → z o< x → HOD)  (z : Ordinal) : Set n where 
-   field
-      u : Ordinal
-      u<x : u o< x
-      chain∋z : odef (chain u u<x ) z
-
-∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
-∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
-
-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 }
-
 --
 --  sup and its fclosure is in a chain HOD
 --    chain HOD is sorted by sup as Ordinal and <-ordered
@@ -260,30 +246,48 @@
 --    minimum index is y not ϕ 
 --
 
-record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD) (sup z : Ordinal) : Set n where
+record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (sup z : Ordinal) : Set n where
    field
-      asup    : odef A sup
-      fcy<sup  : {z : Ordinal } → FClosure A f y z → z << sup
-      csupz   : odef (chainf sup) z
-      order : {sup1 z1 : Ordinal} → (lt : sup1 o< sup ) → odef (chainf sup1 ) z1 → z1 << sup
+      y-init    : supf o∅  ≡ y
+      asup    : (x : Ordinal) → odef A (supf x)
+      fcy<sup  : {z : Ordinal } → FClosure A f y z → z << supf sup
+      csupz   : FClosure A f (supf sup) z 
+      order : {sup1 z1 : Ordinal} → (lt : sup1 o< sup ) → FClosure A f (supf sup1 ) z1 → z1 << supf sup
+
+data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) : Ordinal →  Ordinal → Set n where
+    ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay supf y z 
+    ch-is-sup : {sup z : Ordinal } 
+         → ( is-sup : ChainP A f mf ay supf sup z)
+         → ( fc : FClosure A f (supf sup) z ) → Chain A f mf ay supf sup z
+
+-- Union of supf z which o< x
+--
 
-data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD) : Ordinal →  Ordinal → Set n where
-    ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay chainf y z 
-    ch-is-sup : {sup z : Ordinal } 
-         → ( is-sup : ChainP A f mf ay chainf sup z)
-         → ( fc : FClosure A f sup z ) → Chain A f mf ay chainf sup z
+record UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
+       (supf : Ordinal → Ordinal) (x : Ordinal)  (z : Ordinal) : Set n where 
+   field
+      u : Ordinal
+      u<x : u o< x
+      chain∋z : Chain A f mf ay supf u z
+
+∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
+∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
+
+UnionCF : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) 
+    ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
+UnionCF A f mf ay supf x
+   = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
    field
-      psup :  Ordinal → Ordinal 
-      p≤z : (x : Ordinal ) →   odef A (psup x)
-      chainf : (x : Ordinal) → HOD
-      is-chain : {x w : Ordinal} → odef (chainf x) w → Chain A f mf ay chainf (psup x) w 
+      supf :  Ordinal → Ordinal 
+      supf-mono : (x y : Ordinal ) → x o≤ y  → supf x o≤ supf y
+      is-chain : {w : Ordinal } → Chain A f mf ay supf z w 
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)  
           (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where
    chain : HOD
-   chain = UnionCF A (& A) ( λ x _ → ZChain1.chainf (zc0 (& A)) x )  
+   chain = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A)
    field
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
@@ -307,39 +311,39 @@
 --
 -- data Chain is total
 
-chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD)
-   {s s1 a b : Ordinal } ( ca : Chain A f mf ay chainf s a ) ( cb : Chain A f mf ay chainf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
-chain-total A f mf {y} ay chainf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
-     ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay chainf xa a → Chain A f mf ay chainf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
+chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
+   {s s1 a b : Ordinal } ( ca : Chain A f mf ay supf s a ) ( cb : Chain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
+chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
+     ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay supf xa a → Chain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
           ct00 : * a < * xb
-          ct00 = ChainP.fcy<sup supb fca
+          ct00 = {!!} -- ChainP.fcy<sup supb fca
           ct01 : * a < * b 
-          ct01 with s≤fc xb f mf fcb 
+          ct01 with s≤fc xb f mf {!!}
           ... | case1 eq =  subst (λ k → * a < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
      ct-ind xa xb {a} {b} (ch-is-sup supa fca) (ch-init b fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
           ct00 : * b < * xa
-          ct00 = ChainP.fcy<sup supa fcb
+          ct00 = {!!} -- ChainP.fcy<sup supa fcb
           ct01 : * b < * a 
-          ct01 with s≤fc xa f mf fca 
+          ct01 with s≤fc xa f mf  {!!}
           ... | case1 eq =  subst (λ k → * b < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
      ct-ind xa xb {a} {b} (ch-is-sup supa fca) (ch-is-sup supb fcb) with trio< xa xb
      ... | tri< a₁ ¬b ¬c = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
           ct03 : * a < * xb
-          ct03 = ChainP.order supb a₁ (ChainP.csupz supa)
+          ct03 = {!!} -- ChainP.order supb a₁ (ChainP.csupz supa)
           ct02 : * a < * b 
-          ct02 with s≤fc xb f mf fcb 
+          ct02 with s≤fc xb f mf {!!} 
           ... | case1 eq =  subst (λ k → * a < k ) eq ct03
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
-     ... | tri≈ ¬a  refl ¬c = fcn-cmp xa f mf fca fcb
+     ... | tri≈ ¬a  refl ¬c = fcn-cmp xa f mf {!!} {!!} 
      ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
           ct05 : * b < * xa
-          ct05 = ChainP.order supa c (ChainP.csupz supb)
+          ct05 = {!!} -- ChainP.order supa c (ChainP.csupz supb)
           ct04 : * b < * a 
-          ct04 with s≤fc xa f mf fca 
+          ct04 with s≤fc xa f mf {!!} 
           ... | case1 eq =  subst (λ k → * b < k ) eq ct05
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct05 lt
 
@@ -480,22 +484,18 @@
           sc : ZChain1 A f mf ay px
           sc = prev px px<x
           pchain : HOD
-          pchain  = chainf sc px 
+          pchain  = {!!}
 
           no-ext :  ZChain1 A f mf ay x
-          no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = ? }  where
+          no-ext = {!!} where -- record { supf = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = ? }  where
             psup1 : Ordinal → Ordinal
             psup1 z with o≤? z x
-            ... | yes _ = ZChain1.psup sc z
-            ... | no _ = ZChain1.psup sc x
-            p≤z1 : (z : Ordinal ) → odef A (psup1 z)
-            p≤z1 z with o≤? z x
-            ... | yes _  = ZChain1.p≤z sc z
-            ... | no _  = ZChain1.p≤z sc x
+            ... | yes _ = ZChain1.supf sc z
+            ... | no _ = ZChain1.supf sc x
             chainf1 : (z : Ordinal ) → HOD
             chainf1 z with o≤? z x
-            ... | yes _  = ZChain1.chainf sc z 
-            ... | no _ = ZChain1.chainf sc x 
+            ... | yes _  = {!!}
+            ... | no _ = {!!}
             is-chain1 : {!!}
             is-chain1 = {!!}
           sc4 : ZChain1 A f mf ay x
@@ -504,70 +504,48 @@
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
           ... | case1 pr = no-ext
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { psup = {!!} ; p≤z = {!!} ; chainf = {!!} ; is-chain = {!!} } where
+          ... | case1 is-sup = record { supf = {!!} ; p≤z = {!!} ; chainf = {!!} ; is-chain = {!!} } where
                 schain : HOD
                 schain = {!!} -- record { od = record { def = λ z → odef A z ∧ ( odef (ZChain1.chain sc ) z ∨ (FClosure A f x z)) } 
                     -- ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
           ... | case2 ¬x=sup = no-ext
      ... | no ¬ox = sc4 where
           pchainf : (z : Ordinal) → z o< x → HOD
-          pchainf z z<x = ZChain1.chainf (prev z z<x) z  
+          pchainf z z<x = {!!} -- Chain1.chainf (prev z z<x) z  
           pzc : (z : Ordinal) → z o< x → ZChain1 A f mf ay z
           pzc z z<x = prev z z<x
           UZ : HOD
-          UZ = UnionCF A x pchainf
+          UZ = {!!} -- UnionCF A x pchainf
           chainf0 : (z : Ordinal ) → HOD
           chainf0 z with trio< z x
-          ... | tri< a ¬b ¬c = ZChain1.chainf (pzc z a) z
+          ... | tri< a ¬b ¬c = {!!} -- ZChain1.chainf (pzc z a) z
           ... | tri≈ ¬a b ¬c = UZ
           ... | tri> ¬a ¬b c = UZ
-          Chain-ext : {s a : Ordinal}  → (ca : odef UZ a)
-             → Chain A f mf ay ( ZChain1.chainf (pzc _ (UChain.u<x (proj2 ca)))) s a → Chain A f mf ay chainf0 s a 
-          Chain-ext {s} {a} ca (ch-init a x) = ch-init a x
-          Chain-ext {s} {a} ca (ch-is-sup is-sup fc) = ch-is-sup sc5 fc where
-              sc7 : odef ( ZChain1.chainf (pzc _ (UChain.u<x (proj2 ca))) s ) a
-              sc7 = ChainP.csupz is-sup
-              sc8  : (z<x : s o< x ) → chainf0 s ≡ ( ZChain1.chainf (pzc _ z<x )) s
-              sc8  z<x with  trio< s x
-              ... | tri≈ ¬a b ¬c = ?
-              ... | tri> ¬a ¬b c = ?
-              ... | tri< a ¬b ¬c with o<-irr a z<x 
-              ... | refl = refl 
-              sc6 : odef (chainf0 s) a
-              sc6 with trio< s x 
-              ... | tri≈ ¬a b ¬c = ?
-              ... | tri> ¬a ¬b c = ?
-              ... | tri< a' ¬b ¬c with o<-irr a' ? -- (UChain.u<x (proj2 ca))
-              ... | eq = ? -- ChainP.csupz is-sup 
-              sc5 : ChainP A f mf ay chainf0 s a
-              sc5 = record {
-                  asup = ChainP.asup is-sup
-                ; fcy<sup = ChainP.fcy<sup is-sup
-                ; csupz = sc6
-                ; order = ? }
+          Chain-ext : {!!}
+          Chain-ext = {!!}
           total-UZ : IsTotalOrderSet UZ
           total-UZ {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay chainf0  
+               uz01 = chain-total A f mf ay {!!}
                    (Chain-ext ca (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) (UChain.chain∋z (proj2 ca)))) 
                    (Chain-ext cb (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) (UChain.chain∋z (proj2 cb)))) 
           usup : SUP A UZ
           usup = supP UZ (λ lt → proj1 lt) total-UZ 
           spu = & (SUP.sup usup)
           sc4 :  ZChain1 A f mf ay x
-          sc4 = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = {!!} }  where
+          sc4 = record { supf = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = {!!} }  where
             psup1 : Ordinal → Ordinal
             psup1 z with o≤? x z
             ... | yes _ = spu
-            ... | no z<x = ZChain1.psup (pzc z (o¬≤→< z<x)) z
+            ... | no z<x = ZChain1.supf (pzc z (o¬≤→< z<x)) z
             p≤z1 : (z : Ordinal ) → odef A (psup1 z)
             p≤z1 z with o≤? x z
             ... | yes _  = SUP.A∋maximal usup
-            ... | no z<x  = ZChain1.p≤z (pzc z (o¬≤→< z<x)) z
+            ... | no z<x  = {!!} -- ZChain1.p≤z (pzc z (o¬≤→< z<x)) z
             chainf1 : (z : Ordinal ) → HOD
             chainf1 z with o≤? x z
             ... | yes _  = record { od = record { def = λ w → odef A w ∧ FClosure A f spu w  } ; odmax = & A ; <odmax = {!!} }
-            ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z
+            ... | no z<x = {!!} -- ZChain1.chainf (pzc z (o¬≤→< z<x)) z
             is-chain1 : (z w : Ordinal) → odef (chainf1 z) w → Chain A f mf ay {!!} (psup1 z ) w
             is-chain1 z w lt with o≤? x z
             ... | no z<x = {!!} -- ZChain1.is-chain (pzc z (o¬≤→< z<x)) z w ? ?
@@ -737,13 +715,13 @@
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup {!!} )  } ) 
      ... | no op = zc5 where
           supf : (z : Ordinal ) → z o< x  → HOD
-          supf x lt = ZChain1.chainf ( zc0  (& A) ) x 
-          uzc : {z : Ordinal} → (u : UChain x supf z) → ZChain A f mf ay zc0 (UChain.u u)
+          supf x lt = {!!} -- ZChain1.chainf ( zc0  (& A) ) x 
+          uzc : {!!} -- {z : Ordinal} → (u : UChain x supf z) → ZChain A f mf ay zc0 (UChain.u u)
           uzc {z} u =  prev (UChain.u u) (UChain.u<x u) 
           Uz : HOD
-          Uz = record { od = record { def = λ z → odef A z ∧ ( UChain x supf z ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!}  }
-          Uzchain : ¬ (odef (ZChain1.chainf (zc0 (& A) ) x) x) → ZChain A f mf ay zc0 x
-          Uzchain nz = record { chain-mono = {!!}  ; chain⊆A = {!!} ; chain∋init = {!!} ; initial = {!!} ; f-next = {!!} ; f-total = {!!} ; is-max = {!!} }
+          Uz = {!!} -- record { od = record { def = λ z → odef A z ∧ ( UChain x supf z ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!}  }
+          -- Uzchain : ¬ (odef (ZChain1.chainf (zc0 (& A) ) x) x) → ZChain A f mf ay zc0 x
+          -- Uzchain nz = record { chain-mono = {!!}  ; chain⊆A = {!!} ; chain∋init = {!!} ; initial = {!!} ; f-next = {!!} ; f-total = {!!} ; is-max = {!!} }
           zc5 : ZChain A f mf ay zc0 x 
           zc5 with o≤? x o∅
           ... | yes x=0 = {!!}