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

comparison src/zorn.agda @ 799:c8a166abcae0

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sun, 07 Aug 2022 18:39:18 +0900
parents	9cf74877efab
children	06eedb0d26a0

comparison

equal deleted inserted replaced

-:9cf74877efab
+:c8a166abcae0
 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u : Ordinal) : Set n where
 field
 fcy<sup  : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u )
 order    : {s z1 : Ordinal} → (lt : supf s o< supf u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
-supu=u   : o∅ o< u → supf u ≡ u
+supu=u   : supf u ≡ u
 -- Union of supf z which o< x
 --
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
 sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b
 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
 csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b)
 supf≤x :{x : Ordinal } → z o≤ x → supf z ≡  supf x
-fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
+fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
-fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)
+fcy<sup  {u} {w} u≤z fc with SUP.x<sup (sup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)
 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫
-... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) ))
+... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) ))
-... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
+... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
-supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
+supf-mono : {x y1 : Ordinal } → x o< y1 → supf x o≤ supf y1
-supf-mono {x} {y} x<y = sf<sy where
+supf-mono {x} {y1} x<y1 = sf<sy1 where
---     supf x <<  supf y →   supf x o< supf y
+--     supf x <<  supf y1 →   supf x o< supf y1
---     x o<  y →   supf x <= supf y
+--     x o<  y1 →   supf x <= supf y1
---   z o≤ x → supf x ≡ supf y ≡ supf z
+--   z o≤ x → supf x ≡ supf y1 ≡ supf z
---   x o< z → z o< y → supf x ≡ supf y ≡ supf z
+--   x o< z → z o< y1 → supf x ≡ supf y1 ≡ supf z
-sf<sy : supf x o≤ supf y
+supy : {x : Ordinal } → x o≤ z → FClosure A f y (supf x) → supf x ≡ y
-sf<sy with trio< x z
+supy {x} x≤z fcx = ? where
-... | tri> ¬a ¬b c = o≤-refl0 (( trans (sym (supf≤x (o<→≤ c))) (supf≤x (ordtrans (ordtrans c x<y ) <-osuc ) ) ))
+zc06 : ( * y  ≡  SUP.sup (sup x≤z )) ∨ ( * y  < SUP.sup ( sup x≤z ) )
-... | tri≈ ¬a b ¬c = o≤-refl0 (trans (sym (supf≤x (o≤-refl0 (sym b)))) (supf≤x (subst (λ k → k o< osuc y) b (o<→≤ x<y))))
+zc06 = SUP.x<sup (sup x≤z) ⟪ subst (λ k → odef A k ) (sym &iso)  ay , ch-init (init ay (sym &iso) ) ⟫
-... | tri< x<z ¬b ¬c with trio< (supf x) (supf y)
+sf<sy1 : supf x o≤ supf y1
+sf<sy1 with trio< x z
+... | tri> ¬a ¬b c = o≤-refl0 (( trans (sym (supf≤x (o<→≤ c))) (supf≤x (ordtrans (ordtrans c x<y1 ) <-osuc ) ) ))
+... | tri≈ ¬a b ¬c = o≤-refl0 (trans (sym (supf≤x (o≤-refl0 (sym b)))) (supf≤x (subst (λ k → k o< osuc y1) b (o<→≤ x<y1))))
+... | tri< x<z ¬b ¬c with trio< (supf x) (supf y1)
 ... | tri< a ¬b ¬c = o<→≤ a
 ... | tri≈ ¬a b ¬c = o≤-refl0 b
-... | tri> ¬a ¬b sy<sx with trio< z y
+... | tri> ¬a ¬b sy1<sx with trio< z y1
 ... | tri< a ¬b ¬c = ?
 ... | tri≈ ¬a b ¬c = ?
-... | tri> ¬a ¬b y<z = ?
+... | tri> ¬a ¬b y1<z = ?
-zc04 : x o< z → y o< z → supf x o≤ supf y
+zc04 : x o< z → y1 o≤ z → supf x o≤ supf y1
-zc04 x<z y<z with csupf (o<→≤ x<z) | csupf (o<→≤ y<z)
+zc04 x<z y1≤z with csupf (o<→≤ x<z) | csupf y1≤z
-... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-init fcy ⟫ with fcy<sup x<z fcy
+... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay1 , ch-init fcy1 ⟫ with fcy<sup (o<→≤ x<z) fcy1
 ... | case1 eq = o≤-refl0 (sym eq)
-... | case2 lt with fcy<sup y<z fcx
+... | case2 lt with fcy<sup y1≤z fcx
 ... | case1 eq = o≤-refl0 eq
 ... | case2 lt1 = ⊥-elim ( <-irr (case2 lt) lt1 )
-zc04 x<z y<z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-init fcy ⟫ with fcy<sup x<z fcy
+zc04 x<z y1≤z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay1 , ch-init fcy1 ⟫ with fcy<sup (o<→≤ x<z) fcy1
 ... | case1 eq = o≤-refl0 (sym eq)
