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

changeset 525:dea970e4526e

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, 18 Apr 2022 11:09:52 +0900
parents c02c82656063
children 7e59e0aeaa73
files src/zorn.agda
diffstat 1 files changed, 39 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Apr 18 01:33:07 2022 +0900
+++ b/src/zorn.agda	Mon Apr 18 11:09:52 2022 +0900
@@ -173,7 +173,7 @@
 ic→A∋y : (A : HOD) {x y : Ordinal}  (ax : A ∋ * x) → odef (IChainSet A ax) y → A ∋ * y
 ic→A∋y A {x} {y} ax ⟪ ay , _ ⟫ = subst (λ k → odef A k) (sym &iso) ay
 
-record InFiniteIChain (A : HOD) (max : Ordinal) {x : Ordinal}  (ax : A ∋ * x) : Set n where
+record InfiniteChain (A : HOD) (max : Ordinal) {x : Ordinal}  (ax : A ∋ * x) : Set n where
    field
       chain<x : (y : Ordinal ) → odef (IChainSet A ax) y →  y o< max
       c-infinite : (y : Ordinal ) → (cy : odef (IChainSet A ax) y  )
@@ -205,22 +205,28 @@
 cton : (A : HOD ) (s : Ordinal)   → (next : Ordinal → Ordinal ) → Element (ChainClosure A s next) → ℕ
 cton A s next y = cton0 A s next (is-elm y)
 
-cinext :  (A : HOD) {x max : Ordinal } → (ax : A ∋ * x ) → (ifc : InFiniteIChain A max ax ) → Ordinal  →  Ordinal
+cinext :  (A : HOD) {x max : Ordinal } → (ax : A ∋ * x ) → (ifc : InfiniteChain A max ax ) → Ordinal  →  Ordinal
 cinext A ax ifc y with ODC.∋-p O (IChainSet A ax) (* y)
-... | yes ics-y = IChainSup>.y ( InFiniteIChain.c-infinite ifc y (subst (λ k → odef (IChainSet A ax) k) &iso ics-y ))
+... | yes ics-y = IChainSup>.y ( InfiniteChain.c-infinite ifc y (subst (λ k → odef (IChainSet A ax) k) &iso ics-y ))
 ... | no _ = o∅
 
 InFCSet : (A : HOD) → {x max : Ordinal}  (ax : A ∋ * x)
-     → (ifc : InFiniteIChain A max ax ) → HOD
+     → (ifc : InfiniteChain A max ax ) → HOD
 InFCSet A {x} ax ifc =  ChainClosure (IChainSet A ax) x (cinext A ax ifc ) 
 
-InFCSet⊆A : (A : HOD) → {x max : Ordinal}  (ax : A ∋ * x) →  (ifc : InFiniteIChain A max ax ) → InFCSet A ax ifc ⊆ A
+InFCSet⊆A : (A : HOD) → {x max : Ordinal}  (ax : A ∋ * x) →  (ifc : InfiniteChain A max ax ) → InFCSet A ax ifc ⊆ A
 InFCSet⊆A A {x} ax ifc = record { incl = λ {y} lt → incl (IChainSet⊆A ax) (
      ct∈A (IChainSet A ax) x (cinext A ax ifc) lt ) }
 
+cinext→IChainSup :  (A : HOD) {x max : Ordinal } → (ax : A ∋ * x ) → (ifc : InfiniteChain A max ax ) → (y : Ordinal )
+    → (ay1 : IChainSet A ax ∋ * y ) → IChainSup> A (subst (odef A) (sym &iso) (proj1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1)))
+cinext→IChainSup A {x} ax ifc y ay with ODC.∋-p O (IChainSet A ax) (* y)
+... | no not = ⊥-elim ( not ay )
+... | yes ay1 = InfiniteChain.c-infinite ifc y (subst (λ k → odef (IChainSet A ax) k) &iso ay )
+
 ChainClosure-is-total : (A : HOD) → {x max : Ordinal}  (ax : A ∋ * x)
      → IsPartialOrderSet A 
-     → (ifc : InFiniteIChain A max ax )
+     → (ifc : InfiniteChain A max ax )
      → IsTotalOrderSet ( InFCSet A ax ifc )
 ChainClosure-is-total A {x} ax PO ifc = record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO
    ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}  ; compare = cmp } where
@@ -246,18 +252,18 @@
         ct07 with ODC.∋-p O (IChainSet A ax) (* oy1)
         ... | no not  = ⊥-elim ( not (subst (λ k → odef (IChainSet A ax) k ) (sym &iso) ay ) )
         ... | yes ay1 = IsStrictPartialOrder.trans PO {me (ct02 x1) } {me (ct02 y)} {me ct031 } (ct-monotonic x1 y a ) ct011 where
