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

changeset 610:e0cd78095f1b

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 Fri, 17 Jun 2022 16:21:28 +0900
parents 5039d228838c
children d6ad1af5299e
files src/zorn.agda
diffstat 1 files changed, 60 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Jun 17 11:42:01 2022 +0900
+++ b/src/zorn.agda	Fri Jun 17 16:21:28 2022 +0900
@@ -236,9 +236,9 @@
 record SupF (A : HOD) : Set n where
    field
       chain : Ordinal
-      sup : Ordinal 
-      asup : odef A sup
-      supf-isSup :  IsSup A (* chain) asup
+      -- sup : Ordinal 
+      -- asup : odef A sup
+      -- is-sup :  IsSup A (* chain) asup
 
 record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) (supf : Ordinal → SupF A) ( z : Ordinal ) : Set (Level.suc n) where
    chain : HOD
@@ -253,12 +253,12 @@
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
-      supf-mono : {x y : Ordinal} → x o< y → y o< osuc z →  SupF.sup (supf x ) o< SupF.sup (supf y )
 
 record ZChain1 ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal )  ( z : Ordinal ) : Set (Level.suc n) where
    field
       supf : Ordinal → SupF A
       zc : ZChain A x f supf z
+      chain-mono : {x y : Ordinal} → x o< y → y o< osuc z →  * (SupF.chain (supf x )) ⊆' * (SupF.chain (supf y ))
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -404,21 +404,23 @@
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc1
           c = & (SUP.sup sp1)
 
-     ys : {y : Ordinal} → (ay : odef A y)  (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → HOD
-     ys {y} ay f mf = record { od = record { def = λ x →  FClosure A f y x  } ; odmax = & A ; <odmax = {!!} }
-     init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain1 A y f  x
-     init-chain {y} {x} ay f mf x≤y = record { zc = record { chain⊆A = λ fx →  A∋fc y f mf {!!}
-                     ; f-total = {!!} ; f-next = λ {x} sx → {!!} 
-                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} } ; supf = {!!} } where
-               i-total : IsTotalOrderSet (ys ay f mf )
-               i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb)
-               is-max : {a b : Ordinal} → odef (ys ay f mf) a →
-                    b o< osuc x → (ab : odef A b) → HasPrev A (ys ay f mf) ab f ∨ IsSup A (ys ay f mf) ab →
-                    * a < * b → odef (ys ay f mf) b
-               is-max {a} {b} yca b≤x ab P a<b = {!!}
-               initial : {i : Ordinal} → odef (ys ay f mf) i → * y ≤ * i
-               initial {i} (init ai) = case1 refl
-               initial .{f x} (fsuc x lt) = {!!}
+     -- ys : {y : Ordinal} → (ay : odef A y)  (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → HOD
+     -- ys {y} ay f mf = record { od = record { def = λ x →  FClosure A f y x  } ; odmax = & A ; <odmax = {!!} }
+     -- init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain1 A y f  x
+     -- init-chain {y} {x} ay f mf x≤y = record { zc = record { chain⊆A = λ fx →  A∋fc y f mf {!!}
+     --                 ; f-total = {!!} ; f-next = λ {x} sx → {!!} 
+     --                 ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; chain-mono = {!!} } ; supf = supf } where
+     --           supf : Ordinal → SupF A
+     --           supf x = record { chain = & (ys ay f mf) }
+     --           i-total : IsTotalOrderSet (ys ay f mf )
+     --           i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb)
+     --           is-max : {a b : Ordinal} → odef (ys ay f mf) a →
+     --                b o< osuc x → (ab : odef A b) → HasPrev A (ys ay f mf) ab f ∨ IsSup A (ys ay f mf) ab →
+     --                * a < * b → odef (ys ay f mf) b
+     --           is-max {a} {b} yca b≤x ab P a<b = {!!}
+     --           initial : {i : Ordinal} → odef (ys ay f mf) i → * y ≤ * i
+     --           initial {i} (init ai) = case1 refl
+     --           initial .{f x} (fsuc x lt) = {!!}
 
      --
      -- create all ZChains under o< x
@@ -436,6 +438,8 @@
           px = Oprev.oprev op
           supf : Ordinal → SupF A
           supf = ZChain1.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay)
