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

comparison src/zorn.agda @ 1053:a281ad683577

order connected

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Fri, 09 Dec 2022 20:53:59 +0900
parents	0b6cee971cba
children	38148b08d85c

comparison

equal deleted inserted replaced

-:0b6cee971cba
+:a281ad683577
 supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b
 supf-mono< {a} {b} b≤z sa<sb  with order {a} {b} b≤z sa<sb (init asupf refl)
 ... | case2 lt = lt
 ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb )
-supfeq : {a b : Ordinal } → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b
+supfeq : {a b : Ordinal } → a o≤ z →  b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b
-supfeq = ?
+supfeq {a} {b} a≤z b≤z ua=ub with trio< (supf a) (supf b)
+... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
-unioneq : {a b : Ordinal } → z o≤ supf a → supf a o≤ supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b
+IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb )
-unioneq = ?
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> (
--- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → ChainP A f supf (supf b)
+IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa )
---    the condition of cfcs is satisfied, this is obvious
+union-max : {a b : Ordinal } → z o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b
+union-max {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where
+z47 : {w : Ordinal } → odef (UnionCF A f ay supf a ) w → odef ( UnionCF A f ay supf b ) w
+z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where
+u<b : u o< b
+u<b = ordtrans u<a (supf-inject sa<sb )
+z48 : {w : Ordinal } → odef (UnionCF A f ay supf b ) w → odef ( UnionCF A f ay supf a ) w
+z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where
+u<a : u o< a
+u<a = supf-inject ( osucprev (begin
+osuc (supf u)  ≡⟨ cong osuc su=u ⟩
+osuc u  ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩
+z  ≤⟨ z≤sa ⟩
+supf a ∎ )) where open o≤-Reasoning O
 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
 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> zc45 c ) ---   supf0 px o≤ supf1 x ≡ sp1
 zc40 : f (supf0 px) ≤ supf0 px
 zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39)
 ( MinSUP.x≤sup sup1 (case2 ⟪ fsuc _ (init (ZChain.asupf zc) refl) , subst (λ k → k o< x) (sym zc37) px<x ⟫  ))
+supfeq1 : {a b : Ordinal } → a o≤ x →  b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b
+supfeq1 {a} {b} a≤z b≤z ua=ub with trio< (supf1 a) (supf1 b)
+... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
+IsMinSUP.minsup (is-minsup b≤z) asupf1 (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb )
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> (
+IsMinSUP.minsup (is-minsup a≤z) asupf1 (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa )
+union-max1 : {a b : Ordinal } → x o≤ supf1 a → b o≤ x → supf1 a o< supf1 b → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b
+union-max1 {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where
+z47 : {w : Ordinal } → odef (UnionCF A f ay supf1 a ) w → odef ( UnionCF A f ay supf1 b ) w
+z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where
+u<b : u o< b
+u<b = ordtrans u<a (supf-inject0 supf1-mono sa<sb )
+z48 : {w : Ordinal } → odef (UnionCF A f ay supf1 b ) w → odef ( UnionCF A f ay supf1 a ) w
+z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where
+u<a : u o< a
+u<a = supf-inject0 supf1-mono ( osucprev (begin
+osuc (supf1 u)  ≡⟨ cong osuc su=u ⟩
+osuc u  ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩
+x  ≤⟨ z≤sa ⟩
+supf1 a ∎ )) where open o≤-Reasoning O
 order : {a b : Ordinal} {w : Ordinal} →
 b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
 order {a} {b} {w} b≤x sa<sb fc = z20 where
 a<b : a o< b
 a<b = supf-inject0 supf1-mono sa<sb
 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb)
 (fcup fc (o<→≤ (ordtrans a<b b<px)))
 ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26  where
 z26 : odef ( UnionCF A f ay supf0 b ) w
 z26 with x<y∨y≤x (supf1 a) b
-... | case2 b≤sa = ?
+... | case2 b≤sa = ⊥-elim ( o<¬≡ ( supfeq1  ? ? ( union-max1 ? ? (subst (λ k → supf1 a o< k) ? sa<sb) ))
+(ordtrans<-≤ sa<sb (o≤-refl0 (sym (sf1=sf0 ?)) )))
 ... | case1 sa<b with cfcs a<b b≤x sa<b fc
 ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫
 ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u ? ? ? ⟫
 ... | tri> ¬a ¬b px<b with x<y∨y≤x (supf1 a) b
 ... | case1 sa<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc)))
-... | case2 b≤sa = ? -- x=b  x o≤ sa   UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥
+... | case2 b≤sa = ⊥-elim ( o<¬≡ ? sa<sb ) where -- x=b  x o≤ sa   UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥
+b=x : b ≡ x
+b=x with trio< b x
+... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<b , zc-b<x _ a ⟫   ) -- px o< b o< x
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) -- x o< b ≤ x
+z27 : supf1 a ≡ supf1 b
+z27 = supfeq1  ? ? ( union-max1 ? ? sa<sb )
 ... | no lim with trio< x o∅
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
 ... | tri≈ ¬a b ¬c = record { supf = ? ; sup=u = ? ; asupf = ? ; supf-mono = ? ; order = ?
 ; supfmax = ? ; is-minsup = ? ; cfcs = ?    }

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

comparison src/zorn.agda @ 1053:a281ad683577