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

changeset 565:111d3b641177

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 Sun, 01 May 2022 01:17:54 +0900
parents b8eb708dec3c
children a64dad8d2e93
files src/zorn.agda
diffstat 1 files changed, 28 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Apr 30 17:30:20 2022 +0900
+++ b/src/zorn.agda	Sun May 01 01:17:54 2022 +0900
@@ -242,7 +242,7 @@
       f-total : IsTotalOrderSet chain 
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
-      is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< z  → (ba : odef A b) 
+      is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ba : odef A b) 
           → Prev< A chain ba f
                ∨  (sup (& chain) (subst (λ k → k  ⊆ A) (sym *iso) chain⊆A)  (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b )
           → * a < * b  → odef chain b
@@ -316,7 +316,7 @@
      z03 f mf zc = z14 where
            chain = ZChain.chain zc
            sp1 = sp0 f mf zc
-           z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) 
+           z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) 
               →  Prev< A chain ab f
                    ∨  (supO (& chain) (subst (λ k → k  ⊆ A) (sym *iso) (ZChain.chain⊆A zc))  (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc)) ≡ b )
               → * a < * b  → odef chain b
@@ -326,7 +326,7 @@
            z12 : odef chain (& (SUP.sup sp1))
            z12 with o≡? (& s) (& (SUP.sup sp1))
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋x zc )
-           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) z11 (SUP.A∋maximal sp1)  (case2 refl ) z13 where
+           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) (ordtrans z11 <-osuc ) (SUP.A∋maximal sp1)  (case2 refl ) z13 where
                z13 :  * (& s) < * (& (SUP.sup sp1))
                z13 with SUP.x<sup sp1 (subst (λ k → odef k (& s)) (sym *iso) ( ZChain.chain∋x zc ))
                ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
@@ -374,30 +374,30 @@
           zc0 : ZChain A ay f mf supO (Oprev.oprev op)
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay
           zc4 : ZChain A ay f mf supO x 
-          zc4 with ODC.∋-p O A (* px)
-          ... | no noapx =  -- ¬ A ∋ px, just skip
+          zc4 with ODC.∋-p O A (* x)
+          ... | no noapx =  -- ¬ A ∋ p, just skip
                  record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 
                      ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
                      ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 }  where -- no extention
-                zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< x → (ba : odef A b) →
+                zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ba : odef A b) →
                     Prev< A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (* (& (ZChain.chain zc0)))
                        (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0))
                        (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)))) ≡ b) →
                             * a < * b → odef (ZChain.chain zc0) b
-                zc11 {a} {b} za b<x ba P a<b with osuc-≡< (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) b<x) 
-                ... | case1 eq = ⊥-elim ( noapx (subst (λ k → odef A k) (trans eq (sym &iso) ) ba ))
-                ... | case2 lt = ZChain.is-max zc0 za lt ba P a<b
-          ... | yes apx with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) apx f )   -- we have to check adding x preserve is-max ZChain A ay f mf supO px
+                zc11 {a} {b} za b<ox ba P a<b with osuc-≡< b<ox
+                ... | case1 eq = ⊥-elim ( noapx (subst (λ k → odef A k) (trans eq (sym &iso)) ba ) )
+                ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt )  ba P a<b
+          ... | yes apx with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) apx f )   -- we have to check adding x preserve is-max ZChain A ay f mf supO x
           ... | case1 pr = zc9 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
                 chain = ZChain.chain zc0
-                zc17 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< x → (ba : odef A b) →
+                zc17 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ba : odef A b) →
                             Prev< A (ZChain.chain zc0) ba f ∨ (supO (& (ZChain.chain zc0))
                              (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0))
                              (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)) ≡ b) →
                             * a < * b → odef (ZChain.chain zc0) b
-                zc17 {a} {b} za b<x ba P a<b with osuc-≡< (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) b<x) 
-                ... | case2 lt = ZChain.is-max zc0 za lt ba P a<b
-                ... | case1 b=px = subst (λ k → odef chain k ) (trans (sym (Prev<.x=fy pr )) (trans &iso (sym b=px))) ( ZChain.f-next zc0 (Prev<.ay pr))
+                zc17 {a} {b} za b<ox ba P a<b with osuc-≡< b<ox
+                ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt) ba P a<b
+                ... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (Prev<.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (Prev<.ay pr))
                 zc9 :  ZChain A ay f mf supO x
                 zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
                      ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 }  -- no extention
@@ -469,28 +469,29 @@
                 ... | case2 sp<a | case1 b=sp = <-irr (case2 (subst ( λ  k → k < * a ) (trans *iso (sym b=sp)) sp<a  )) (proj1 p )
                 ... | case2 sp<a | case2 b<sp = <-irr (case2 (ptrans b<sp (subst (λ k → k < * a) *iso sp<a ))) (proj1 p )
                 simm {a} {b} (case2 sa) (case2 sb) p = fcn-imm {A} (& sp) {a} {b} f mf sa sb p
-                s-ismax : {a b : Ordinal} → odef schain a → b o< x → (ba : odef A b) →
+                s-ismax : {a b : Ordinal} → odef schain a → b o< osuc x → (ba : odef A b) →
                     Prev< A schain ba f ∨ (& (SUP.sup (supP (* (& schain))
                        (subst (λ k → k ⊆ A) (sym *iso) (record { incl = A∋schain }))
-                       (subst IsTotalOrderSet (sym *iso) scmp)))
-                     ≡ b) →
-                    * a < * b → odef schain b
-                s-ismax {a} {b} (case2 sa) b<x ba P a<b = {!!}
-                s-ismax {a} {b} (case1 sa) b<x ba P a<b with trio< b px
-                ... | tri< a₁ ¬b ¬c = case1 ( ZChain.is-max zc0 sa a₁ ba {!!} a<b )
-                ... | tri≈ ¬a b₁ ¬c = {!!}
-                ... | tri> ¬a ¬b c = {!!}
+                       (subst IsTotalOrderSet (sym *iso) scmp))) ≡ b)
+                     → * a < * b → odef schain b
+                s-ismax {a} {b} (case1 za) b<x ba (case1 Prev) a<b = {!!}
+                s-ismax {a} {b} (case2 sa) b<x ba (case1 Prev) a<b = {!!}
+                s-ismax {a} {b} (case1 za) b<x ba (case2 Sup) a<b = {!!}
+                s-ismax {a} {b} (case2 sa) b<x ba (case2 Sup) a<b = {!!}
           ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
                    record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
-                     ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = {!!} }  where -- no extention
-                z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< x → (ba : odef A b) →
+                     ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 }  where -- no extention
+                z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ba : odef A b) →
                             Prev< A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (* (& (ZChain.chain zc0)))
                                (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0))
                                (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0))))
                              ≡ b) →
                             * a < * b → odef (ZChain.chain zc0) b
-                z18 {a} {b} za b<x ba (case1 p) a<b = {!!}
-                z18 {a} {b} za b<x ba (case2 p) a<b = {!!}
+                z18 {a} {b} za b<x ba p a<b with osuc-≡< b<x
+                ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  lt ) ba p a<b 
+                ... | case1 b=x with p
+                ... | case1 pr = ⊥-elim ( ¬fy<x record {y = Prev<.y pr ; ay = Prev<.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (Prev<.x=fy pr ) } )
+                ... | case2 b=sup = ⊥-elim ( ¬x=sup {!!}) 
      ... | no ¬ox =  {!!}  where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
             field