+          zc1 : ZChain1 A y f (Oprev.oprev op)
+          zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay 
           zc0 : ZChain A y f (ZChain1.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay)) (Oprev.oprev op)
           zc0 = ZChain1.zc (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay)
           zc0-b<x : (b : Ordinal ) → b o< x → b o< osuc px
@@ -443,12 +447,45 @@
           px<x : px o< x
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
 
+          no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
+                    HasPrev A (ZChain.chain zc0) ab f ∨  IsSup A (ZChain.chain zc0) ab →
+                            * a < * b → odef (ZChain.chain zc0) b ) → ZChain1 A y f x
+          no-extenion is-max = record { supf = supf0 ; zc = record { chain⊆A = subst (λ k → k ⊆' A ) seq (ZChain.chain⊆A zc0)
+                     ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) seq (ZChain.initial zc0)
+                     ; f-total = subst (λ k → IsTotalOrderSet k ) seq (ZChain.f-total zc0)
+                     ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) seq (ZChain.f-next zc0) 
+                     ; f-immediate =  subst (λ k →  {x₁ : Ordinal} {y₁ : Ordinal} → odef k x₁ → odef k y₁ →
+                            ¬ (* x₁ < * y₁) ∧ (* y₁ < * (f x₁)) ) seq (ZChain.f-immediate zc0) ; chain∋x  = subst (λ k → odef k y ) seq (ZChain.chain∋x  zc0)
+                             ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) →
+                                 HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) seq is-max } 
+                     ; chain-mono = mono } where
+                supf0 : Ordinal → SupF A
+                supf0 z with trio< z x
+                ... | tri< a ¬b ¬c = supf z
+                ... | tri≈ ¬a b ¬c = record { chain = & (ZChain.chain zc0) } 
+                ... | tri> ¬a ¬b c = record { chain = & (ZChain.chain zc0) } 
+                seq : ZChain.chain zc0 ≡ * (SupF.chain (supf0 x)) 
+                seq with trio< x x
+                ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
+                ... | tri≈ ¬a b ¬c = sym *iso
+                ... | tri> ¬a ¬b c = sym *iso
+                mono : {a b  : Ordinal}  → a o< b → b o< osuc x →
+                    * (SupF.chain (supf0 a )) ⊆' * (SupF.chain (supf0 b ))
+                mono {a} {b} a<b b<ox with osuc-≡< b<ox | trio< a x | trio< b x
+                ... | case1 b=x | tri< a₁ ¬b ¬c | tri< a₂ ¬b₁ ¬c₁ = ⊥-elim ( ¬b₁ b=x ) 
+                ... | case1 b=x | tri< a₁ ¬b ¬c | tri≈ ¬a b₁ ¬c₁ = subst (λ k →  _  ⊆' k ) {!!} ( ZChain1.chain-mono zc1 a<b {!!} )
+                ... | case1 b=x | tri< a₁ ¬b ¬c | tri> ¬a ¬b₁ c =  ⊥-elim ( ¬b₁ b=x )
+                ... | case1 b=x | tri≈ ¬a b₁ ¬c | u = {!!}
+                ... | case1 b=x | tri> ¬a ¬b c | u = {!!}
+                ... | case2 b<x | t | u = {!!}
+
+
           zc4 : ZChain1 A y f x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax =  -- ¬ A ∋ p, just skip
-                 record { zc = record { 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
+                 record { supf = supf ; zc = record { chain⊆A = {!!} ; initial = {!!}
+                     ; f-total = {!!} ; f-next =  {!!}  ; chain-mono = {!!} 
+                     ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!}  } }  where -- no extention
                 zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc0) ab f ∨  IsSup A (ZChain.chain zc0) ab →
                             * a < * b → odef (ZChain.chain zc0) b
@@ -456,7 +493,7 @@
                 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
                 ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt)  ab P a<b
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax f )   -- we have to check adding x preserve is-max ZChain A y f mf supO x
-          ... | case1 pr = {!!}  where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
+          ... | case1 pr = zc9 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
                 chain0 = ZChain.chain zc0
                 zc17 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
                             HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0) ab →