Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 624:d0938f220648

supf again

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 20 Jun 2022 07:49:35 +0900
parents	7c5a922931e5
children	886e1f82cca0

comparison

equal deleted inserted replaced

-:7c5a922931e5
+:d0938f220648
 record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
 field
 x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
-record SupF (A : HOD) : Set n where
+record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) (supf : Ordinal → HOD) ( z : Ordinal ) : Set (Level.suc n) where
-field
-chain : Ordinal
--- 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
-chain = * (SupF.chain (supf z ))
+chain = supf z
 field
 chain⊆A : chain ⊆' A
 chain∋x : odef chain x
 initial : {y : Ordinal } → odef chain y → * x ≤ * y
-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< osuc z  → (ab : odef A b)
 → HasPrev A chain ab f ∨  IsSup A chain ab
 → * a < * b  → odef chain b
 record ZChain1 ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal )  ( z : Ordinal ) : Set (Level.suc n) where
 field
-supf : Ordinal → SupF A
+supf : Ordinal → HOD
 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 ))
+chain-mono : {x y : Ordinal} → x o≤ y → y o≤ z →  supf x ⊆' supf y
+f-total : {x y : Ordinal} → x o≤ z → IsTotalOrderSet (supf x)
 record Maximal ( A : HOD )  : Set (Level.suc n) where
 field
 maximal : HOD
 A∋maximal : A ∋ maximal
 cf-is-<-monotonic nmx x ax = ⟪ proj2 (is-cf nmx ax ) , proj1 (is-cf nmx ax ) ⟫
 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
 cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
 zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc1 : ZChain1 A (& s) f (& A) ) → SUP A  (ZChain.chain (ZChain1.zc zc1))
-zsup f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc  )   where
+zsup f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain1.f-total zc1 {!!} )   where
 zc = ZChain1.zc zc1
 A∋zsup : (nmx : ¬ Maximal A ) (zc1 : ZChain1 A (& s) (cf nmx)  (& A) )
 →  A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc1 )))
 A∋zsup nmx zc1 = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal  (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc1 ) )
 sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc1 : ZChain1 A (& s) f  (& A) ) → SUP A (ZChain.chain (ZChain1.zc zc1))
-sp0 f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain.f-total zc)   where
+sp0 f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain1.f-total zc1 {!!} )   where
 zc = ZChain1.zc zc1
 zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P
 zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y)
 ---
 z20 {y} zy with SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) zy)
 ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
 ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
 -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ?  (SUP.x<sup sp1 ? ) }
 z14 :  f (& (SUP.sup (sp0 f mf zc1))) ≡ & (SUP.sup (sp0 f mf zc1))
-z14 with ZChain.f-total zc  (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12
+z14 with ZChain1.f-total zc1 {!!}  (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12
 ... | tri< a ¬b ¬c = ⊥-elim z16 where
 z16 : ⊥
 z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
 ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
 ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
 -- we have previous ordinal to use induction
 --
 open ZChain
 px = Oprev.oprev op
-supf : Ordinal → SupF A
+supf : Ordinal → HOD
 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)
 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 : Ordinal → HOD
 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 = ZChain.chain zc0
-... | tri> ¬a ¬b c = record { chain = & (ZChain.chain zc0) }
+... | tri> ¬a ¬b c = ZChain.chain zc0
-seq : ZChain.chain zc0 ≡ * (SupF.chain (supf0 x))
+seq : ZChain.chain zc0 ≡ supf0 x
 seq with trio< x x
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
-... | tri≈ ¬a b ¬c = sym *iso
+... | tri≈ ¬a b ¬c = refl
-... | tri> ¬a ¬b c = sym *iso
+... | tri> ¬a ¬b c = refl
-seq<x : {b : Ordinal } → b o< x →  * (SupF.chain (supf b))  ≡ * (SupF.chain (supf0 b))
+seq<x : {b : Ordinal } → b o< x →  supf b  ≡ supf0 b
 seq<x {b} b<x with trio< b x
 ... | tri< a ¬b ¬c = refl
 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
 mono : {a b  : Ordinal}  → a o≤ b → b o< osuc x →
-* (SupF.chain (supf0 a )) ⊆' * (SupF.chain (supf0 b ))
+supf0 a  ⊆' supf0 b
 mono {a} {b} a≤b b<ox with osuc-≡< a≤b
 ... | case1 refl = λ x → x
 ... | case2 a<b with osuc-≡< b<ox
 ... | case1 b=x = subst₂ (λ j k → j ⊆' k ) (seq<x a<x) nc00 ( ZChain1.chain-mono zc1 a≤px <-osuc  ) where
 a<x : a o< x
 a<x with  osuc-≡< b<ox
 ... | case1 b=x = subst (λ k → a o< k ) b=x a<b
 ... | case2 b<x = ordtrans a<b b<x
 a≤px : a o≤  px
 a≤px = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) a<x
-nc00 : * (SupF.chain (supf px))  ≡ * (SupF.chain (supf0 b))
+nc00 : supf px  ≡ supf0 b
 nc00 with trio< b x
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b b=x )
-... | tri≈ ¬a b ¬c = sym *iso
+... | tri≈ ¬a b ¬c = refl
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b=x )
 ... | case2 b<x = subst₂ (λ j k → j ⊆' k ) (seq<x a<x ) (seq<x b<x )
 ( ZChain1.chain-mono zc1 a≤b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) b<x ) )
 where
 a<x : a o< x
 zc17 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
 ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b
 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
 ... | case1 is-sup = -- x is a sup of zc0