-... | case2 lt with ChainP.fcy<sup is-sup-x fcy
+... | case2 lt with trio< (supf x) (supf y1)
-... | case1 eq with s≤fc (supf ux) f mf fcx
+... | tri< a ¬b ¬c = o<→≤ a
-... | case1 eq1 = o≤-refl0 ( trans ( subst₂ (λ j k → j ≡ k ) &iso &iso (sym (cong (&) eq1))) (sym eq) )
+... | tri≈ ¬a b ¬c = o≤-refl0 b
-... | case2 lt1 = ?    --  ux << sx, sy << sx
+... | tri> ¬a ¬b y1<z = ? where
-zc04 x<z y<z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-init fcy ⟫ | case2 lt1 = ? -- sy << sx
+zc05 : ( supf y1 ≡ supf ux ) ∨ (supf y1 << supf ux )
-zc04 x<z y<z | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ?
+zc05 = ChainP.fcy<sup is-sup-x fcy1
-zc04 x<z y<z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ?
+zc04 x<z y1≤z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay1 , ch-init fcy1 ⟫ | case2 lt1 = ? -- sy1 << sx
+zc04 x<z y1≤z | ⟪ ax , ch-init fcx ⟫ | ⟪ ay1 , ch-is-sup uy1 uy1≤z is-sup-y1 fcy1 ⟫ = ?
+zc04 x<z y1≤z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay1 , ch-is-sup uy1 uy1≤z is-sup-y1 fcy1 ⟫ = ?
 -- ... | tri< a ¬b ¬c = csupf (o<→≤ a)
 -- ... | tri≈ ¬a b ¬c = csupf (o≤-refl0 b)
--- ... | tri> ¬a ¬b c = subst (λ k → odef (UnionCF A f mf ay supf x) k ) ? (csupf ? )
+-- ... | tri> ¬a ¬b c = subst (λ k → odef (UnionCF A f mf ay1 supf x) k ) ? (csupf ? )
--- csy : odef (UnionCF A f mf ay supf y) (supf y)
+-- csy1 : odef (UnionCF A f mf ay1 supf y1) (supf y1)
--- csy = csupf ?
+-- csy1 = csupf ?
 order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
 order {b} {s} {z1} b<z sf<sb fc = zc04 where
 zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
 zc01  (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc03  where
 b<A = z09 ab
 m05 : b ≡ ZChain.supf zc b
 m05 = sym ( ZChain.sup=u zc ab (z09 ab)
 record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) uz )  }  )
 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
-m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
+m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
 m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b)
 → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
 m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
 m06 : ChainP A f mf ay (ZChain.supf zc) b
-m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = λ _ → ZChain.sup=u zc ab b<A {!!} }
+m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = ZChain.sup=u zc ab b<A {!!} }
 ... | no lim = record { is-max = is-max }  where
 is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
 b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
 ... | case2 y<b = chain-mono1 (osucc b<x)
 ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc )  m06 (subst (λ k → FClosure A f k b) m05 (init ab refl))  ⟫ where
 m09 : b o< & A
 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
-m07 {z} fc = ZChain.fcy<sup zc m09 fc
+m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
 m08 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b)
 → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
 m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
 m05 : b ≡ ZChain.supf zc b
 m05 = sym (ZChain.sup=u zc ab m09
 record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) lt )} )   -- ZChain on x
 m06 : ChainP A f mf ay (ZChain.supf zc) b
-m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = λ _ → ZChain.sup=u zc ab m09 {!!} }
+m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = ZChain.sup=u zc ab m09 {!!} }
 ---
 --- the maximum chain  has fix point of any ≤-monotonic function
 ---
 fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
 spi  ∎ ) where open ≡-Reasoning
 ... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt )
 uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi)
 uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi )
 uz02 :  ChainP A f mf ay isupf o∅
-uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} ; supu=u = λ lt → ⊥-elim ( o<¬≡ refl lt ) }
+uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} ; supu=u = ? }
 SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B
 SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; A∋maximal = SUP.A∋maximal sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt)    }
 --
 u=x : u ≡ x
 u=x with trio< u x
 ... | tri< a ¬b ¬c = {!!}
 ... | tri≈ ¬a b ¬c = b
 ... | tri> ¬a ¬b c = {!!}
-... | tri> ¬a ¬b c = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x (su=u1 {!!}) )) where
+... | tri> ¬a ¬b c = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x su=u1 )) where
 u=x : u ≡ x
 u=x with trio< u x
 ... | tri< a ¬b ¬c = {!!}
 ... | tri≈ ¬a b ¬c = b
 ... | tri> ¬a ¬b c = {!!}
 supf1 : Ordinal → Ordinal
 supf1 z with trio< z x
 ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
 ... | tri≈ ¬a b ¬c = spu
 ... | tri> ¬a ¬b c = spu
-fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → (w ≡ supf1 u) ∨ (w << supf1 u)
-fcy<sup {u} {w} u<x fc with trio< u x
-... | tri< a ¬b ¬c = ZChain.fcy<sup uzc <-osuc fc where
-uzc = pzc (osuc u) (ob<x lim a)
-... | tri≈ ¬a b ¬c = ⊥-elim (¬a u<x)
-... | tri> ¬a ¬b c = ⊥-elim (¬a u<x)
 pchain : HOD
 pchain = UnionCF A f mf ay supf1 x
 pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y

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

comparison src/zorn.agda @ 799:c8a166abcae0