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

changeset 528:8facdd7cc65a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TransitiveClosure with x <= f x is possible
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 20 Apr 2022 01:54:57 +0900
parents 634c4a66cfcf
children 6e94ea146fc1
files src/zorn.agda
diffstat 1 files changed, 17 insertions(+), 59 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Apr 19 11:24:55 2022 +0900
+++ b/src/zorn.agda	Wed Apr 20 01:54:57 2022 +0900
@@ -40,6 +40,9 @@
 
 open HOD
 
+_≤_ : (x y : HOD) → Set (Level.suc n)
+x ≤ y = ( x ≡ y ) ∨ ( x < y )
+
 record Element (A : HOD) : Set (Level.suc n) where
     field
        elm : HOD
@@ -213,7 +216,7 @@
       c-infinite : (y : Ordinal ) → (cy : odef (IChainSet A ax) y  )
           → IChainSup> A (ic→A∋y A ax cy)
 
-open import Data.Nat hiding (_<_) 
+open import Data.Nat hiding (_<_ ; _≤_ ) 
 import Data.Nat.Properties as NP
 open import nat
 
@@ -267,7 +270,7 @@
     IPO : IsPartialOrderSet (InFCSet A ax ifc )
     IPO = ⊆-IsPartialOrderSet record { incl = λ {y} lt → incl (InFCSet⊆A A {x} ax ifc) lt} PO
     B = IChainSet A ax
-    cnext = cinext A ax ifc
+    cnext = {!!} -- cinext A ax ifc
     ct02 : {oy : Ordinal} → (y : Chain B x cnext oy ) → A ∋ * oy 
     ct02 y = incl (IChainSet⊆A {A} ax) (subst (λ k → odef (IChainSet A ax) k) (sym &iso) (ct∈A B x cnext y) ) 
     ct-inject : {ox oy : Ordinal} → (x1 : Chain B x cnext ox ) → (y : Chain B x cnext oy )
@@ -285,7 +288,7 @@
         ct07 :  * ox < * (cnext oy1)
         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
+        ... | yes ay1 = {!!} where -- IsStrictPartialOrder.trans PO {me (ct02 x1) } {me (ct02 y)} {me ct031 } (ct-monotonic x1 y a ) ct011 where
            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 (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) )
@@ -295,7 +298,7 @@
            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
+           ... | yes ay1 = subst (λ k → * k < _) (sym (ct-inject _ _ b)) {!!} where
               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 ) 
@@ -328,9 +331,13 @@
 extendInfiniteChain : (A : HOD) → {x mx y my : Ordinal}  (ax : A ∋ * x) (ay : A ∋ * y)
      → IsPartialOrderSet A 
      → (ifcx : InfiniteChain A mx ax ) → (ifcy : InfiniteChain A my ay )
-     → * mx < * my
-     → InfiniteChain A my ax 
-extendInfiniteChain = ?
+     → * y ≤ * mx
+     → InfiniteChain A (maxα mx my) ax 
+extendInfiniteChain A {x} {mx} {y} {my} ax ay PO ifcx ifcy y<mx = record { chain<x = eic00 ; c-infinite = eic01 } where
+    eic00 : (z : Ordinal) → odef (IChainSet A ax) z → z o< maxα mx my
+    eic00 z xz = {!!}
+    eic01 :  (z : Ordinal) (cy : odef (IChainSet A ax) z) → IChainSup> A (ic→A∋y A ax cy)
+    eic01 z cy = {!!}
       
 record IsFC (A : HOD) {x : Ordinal}  (ax : A ∋ * x) (y : Ordinal) : Set n where
    field
@@ -470,61 +477,12 @@
               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) (  TransitiveClosure-is-total  A {x} ax PO ifc ))
-     z03 : {x : Ordinal } → (ax : A ∋ * x ) → InfiniteChain A (& A)  ax  → ⊥
-     z03 {x}  ax ifc = {!!}
+     -- z03 : {x : Ordinal } → (ax : A ∋ * x ) → InfiniteChain A (& A)  ax  → ⊥
+     -- z03 {x}  ax 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 
-     ind x prev with Oprev-p x
-     ... | yes op with ODC.∋-p O A (* x)
-     ... | no ¬Ax = zc1 where
-          -- we have previous ordinal and ¬ A ∋ x, use previous Zchain
-          px = Oprev.oprev op
-          zc1 : ZChain A x ∨ Maximal A
-          zc1 with prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
-          ... | case2 x = case2 x  -- we have the Maximal
-          ... | case1 z with trio< x (& (ZChain.max z))
-          ... | tri< a ¬b ¬c = case1 record { max = ZChain.max z ; y<max = a }
-          ... | tri≈ ¬a b ¬c = {!!} -- x = max so ¬ A ∋ max 
-          ... | tri> ¬a ¬b c = {!!} -- can't happen
-     ... | yes ax = zc4 where -- we have previous ordinal and A ∋ x
-          px = Oprev.oprev op
-          zc1 : OSup> A (subst (OD.def (od A)) (sym &iso) ax) → ZChain A x ∨ Maximal A
-          zc1 os with  prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
-          ... | case2 x = case2 x
-          ... | case1 x = {!!}
-          zc4 : ZChain A x ∨ Maximal A
-          zc4 with Zorn-lemma-3case 0<A PO x {!!}
-          ... | case1 y>x = zc1 {!!}
-          ... | case2 (case1 x) = case2 x
-          ... | case2 (case2 ex) = ⊥-elim (zc5 {!!} ) where
-              FC : HOD
-              FC = IChainSet A ax
-              B : InfiniteChain A x ax  → HOD
-              B ifc =  InFCSet A ax ifc
-              zc6 :  (ifc : InfiniteChain A x ax ) → ¬ SUP A (B ifc)
-              zc6 = {!!}
-              FC-is-total : (ifc : InfiniteChain A x ax)  → IsTotalOrderSet (B ifc)
-              FC-is-total ifc = TransitiveClosure-is-total A ax PO ifc 
-              B⊆A : (ifc : InfiniteChain A x ax)  →   B ifc ⊆ A
-              B⊆A = {!!}
-              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 : 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
-          zc1 : ZChain A (& A) 
-          zc1 with prev (& A) a 
-          ... | t = {!!}
-     ... | tri≈ ¬a b ¬c = {!!} where
-     ... | tri> ¬a ¬b c with ODC.∋-p O A (* x)
-     ... | no ¬Ax = {!!} where
-     ... | yes ax = {!!}
+     ind x prev = {!!}
      zorn03 : (x : Ordinal) → ZChain A x  ∨ Maximal A 
      zorn03 x = TransFinite ind  x
      zorn04 : Maximal A