-record { zc = record { chain⊆A = {!!}  ; f-total = {!!} ; f-next = {!!} ; chain∋sup = {!!}
+record { zc = record { chain⊆A = {!!}  ; f-total = {!!} ; f-next = {!!}
-; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  ; supf = supf0 ; chain-mono = mono } where
+; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!} }  ; supf = supf0 ; chain-mono = mono } where
 sup0 : SUP A (ZChain.chain zc0)
 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
 x21 :  {y : HOD} → ZChain.chain zc0 ∋ y → (y ≡ * x) ∨ (y < * x)
 x21 {y} zy with IsSup.x<sup is-sup zy
 ... | case1 y=x = case1 ( subst₂ (λ j k → j ≡ * k  ) *iso &iso ( cong (*) y=x)  )
 a<b = subst (λ k → a < k ) (trans sp=b *iso ) (subst (λ k → a < k ) (sym *iso) a<sp )
 ... | case2 a<sp | case2 sp<b  = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b) lt ) where
 a<b : a < b
 a<b = ptrans  (subst (λ k → a < k ) (sym *iso) a<sp ) ( subst₂ (λ j k → j < k ) refl *iso sp<b )
 scmp : {a b : HOD} → odef schain (& a) → odef schain (& b) → Tri (a < b) (a ≡ b) (b < a )
-scmp (case1 za) (case1 zb) = ZChain.f-total zc0 za zb
+scmp (case1 za) (case1 zb) = ZChain1.f-total zc1 {!!} za zb
 scmp {a} {b} (case1 za) (case2 fb) = cmp za fb
 scmp  (case2 fa) (case1 zb) with  cmp zb fa
 ... | tri< a ¬b ¬c = tri> ¬c (λ eq → ¬b (sym eq))  a
 ... | tri≈ ¬a b ¬c = tri≈ ¬c (sym b) ¬a
 ... | tri> ¬a ¬b c = tri< c (λ eq → ¬b (sym eq))  ¬a
 z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
 z23 : odef chain0 b
 z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋x zc0 )
 ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋x zc0 )
 ... | case2 y<b  = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b
-supf0 : Ordinal → SupF A
+supf0 : Ordinal → HOD
 supf0 z with trio< z x
 ... | tri< a ¬b ¬c = supf z
-... | tri≈ ¬a b ¬c = record { chain = & schain }
+... | tri≈ ¬a b ¬c = schain
-... | tri> ¬a ¬b c = record { chain = & schain }
+... | tri> ¬a ¬b c = schain
-seq : schain ≡ * (SupF.chain (supf0 x))
+seq : schain ≡ supf0 x
 seq with trio< x x
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
-... | tri≈ ¬a b ¬c = sym *iso
+... | tri≈ ¬a b ¬c = refl
-... | tri> ¬a ¬b c = sym *iso
+... | tri> ¬a ¬b c = refl
-seq<x : {b : Ordinal } → b o< x →  * (SupF.chain (supf b))  ≡ * (SupF.chain (supf0 b))
+seq<x : {b : Ordinal } → b o< x →  supf b  ≡ supf0 b
 seq<x {b} b<x with trio< b x
 ... | tri< a ¬b ¬c = refl
 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
