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

changeset 738:ffd3bb1a43fe

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 Tue, 19 Jul 2022 17:57:26 +0900
parents 961abb22f2d9
children f92c675c3ef0
files src/zorn.agda
diffstat 1 files changed, 15 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jul 19 15:56:49 2022 +0900
+++ b/src/zorn.agda	Tue Jul 19 17:57:26 2022 +0900
@@ -264,17 +264,19 @@
 
 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u z : Ordinal) : Set n where
    field
-      u>0      : o∅ o< u    -- ¬ ch-init
-      supf=u   : supf u ≡ u  
-      supf-mono  : {a b : Ordinal } → a o≤ b → supf a o≤ supf b
-      supf-<  : {a b : Ordinal } → a o≤ b → (supf a ≡ supf b) ∨ (supf a << supf b)
-      au       : odef A u
-      ¬u=fx    : {x : Ordinal} → ¬ ( u ≡ f x )
-      asup     : (x : Ordinal) → odef A (supf x)
       fcy<sup  : {z : Ordinal } → FClosure A f y z → z << supf u
-      csupz    : FClosure A f (supf u) z 
       order    : {sup1 z1 : Ordinal} → (lt : sup1 o< u ) → FClosure A f (supf sup1 ) z1 → z1 << supf u
 
+      -- u>0      : o∅ o< u    -- ¬ ch-init
+      -- supf=u   : supf u ≡ u  
+      -- supf-mono  : {a b : Ordinal } → a o≤ b → supf a o≤ supf b
+      -- supf-<  : {a b : Ordinal } → a o≤ b → (supf a ≡ supf b) ∨ (supf a << supf b)
+      -- au       : odef A u
+      -- ¬u=fx    : {x : Ordinal} → ¬ ( u ≡ f x )
+      -- asup     : (x : Ordinal) → odef A (supf x)
+      -- csupz    : FClosure A f (supf u) z 
+
+
 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 o∅ z 
     ch-is-sup : {sup z : Ordinal } 
@@ -306,13 +308,13 @@
    chain : HOD
    chain = UnionCF A f mf ay supf z
    field
-      chain<A : {z : Ordinal } → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf (& A) 
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
       sup=u : {b : Ordinal} → (ab : odef A b)  → IsSup A chain ab → supf b ≡ b 
+      -- chain<A : {z : Ordinal } → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf (& A) 
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {init : Ordinal} (ay : odef A init)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
@@ -640,7 +642,8 @@
           -- if previous chain satisfies maximality, we caan reuse it
           --
           no-extension : ZChain A f mf ay x
-          no-extension = record { supf = ZChain.supf (prev px ? ); initial = pinit ; chain∋init = pcy 
+          no-extension = record { supf = ZChain.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))
+               ; initial = pinit ; chain∋init = pcy  ; sup=u = ? 
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
 
           chain-mono : UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) ⊆' pchain
@@ -723,7 +726,7 @@
           pcy = ⟪ ay , record { u =  o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay)  }  ⟫
 
           no-extension : ZChain A f mf ay x
-          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf0 ; chain<A = {!!}
+          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf0 
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
 
           usup : SUP A pchain
@@ -735,19 +738,6 @@
           ... | tri≈ ¬a b ¬c = spu
           ... | tri> ¬a ¬b c = spu
 
-
-          -- chain-mono : pchain ⊆'  UnionCF A f mf ay psupf x  
-          -- chain-mono {a} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ = 
-          --          ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ 
-          -- chain-mono {.(psupf0 u)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (init x) } ⟫ = 
-          --          ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup {!!} {!!} } ⟫ 
-          -- chain-mono {.(f x)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (fsuc x fc) } ⟫ = 
-          --          ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup {!!} (fsuc x {!!}) } ⟫ 
-          
-          -- chain-≡ : UnionCF A f mf ay psupf x ⊆' pchain 
-          --    → UnionCF A f mf ay psupf x ≡ pchain 
-          -- chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
-
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = no-extension -- ¬ A ∋ p, just skip
@@ -755,7 +745,7 @@
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extension  
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; chain<A = {!!}
+          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  
               ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} } where -- x is a sup of (zc ?) 
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x