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

changeset 541:f3e2cbd07e7c

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, 25 Apr 2022 17:51:24 +0900
parents 920a5c0568c3
children 3826221c61a6
files src/zorn.agda
diffstat 1 files changed, 32 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Apr 24 18:59:31 2022 +0900
+++ b/src/zorn.agda	Mon Apr 25 17:51:24 2022 +0900
@@ -177,10 +177,10 @@
       x<z : * x < * z 
       z<y : * z < * y 
 
-record Prev< (A : HOD) {x : Ordinal } (xa : odef A x)  ( f : Ordinal → Ordinal )  : Set n where
+record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x)  ( f : Ordinal → Ordinal )  : Set n where
    field
       y : Ordinal
-      ay : odef A y
+      ay : odef B y
       x=fy :  x ≡ f y 
 
 record SUP ( A B : HOD )  : Set (Level.suc n) where
@@ -200,9 +200,10 @@
       chain∋x : odef chain x
       f-total : IsTotalOrderSet chain 
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
-      is-max :  {a b : Ordinal } → (ca : odef chain a ) → odef A b → a o< z
-          → ( Prev< A (incl chain⊆A (subst (λ k → odef chain k ) (sym &iso) ca)) f
-               ∨ (sup (& chain) (subst (λ k → k  ⊆ A) (sym *iso) chain⊆A)  (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b ))
+      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 ) → (ba : odef A b) → a o< z
+          → 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
 
 Zorn-lemma : { A : HOD } 
@@ -266,9 +267,9 @@
      z03 f mf zc = z14 where
            chain = ZChain.chain zc
            sp1 = sp0 f mf zc
-           z10 :  {a b : Ordinal } → (ca : odef chain a ) → odef A b → a o< (& A)
-              → ( Prev< A (incl (ZChain.chain⊆A zc)  (subst (λ k → odef chain k ) (sym &iso) ca)) f
-                   ∨ (supO (& chain) (subst (λ k → k  ⊆ A) (sym *iso) (ZChain.chain⊆A zc))  (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc)) ≡ b ))
+           z10 :  {a b : Ordinal } → (ca : odef chain a ) → (ab : odef A b ) → a o< (& A)
+              →  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
            z10 = ZChain.is-max zc
            z12 : odef chain (& (SUP.sup sp1))
@@ -301,6 +302,12 @@
            (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc 
           c = & (SUP.sup sp1)
+     premax : {x y : Ordinal} → y o< x → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 :  ZChain A sa f mf supO y ) 
+        → {a b : Ordinal} (ca : odef (ZChain.chain zc0) a)
+        → odef A b → a o< x → Prev< A (ZChain.chain zc0) (incl (ZChain.chain⊆A zc0) (subst (odef (ZChain.chain zc0)) (sym &iso) ca)) 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
+     premax {x} {y} y<x  f mf zc0 {a} {b} ca ab a<x P a<b = ZChain.is-max zc0 ca ab {!!} {!!} a<b
      -- Union of ZFChain
      UZFChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (B : Ordinal) 
             → ( (y : Ordinal) → y o< B → ZChain A sa f mf supO y ) → HOD
@@ -317,8 +324,8 @@
           zc0 : ZChain A sa f mf supO (Oprev.oprev op) 
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
           zc1 : ZChain A sa f mf supO x 
-          zc1 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
-             ; chain∋x  = {!!} ; is-max = {!!} }
+          zc1 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; f-immediate = {!!}
+             ; chain∋x  = ZChain.chain∋x zc0 ; is-max = {!!} }
      ... | yes ax = zc4 where -- we have previous ordinal and A ∋ x
           px = Oprev.oprev op
           zc0 : ZChain A sa f mf supO (Oprev.oprev op) 
@@ -327,34 +334,39 @@
           --   x has some y which y < x ∧ f y ≡ x
           --   x has no y which y < x 
           zc4 : ZChain A sa f mf supO x
-          zc4 with ODC.p∨¬p O ( Prev< A ax f )
+          zc4 with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ax f )
           ... | case1 y = zc7 where
+                chain = ZChain.chain zc0
                 zc7 :  ZChain A sa f mf supO x
                 zc7 with ODC.∋-p O  (ZChain.chain zc0) (* ( f x ) )
                 ... | yes y = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 
-                     ; chain∋x  = {!!} ; is-max = {!!} }  -- no extention
+                     ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} }  -- no extention
                 ... | no not = record { chain = zc5 ; chain⊆A =  ⊆-zc5
-                    ; f-total = zc6 ; f-next = {!!} ; chain∋x  = ⟪ subst (λ k → odef A (& k)) *iso sa , case1 (ZChain.chain∋x zc0)  ⟫ ; is-max = {!!} } where
+                    ; f-total = zc6 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = {!!} } where
                 --   extend with f x
                     zc5 : HOD
-                    zc5 = record { od = record { def = λ z → odef A z ∧ (odef (ZChain.chain zc0) z ∨ (z ≡ f x)) } ; odmax = & A ; <odmax = z07 }
+                    zc5 = record { od = record { def = λ z → odef (ZChain.chain zc0) z ∨ (z ≡ f x) } ; odmax = & A ; <odmax = {!!} }
                     ⊆-zc5 : zc5 ⊆ A 
-                    ⊆-zc5 = record { incl = λ lt → proj1 lt  }
+                    ⊆-zc5 = record { incl = λ lt → {!!} }
                     IPO = ⊆-IsPartialOrderSet  ⊆-zc5 PO
-                    fx>zc : ( z : Ordinal ) → (odef (ZChain.chain zc0) z → * z < * ( f x )
-                    fx>zc = ?
+                    fx>zc : ( z : Ordinal ) → odef (ZChain.chain zc0) z → * z < * ( f x )
+                    fx>zc = {!!}
                     cmp : Trichotomous _ _ 
-                    cmp record { elm = a ; is-elm = aa } record { elm = b ; is-elm = ab } = ?
+                    cmp record { elm = a ; is-elm = aa } record { elm = b ; is-elm = ab } with aa | ab
+                    ... | case1 x | case1 x₁ = IsStrictTotalOrder.compare (ZChain.f-total zc0) (me x) (me x₁)
+                    ... | case1 c | case2 fx = {!!}
+                    ... | case2 x | case1 x₁ = {!!}
+                    ... | case2 x | case2 x₁ = tri≈ {!!} (subst₂ (λ j k → j ≡ k ) *iso *iso (trans (cong (*) x) (sym (cong (*) x₁ ) ))) {!!}
                     zc6 : IsTotalOrderSet zc5
                     zc6 =  record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}
                         ; compare = cmp }
           ... | case2 not with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) {!!} {!!} ) ))
           ... | case1 y = {!!}
           ... | case2 not = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 
-                     ; chain∋x  = {!!} ; is-max = {!!} }  -- no extention
+                     ; f-immediate = {!!} ; chain∋x  = ZChain.chain∋x zc0 ; is-max = {!!} }  -- no extention
      ind f mf x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
      ... | tri< a ¬b ¬c = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
-              ; chain∋x  = {!!}  ; is-max = {!!} } where
+              ; f-immediate = {!!} ; chain∋x  = {!!}  ; is-max = {!!} } where
           zc0 = prev (& A) a
      ... | tri≈ ¬a b ¬c = {!!}
      ... | tri> ¬a ¬b c = {!!}