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

comparison src/zorn.agda @ 995:04f4baee7b68

UChain is now u o< x

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Thu, 17 Nov 2022 08:36:03 +0900
parents	a15f1cddf4c6
children	61d74b3d5456

comparison

equal deleted inserted replaced

-:a15f1cddf4c6
+:04f4baee7b68
 supu=u   : supf u ≡ u
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
 (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where
 ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z
-ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : supf u o< supf x) ( is-sup : ChainP A f mf ay supf u )
+ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : u o< x) ( is-sup : ChainP A f mf ay supf u )
 ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 --
 --         f (f ( ... (supf y))) f (f ( ... (supf z1)))
 --        /          |         /             |
 (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b
 → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c
 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ =
 ⟪ ua , ch-init fc  ⟫
 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa ,  ch-is-sup ua ua<x is-sup fc  ⟫ =
-⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x (supf-mono a≤b ) ) is-sup fc  ⟫
+⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b) is-sup fc  ⟫
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
 field
 supf :  Ordinal → Ordinal
 → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )
 → ( { x : Ordinal } → x o< z → supf x ≡ supf1 x)
 → ( { x : Ordinal } → z o≤ x → supf z o≤ supf1 x)
 → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf1 z
 UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-is-sup u {x} u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u u<x1 cp1 fc1 ⟫  where
+UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-is-sup u {x} u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u u<x cp1 fc1 ⟫  where
-u<x0 : u o< z
-u<x0 = supf-inject0 supf-mono u<x
-u<x1 : supf1 u o< supf1 z
-u<x1 = subst (λ k → k o< supf1 z ) (eq<x u<x0) (ordtrans<-≤ u<x (lex o≤-refl ) )
 fc1 : FClosure A f (supf1 u) x
-fc1 = subst (λ k → FClosure A f k x ) (eq<x u<x0) fc
+fc1 = subst (λ k → FClosure A f k x ) (eq<x u<x) fc
+supf1-mono : {x y : Ordinal } →  x o≤  y  → supf1 x o≤ supf1 y
+supf1-mono = ?
 uc01 : {s : Ordinal } →  supf1 s o< supf1 u → s o< z
 uc01 {s} s<u with trio< s z
 ... | tri< a ¬b ¬c = a
 ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> uc02  s<u ) where -- (supf-mono (o<→≤ u<x0))
 uc02 :  supf1 u o≤ supf1 s
 uc02 = begin
-supf1 u  <⟨ u<x1 ⟩
+supf1 u  ≤⟨ supf1-mono (o<→≤ u<x) ⟩
 supf1 z  ≡⟨ cong supf1 (sym b) ⟩
 supf1 s ∎  where open o≤-Reasoning O
 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> uc03 s<u ) where
 uc03 :  supf1 u o≤ supf1 s
 uc03 = begin
-supf1 u  ≡⟨ sym (eq<x u<x0) ⟩
+supf1 u  ≡⟨ sym (eq<x u<x) ⟩
-supf u  <⟨ u<x ⟩
+supf u  ≤⟨ supf-mono (o<→≤ u<x) ⟩
 supf z  ≤⟨ lex (o<→≤ c) ⟩
 supf1 s ∎  where open o≤-Reasoning O
 cp1 : ChainP A f mf ay supf1 u
-cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x0) (ChainP.fcy<sup is-sup fc )
+cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x) (ChainP.fcy<sup is-sup fc )
-; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x0)
+; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x)
-(ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (eq<x (uc01 s<u) )) (sym (eq<x u<x0)) s<u)
+(ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (eq<x (uc01 s<u) )) (sym (eq<x u<x)) s<u)
 (subst (λ k → FClosure A f k z ) (sym (eq<x (uc01 s<u) )) fc ))
-; supu=u = trans (sym (eq<x u<x0)) (ChainP.supu=u is-sup)  }
+; supu=u = trans (sym (eq<x u<x)) (ChainP.supu=u is-sup)  }
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
 supf = ZChain.supf zc
 field
 zc04 : odef (UnionCF A f mf ay supf (& A))  (supf s)
 zc04 = ZChain.csupf zc (ordtrans<-≤ ss<sb (ZChain.supf-mono zc (o<→≤ b<z)))
 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
 zc05 with zc04
 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫
-... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u zc08 is-sup fc ⟫ where
+... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ZChain.supf-inject zc zc08) is-sup fc ⟫ where
 zc07 : FClosure A f (supf u) (supf s)   -- supf u ≤ supf s  → supf u o≤ supf s
 zc07 = fc
 zc06 : supf u ≡ u
 zc06 = ChainP.supu=u is-sup
 zc08 : supf u o< supf b
 HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
 * a < * b → odef (UnionCF A f mf ay supf x) b
 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
 is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
 is-max {a} {b} ua b<x ab P a<b | case2 is-sup with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
