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

changeset 646:c2446d7d24c0

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, 27 Jun 2022 03:23:44 +0900
parents 2648a273647e
children 7629714b4d07
files src/zorn.agda
diffstat 1 files changed, 17 insertions(+), 53 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jun 27 00:48:05 2022 +0900
+++ b/src/zorn.agda	Mon Jun 27 03:23:44 2022 +0900
@@ -385,25 +385,6 @@
      -- create all ZChains under o< x
      --
 
-     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 = λ lt →
-        subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc _ f mf lt )) ) }
-     init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain A y f x
-     init-chain {y} {x} ay f mf x≤y = record { chain⊆A = λ fx →  A∋fc y f mf fx
-                     ; f-next = λ {x} sx → fsuc x sx  ; supf = λ _ → ys ay f mf  ; chain = ys ay f mf
-                     ; initial = initial ; chain∋x  = init ay ; is-max = is-max } 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 (case1 prev) a<b = subst (λ k → FClosure A f y k ) (sym (HasPrev.x=fy prev )) ( fsuc (HasPrev.y prev) (HasPrev.ay prev) )
-               is-max {a} {b} yca b≤x ab (case2 sup) a<b with IsSup.x<sup sup (init ay)
-               ... | case1 y=b = subst ( λ k → FClosure A f y k )  y=b  (init ay)
-               ... | case2 y<b = ?
-               initial : {i : Ordinal} → odef (ys ay f mf) i → * y ≤ * i
-               initial lt = s≤fc _ f mf lt
-
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
          → ((z : Ordinal) → z o< x → ZChain A y f z) → ZChain A y f x
      ind f mf {y} ay x prev with Oprev-p x
@@ -424,10 +405,10 @@
           no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc) ab f ∨  IsSup A (ZChain.chain zc) ab →
                             * a < * b → odef (ZChain.chain zc) b ) → ZChain A y f x
-          no-extenion is-max = record { chain⊆A = subst (λ k → k ⊆' A ) ? (ZChain.chain⊆A zc)
-                     ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) ? (ZChain.initial zc)
-                     ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) ? (ZChain.f-next zc)  ; chain  = ZChain.chain zc 
-                     ; chain∋x  = subst (λ k → odef k y ) ? (ZChain.chain∋x  zc)
+          no-extenion is-max = record { chain⊆A = ZChain.chain⊆A zc
+                     ; initial = ZChain.initial zc
+                     ; f-next =  ZChain.f-next zc  ; chain  = ZChain.chain zc 
+                     ; chain∋x  = ZChain.chain∋x  zc
                              ; 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  ) ? is-max } 
 
@@ -451,8 +432,8 @@
                 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc) ax )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  chain⊆A = {!!} ; f-next = {!!}  ; chain = schain
-                     ; initial = {!!} ; chain∋x  = {!!} ; is-max = {!!}   } where
+                record {  chain⊆A = s⊆A ; f-next = scnext ; chain = schain
+                     ; initial = scinit ; chain∋x  = case1 (ZChain.chain∋x zc) ; is-max = s-ismax } where
                 sup0 : SUP A (ZChain.chain zc) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
                         x21 :  {y : HOD} → ZChain.chain zc ∋ y → (y ≡ * x) ∨ (y < * x)
@@ -545,46 +526,29 @@
                 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
-     ... | no ¬ox with trio< x y
-     ... | tri< a ¬b ¬c = init-chain ay f mf {!!}
-     ... | tri≈ ¬a b ¬c = init-chain ay f mf {!!}
-     ... | tri> ¬a ¬b y<x = record { chain⊆A = {!!} ; f-next = {!!} ; chain = Uz
-                     ; initial = {!!} ; chain∋x  = {!!} ; is-max = {!!} }   where --- limit ordinal case
+     ... | no ¬ox = record { chain⊆A = Uz⊆A ; f-next = u-next ; chain = Uz
+                     ; initial = u-initial ; chain∋x  = u-chain∋x ; is-max = {!!} }   where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
             field
                u : Ordinal
                u<x : u o< x
                chain∋z : odef (ZChain.chain (prev u u<x  )) z
-         Uz⊆A : {z : Ordinal} → UZFChain z → odef A z
-         Uz⊆A {z} u = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u)
+         Uz⊆A : {z : Ordinal} → UZFChain z ∨ FClosure A f y z → odef A z
+         Uz⊆A {z} (case1 u) = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u)
+         Uz⊆A (case2 lt) = A∋fc _ f mf lt 
          uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f (UZFChain.u u)
          uzc {z} u =  prev (UZFChain.u u) (UZFChain.u<x u) 
          Uz : HOD
-         Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A
+         Uz = record { od = record { def = λ z → UZFChain z ∨ FClosure A f y z } ; odmax = & A
              ; <odmax = λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) }
          u-next : {z : Ordinal} → odef Uz z → odef Uz (f z)
-         u-next {z} u = record { u = UZFChain.u u ; u<x = UZFChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UZFChain.chain∋z u)  }
+         u-next {z} (case1 u) = case1 record { u = UZFChain.u u ; u<x = UZFChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UZFChain.chain∋z u)  }
+         u-next {z} (case2 u) = case2 ( fsuc _ u )
          u-initial :  {z : Ordinal} → odef Uz z → * y ≤ * z 
-         u-initial {z} u = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
+         u-initial {z} (case1 u) = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
+         u-initial {z} (case2 u) = s≤fc _ f mf u
          u-chain∋x :  odef Uz y
-         u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ) }
-         ord≤< : {x y z : Ordinal} → x o< z → z o≤ y → x o< y
-         ord≤< {x} {y} {z} x<z z≤y  with  osuc-≡< z≤y
-         ... | case1 z=y  = subst (λ k → x o< k ) z=y x<z
-         ... | case2 z<y  = ordtrans x<z z<y
-         u-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → ? ⊆' ? 
-         u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
-         ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ? -- um00 where -- ZChain.chain-mono (prev w ? ay) ? ? lt
-             -- um00 : odef  (ZChain.supf (prev z a ) z) i → odef  (ZChain.supf (prev w a₁ ) w) i 
-             -- um00 = {!!}
-             -- um01 : odef  (ZChain.supf (prev z a ) z) i → odef  (ZChain.supf (prev z {!!} ) w) i 
-             -- um01 = ? -- ZChain.mono (prev z a ) ?  ?
-         ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = λ lt → record { u = z ; u<x = a ; chain∋z = ? }
-         ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim ( osuc-< w≤x c )
-         ... | tri≈ ¬a z=x ¬c | tri< w<x ¬b ¬c₁ = ⊥-elim ( osuc-< z≤w (subst (λ k → w o< k ) (sym z=x) w<x ) )
-         ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = λ lt → lt 
-         ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim ( osuc-< w≤x c ) -- o<> c ( ord≤< w≤x )) -- z≡w x o< w
-         ... | tri> ¬a ¬b c | t = ⊥-elim ( osuc-< w≤x (ord≤< c  z≤w ) ) -- x o< z → x o< w 
+         u-chain∋x = case2 ( init ay )
          
      record ZChain1 ( f : Ordinal → Ordinal )  ( y z : Ordinal ) : Set (Level.suc n) where
       inductive