-           ct031 :  A ∋ * (IChainSup>.y (InFiniteIChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 ) )) 
+           ct031 :  A ∋ * (IChainSup>.y (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 ) )) 
            ct031 = subst (λ k → odef A k ) (sym &iso) (
-              IChainSup>.A∋y (InFiniteIChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) )
-           ct011 :  * oy1 < * ( IChainSup>.y (InFiniteIChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) )
-           ct011 = IChainSup>.y>x (InFiniteIChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) 
+              IChainSup>.A∋y (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) )
+           ct011 :  * oy1 < * ( IChainSup>.y (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) )
+           ct011 = IChainSup>.y>x (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) 
     ... | tri≈ ¬a b ¬c = ct11 where
            ct11 : * ox < * (cnext oy1)
            ct11 with ODC.∋-p O (IChainSet A ax) (* oy1)
            ... | no not  = ⊥-elim ( not (subst (λ k → odef (IChainSet A ax) k ) (sym &iso) ay ) )
            ... | yes ay1 = subst (λ k → * k < _) (sym (ct-inject _ _ b)) ct011  where
-              ct011 :  * oy1 < * ( IChainSup>.y (InFiniteIChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) )
-              ct011 = IChainSup>.y>x (InFiniteIChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) 
+              ct011 :  * oy1 < * ( IChainSup>.y (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) )
+              ct011 = IChainSup>.y>x (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) 
     ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> lt c ) 
     ct12 : {y z : Element (ChainClosure B x cnext) } → elm y ≡ elm z → elm y < elm z → ⊥ 
     ct12 {y} {z} y=z y<z = IsStrictPartialOrder.irrefl IPO {y} {z} y=z y<z
@@ -307,7 +313,7 @@
 Zorn-lemma-3case : { A : HOD } 
     → o∅ o< & A 
     → IsPartialOrderSet A 
-    → (x : Ordinal ) → (ax : odef A x)  → OSup> A (d→∋ A ax) ∨ Maximal A ∨ InFiniteIChain A x  (d→∋ A ax)
+    → (x : Ordinal ) → (ax : odef A x)  → OSup> A (d→∋ A ax) ∨ Maximal A ∨ InfiniteChain A x  (d→∋ A ax)
 Zorn-lemma-3case {A}  0<A PO x ax = zc2 where
     Gtx : HOD
     Gtx = record { od = record { def = λ y → odef ( IChainSet A ax ) y ∧  ( x o< y ) } ; odmax = & A
@@ -315,7 +321,7 @@
     HG : HOD
     HG = record { od = record { def = λ y → odef A y ∧ IsFC A (d→∋ A ax ) y } ; odmax = & A
         ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (d→∋  A  (proj1 lt) ))  }
-    zc2 :  OSup> A (d→∋ A ax)  ∨ Maximal A ∨ InFiniteIChain A x  (d→∋ A ax )
+    zc2 :  OSup> A (d→∋ A ax)  ∨ Maximal A ∨ InfiniteChain A x  (d→∋ A ax )
     zc2 with  is-o∅ (& Gtx)
     ... | no not = case1 record { y = & y ; icy = zc4 ; y>x = proj2 zc3 } where
         y : HOD
@@ -369,7 +375,7 @@
 all-climb-case : { A : HOD } → (0<A : o∅ o< & A) → IsPartialOrderSet A
      → (( x : Ordinal ) → (ax : odef A (& (* x))) → OSup> A ax )
      → (x : HOD) ( ax : A ∋ x )
-     → InFiniteIChain A (& A) (d→∋ A ax)
+     → InfiniteChain A (& A) (d→∋ A ax)
 all-climb-case {A} 0<A PO climb x ax = record {    c-infinite = ac00 ; chain<x = ac01 }  where
         B = IChainSet A ax
         ac01 : (y : Ordinal) → odef (IChainSet A (d→∋ A ax)) y → y o< & A 
@@ -406,22 +412,24 @@
           (IsStrictPartialOrder.trans PO {me A∋b} {me A∋a} {me A∋b}  b<a a<b)
      s = ODC.minimal O A (λ eq → ¬x<0 (subst (_o<_ o∅) (=od∅→≡o∅ eq) 0<A))
      sa = ODC.x∋minimal O A (λ eq → ¬x<0 (subst (_o<_ o∅) (=od∅→≡o∅ eq) 0<A))
-     z02 : {x max : Ordinal } → (ax : A ∋ * x ) → InFiniteIChain A max ax  → ⊥
+     z02 : {x max : Ordinal } → (ax : A ∋ * x ) → InfiniteChain A max ax  → ⊥
      z02 {x} {max} ax ifc = zc5 ifc where
           FC : HOD
           FC = IChainSet A ax