-mono : {a b  : Ordinal}  → a o≤ b → b o< osuc x →
+mono : {a b  : Ordinal}  → a o≤ b → b o< osuc x → supf0 a ⊆' supf0 b
-* (SupF.chain (supf0 a )) ⊆' * (SupF.chain (supf0 b ))
 mono {a} {b} a≤b b<ox = {!!}
 ... | case2 ¬x=sup =  no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
 z18 :  {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 →
 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-initial :  {z : Ordinal} → odef Uz z → * y ≤ * z
 u-initial {z} u = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
 u-chain∋x :  odef Uz y
 u-chain∋x = record { u = y ; u<x = {!!} ; chain∋z = ZChain.chain∋x (ZChain1.zc (prev y {!!} ay )) }
-supf0 : Ordinal → SupF A
+supf0 : Ordinal → HOD
 supf0 z with trio< z x
 ... | tri< a ¬b ¬c = ZChain1.supf (prev z a {y} ay) z
-... | tri≈ ¬a b ¬c = record { chain = & Uz }
+... | tri≈ ¬a b ¬c = Uz
-... | tri> ¬a ¬b c = record { chain = & Uz }
+... | tri> ¬a ¬b c = Uz
-seq : Uz ≡ * (SupF.chain (supf0 x))
+seq : Uz ≡ supf0 x
 seq with trio< x x
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
-... | tri≈ ¬a b ¬c = sym *iso
+... | tri≈ ¬a b ¬c = refl
-... | tri> ¬a ¬b c = sym *iso
+... | tri> ¬a ¬b c = refl
-seq<x : {b : Ordinal } → (b<x : b o< x ) →  * (SupF.chain (ZChain1.supf (prev b b<x {y} ay) b))  ≡ * (SupF.chain (supf0 b))
+seq<x : {b : Ordinal } → (b<x : b o< x ) →  ZChain1.supf (prev b b<x {y} ay) b  ≡ supf0 b
 seq<x {b} b<x with trio< b x
-... | tri< a ¬b ¬c = cong (λ k → * (SupF.chain (ZChain1.supf (prev b k {y} ay) b)) ) o<-irr --  b<x ≡ a
+... | tri< a ¬b ¬c = cong (λ k → ZChain1.supf (prev b k {y} ay) b) o<-irr --  b<x ≡ a
 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
 u-mono :  ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain1 A y f a) (zb : ZChain1 A y f b) → ZChain.chain (ZChain1.zc za)  ⊆' ZChain.chain (ZChain1.zc zb)
 u-mono a b b<x a≤b za zb {i} zai = ZChain1.chain-mono zb a≤b <-osuc (uz01 zai) where
-uz01 : odef (* (SupF.chain (ZChain1.supf za a))) i → odef (* (SupF.chain (ZChain1.supf zb a))) i
+uz01 : odef (ZChain1.supf za a) i → odef (ZChain1.supf zb a) i
 uz01 = {!!}
 u-total : IsTotalOrderSet Uz
 u-total {x} {y} ux uy  with trio< (UZFChain.u ux) (UZFChain.u uy)
-... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-mono (UZFChain.u ux) (UZFChain.u uy)
+... | tri< a ¬b ¬c = ZChain1.f-total (uzc1 uy) {!!} (u-mono (UZFChain.u ux) (UZFChain.u uy)
 (UZFChain.u<x uy) (ordtrans a <-osuc ) (uzc1 ux) (uzc1 uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
-... | tri≈ ¬a b ¬c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
+... | tri≈ ¬a b ¬c = ZChain1.f-total (uzc1 ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
 (UZFChain.u<x ux) (subst (λ k → k o< osuc (UZFChain.u ux)) b <-osuc) (uzc1 uy) (uzc1 ux) (UZFChain.chain∋z uy))
-... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
+... | tri> ¬a ¬b c = ZChain1.f-total (uzc1 ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
 (UZFChain.u<x ux) (ordtrans c <-osuc) (uzc1 uy) (uzc1 ux) (UZFChain.chain∋z uy))
 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain1 A y f (& A)
 SZ f mf = TransFinite {λ z → {y : Ordinal } → (ay : odef A y ) → ZChain1 A y f z  } (ind f mf) (& A)

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

comparison src/zorn.agda @ 624:d0938f220648