-... | case2 sb<sx = ⟪ ab , ch-is-sup b sb<sx  m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
+... | case2 sb<sx = ⟪ ab , ch-is-sup b b<x  m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
 b<A : b o< & A
 b<A = z09 ab
 m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
 chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
 is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
 is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
 ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
 ... | case2 y<b with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
-... | case2 sb<sx = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+... | case2 sb<sx = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym 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 (o<→≤ m09) fc
 m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
 fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc
 fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px →  FClosure A f (supf1 u) z
 fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc
 fcs<sup : {a b w : Ordinal } → a o< b → b o≤ x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
-fcs<sup with trio< a px
+fcs<sup {a} {b} {w} a<b b≤x fc with trio< a px
-... | tri< a ¬b ¬c = ? -- chain-mono ZChain.fcs<sup a
+... | tri< a<px ¬b ¬c = ? -- chain-mono ZChain.fcs<sup a
-... | tri≈ ¬a b ¬c = ? -- a ≡ px , b ≡ x, sp o≤ x → supf px o≤ supf x
+... | tri≈ ¬a a=px ¬c = ⟪ A∋fc _ f mf fc , ch-is-sup px px<b ? ? ⟫ where -- a ≡ px , b ≡ x, sp o≤ x → supf px o≤ supf x
+px<b : px o< b
+px<b = subst₂ (λ j k → j o< k) a=px refl a<b
+b=x : b ≡ x
+b=x with trio< b x
+... | tri< a ¬b ¬c = ?
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b c = ⊥-elim ( o<> c ? ) -- subst₂ (λ j k → j o≤ k ) ? ? a<b
 ... | tri> ¬a ¬b c = ? --  px o< a o< b o≤ x
 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z
 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
-zc11 {z} ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ = zc21 fc where
+zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc21 fc where
-u<x :  u o< x
-u<x =  supf-inject0 supf1-mono su<sx
 u≤px : u o≤ px
 u≤px = zc-b<x _ u<x
 zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1
 zc21 {z1} (fsuc z2 fc ) with zc21 fc
 ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
 ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫
 ... | case2 fc = case2 (fsuc _ fc)
 zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) | inspect supf1 u
-... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = zc17
+... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u u<px record {fcy<sup = zc13 ; order = zc17
 ; supu=u = trans (sym (sf1=sf0 (o<→≤ u<px))) (ChainP.supu=u is-sup) } (init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where
 u<px :  u o< px
 u<px =  ZChain.supf-inject zc a
 asp0 : odef A (supf0 u)
 asp0 = ZChain.asupf zc
 ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) )
 ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x ))
 ... | tri> ¬a ¬b c = o≤-refl0 ? -- (sym ( ZChain.supfmax zc px<x ))
 zc17 : {z : Ordinal } → supf0 z o≤ supf0 px
-zc17 = ? -- px o< z, px o< supf0 px
+zc17 {z} with trio< z px
+... | tri< a ¬b ¬c = ZChain.supf-mono zc (o<→≤ a)
+... | tri≈ ¬a b ¬c = o≤-refl0 (cong supf0 b)
+... | tri> ¬a ¬b px<z = o≤-refl0 zc177 where
+zc177 : supf0 z ≡ supf0 px
+zc177 = ZChain.supfmax zc px<z  -- px o< z, px o< supf0 px
 supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w
 supf-mono1 {z} {w} z≤w with trio< w px
 ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (ordtrans≤-< z≤w a))) refl ( supf-mono z≤w )
 ... | tri≈ ¬a refl ¬c with trio< z px
 ... | tri< a ¬b ¬c = zc17
 ... | tri≈ ¬a refl ¬c = o≤-refl
 ... | tri> ¬a ¬b c = o≤-refl
-supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
+supf-mono1 {z} {w} z≤w | tri> ¬a ¬b px<w with trio< z px
 ... | tri< a ¬b ¬c = zc17
-... | tri≈ ¬a b ¬c = o≤-refl0 ?
+... | tri≈ ¬a b ¬c = o≤-refl0 (cong supf0 b)  -- z=px   supf1 z = supf0 z, supf1 w = supf0 px
 ... | tri> ¬a ¬b c = o≤-refl
 pchain1 : HOD
 pchain1 = UnionCF A f mf ay supf1 x

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

comparison src/zorn.agda @ 995:04f4baee7b68