-          zc6 :  InFiniteIChain A max ax  → ¬ SUP A (InFCSet A ax ifc) 
-          zc6 inf sup = z01 nxa (SUP.A∋maximal sup) (SUP.x<sup sup {!!} ) {!!} where
+          zc6 : (ifc : InfiniteChain A max ax)  → ¬ SUP A (InFCSet A ax ifc) 
+          zc6 ifc sup = z01 nxa (SUP.A∋maximal sup) (SUP.x<sup sup {!!} ) {!!} where
               nx : Ordinal
               nx = cinext A ax ifc (& (SUP.sup sup))
+              zc7 : A ∋ * (& (SUP.sup sup))
+              zc7 = subst (λ k → odef A k ) (cong (&) (sym *iso)) (SUP.A∋maximal sup)
+              sup-ics :  odef (IChainSet A ax) (& (SUP.sup sup))
+              sup-ics = ? -- SUP.A∋maximal sup
+              ncsup : (z : Ordinal) → (az : odef (IChainSet A ax) z)  → IChainSup> A {z} (subst (odef A) (sym &iso) (proj1 az)) 
+              ncsup z az = InfiniteChain.c-infinite ifc z az
               nxa : A ∋ * nx
-              nxa = {!!}
-          fct : IsTotalOrderSet (InFCSet A ax ifc)
-          fct = ChainClosure-is-total  A {x} ax PO ifc
-          FC⊆A :  InFCSet A ax ifc ⊆ A
-          FC⊆A = InFCSet⊆A A {x} ax ifc
-          zc5 : InFiniteIChain A max ax → ⊥
-          zc5 ic = zc6 ic ( supP (InFCSet A ax ifc) FC⊆A fct )
+              nxa = {!!} -- cinext∈A A ax ifc (& (SUP.sup sup)) {!!}
+          zc5 : InfiniteChain A max ax → ⊥
+          zc5 ifc = zc6 ifc ( supP (InFCSet A ax ifc) (InFCSet⊆A A {x} ax ifc) (  ChainClosure-is-total  A {x} ax PO ifc ))
      -- ZChain is not compatible with the SUP condition
      ind : (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y ∨ Maximal A )
          →  ZChain A x ∨ Maximal A 
@@ -450,21 +458,21 @@
           ... | case2 (case2 ex) = ⊥-elim (zc5 {!!} ) where
               FC : HOD
               FC = IChainSet A ax
-              B : InFiniteIChain A x ax  → HOD
+              B : InfiniteChain A x ax  → HOD
               B ifc =  InFCSet A ax ifc
-              zc6 :  (ifc : InFiniteIChain A x ax ) → ¬ SUP A (B ifc)
+              zc6 :  (ifc : InfiniteChain A x ax ) → ¬ SUP A (B ifc)
               zc6 = {!!}
-              FC-is-total : (ifc : InFiniteIChain A x ax)  → IsTotalOrderSet (B ifc)
+              FC-is-total : (ifc : InfiniteChain A x ax)  → IsTotalOrderSet (B ifc)
               FC-is-total ifc = ChainClosure-is-total A ax PO ifc 
-              B⊆A : (ifc : InFiniteIChain A x ax)  →   B ifc ⊆ A
+              B⊆A : (ifc : InfiniteChain A x ax)  →   B ifc ⊆ A
               B⊆A = {!!}
-              ifc : InFiniteIChain A x (subst (OD.def (od A)) (sym &iso) ax) → InFiniteIChain A x ax
+              ifc : InfiniteChain A x (subst (OD.def (od A)) (sym &iso) ax) → InfiniteChain A x ax
               ifc record {  c-infinite = c-infinite } = record {  c-infinite = {!!} }  where
                   ifc01 : {!!} -- me (subst (OD.def (od A)) (sym &iso) ax)
                   ifc01 = {!!}
                -- (y : Ordinal) → odef (IChainSet (me (subst (OD.def (od A)) (sym &iso) ax))) y → y o< & (* x₁)
                --  (y : Ordinal) → odef (IChainSet (me ax)) y → y o< x₁
-              zc5 : InFiniteIChain A x (subst (OD.def (od A)) (sym &iso) ax) → ⊥
+              zc5 : InfiniteChain A x (subst (OD.def (od A)) (sym &iso) ax) → ⊥
               zc5 x = zc6 (ifc x) ( supP (B (ifc x)) (B⊆A (ifc x)) (FC-is-total (ifc x) ))
      ind x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
      ... | tri< a ¬b ¬c = {!!} where