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

comparison src/zorn.agda @ 990:9672214d4e13

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Thu, 17 Nov 2022 00:04:52 +0900
parents	ce713b5db3f3
children	c190f708862a

comparison

equal deleted inserted replaced

-:ce713b5db3f3
+:9672214d4e13
 <=-trans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
 ftrans<=-< : {x y z : Ordinal } →  x <=  y →  y << z →  x <<  z
 ftrans<=-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) (sym (cong (*) eq))  y<z
 ftrans<=-< {x} {y} {z} (case2 lt) y<z = IsStrictPartialOrder.trans PO lt y<z
+ftrans<-<= : {x y z : Ordinal } →  x <<  y →  y <= z →  x <<  z
+ftrans<-<= {x} {y} {z} x<y (case1 eq) = subst (λ k → * x < k ) ((cong (*) eq)) x<y
+ftrans<-<= {x} {y} {z} x<y (case2 lt) = IsStrictPartialOrder.trans PO x<y lt
 <=to≤ : {x y : Ordinal } → x <= y → * x ≤ * y
 <=to≤ (case1 eq) = case1 (cong (*) eq)
 <=to≤ (case2 lt) = case2 lt
 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 )
 ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 --
---         f (f ( ... (sup y))) f (f ( ... (sup z1)))
+--         f (f ( ... (supf y))) f (f ( ... (supf z1)))
 --        /          |         /             |
 --       /           |        /              |
---    sup y   <       sup z1          <    sup z2
+--    supf y   <       supf z1          <    supf z2
 --           o<                      o<
+--
+--    if sup z1 ≡ sup z2, the chain is stopped at sup z1, then f (sup z1) ≡ sup z1
+fc-stop : ( A : HOD )    ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) { a b : Ordinal }
+→ (aa : odef A a ) →(  {y : Ordinal} → FClosure A f a y → (y ≡ b ) ∨ (y << b )) → a ≡ b → f a ≡ a
+fc-stop A f mf {a} {b} aa x≤sup a=b with x≤sup (fsuc a (init aa refl ))
+... | case1 eq = trans eq (sym a=b)
+... | case2 lt = ⊥-elim (<-irr (case1 (cong (λ k → * (f k) ) (sym a=b))) (ftrans<-<= lt (≤to<= fc00 )) ) where
+fc00 :  * b ≤ * (f b)
+fc00 = proj1 (mf _ (subst (λ k → odef A k) a=b aa ))
+--
 -- data UChain is total
 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
 {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
 chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
 {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
 field
 supf :  Ordinal → Ordinal
 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
 → IsSUP A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) f b ) → supf b ≡ b
+fcs<sup : {a b w : Ordinal } → a o< b → b o≤ z → FClosure A f (supf a) w → odef (UnionCF A f mf ay supf b) w
 asupf :  {x : Ordinal } → odef A (supf x)
 supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
 supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
 m09 {s} {z} s<b fcz = order b<A s<b fcz
 m06 : ChainP A f mf ay supf b
 m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
 ... | case1 sb=sx = ? where
+b<A : b o< & A
+b<A = z09 ab
 m09 : IsSUP A (UnionCF A f mf ay (ZChain.supf zc) b) ab
 m09 = proj2 is-sup
 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 } )
 m05 : ZChain.supf zc b ≡ b
 m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
 m07 : MinSUP A (UnionCF A f mf ay supf (supf x)) -- supf z o< supf ( supf x )
 m07 = ZChain.minsup zc (o<→≤ (z09 (ZChain.asupf zc)))
+m29 : x o≤ & A
+m29 = ?
+m15 : supf (supf x) ≡ MinSUP.sup m07
+m15 = ZChain.supf-is-minsup zc (o<→≤ (z09 (ZChain.asupf zc)))
+m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x )
+m17 = ZChain.minsup zc m29
+m18 : supf x ≡ MinSUP.sup m17
+m18 = ZChain.supf-is-minsup zc m29
+m10 : f (supf b) ≡ supf b
+m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
+m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
+m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
+m13 :  odef (UnionCF A f mf ay supf x) z
+m13 = ZChain.fcs<sup zc b<x m29  fc
+m12 :  odef (UnionCF A f mf ay supf (& A)) z
+m12 = ZChain.fcs<sup zc ? ?  fc
+-- m14 :  odef (UnionCF A f mf ay supf x) z
+-- m14 = ZChain.fcs<sup zc ? ?
 m08 : MinSUP A (UnionCF A f mf ay supf b)
 m08 = ZChain.minsup zc (o<→≤ (z09 ab))           -- supf z o< supf b
 ... | no lim = record { is-max = is-max ; order = order }  where
 is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
 * 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 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 = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+... | 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
 m09 : b o< & A
 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
-sb<sx : supf b o< supf x
-sb<sx  = ?
 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
 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
 m08 {s} {z1} s<b fc = order m09 s<b fc
 ; x=fy = HasPrev.x=fy nhp } )
 m05 : ZChain.supf zc b ≡ b
 m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
 m06 : ChainP A f mf ay supf b
 m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
+... | case1 sb=sx = ? where
+m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x )
+m17 = ZChain.minsup zc ?
+m18 : supf x ≡ MinSUP.sup m17
+m18 = ZChain.supf-is-minsup zc ?
+m10 : f (supf b) ≡ supf b
+m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
+m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
+m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
+m13 :  odef (UnionCF A f mf ay supf x) z
+m13 = ZChain.fcs<sup zc b<x ?  fc
 uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
 uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax =
 λ {z} cz → subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (A∋fc y f mf cz ))) }

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

comparison src/zorn.agda @ 990:9672214d4e13