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

comparison src/zorn.agda @ 1018:c63f1fadd27f

sa<b

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Thu, 24 Nov 2022 11:18:46 +0900
parents	ffdfd8d1303a
children	eb2d0fb19b67

comparison

equal deleted inserted replaced

-:ffdfd8d1303a
+:c63f1fadd27f
 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
 cfcs : (mf< : <-monotonic-f A f)
-{a b w : Ordinal } → a o< b → b o≤ z → supf a o< z  → FClosure A f (supf a) w → odef (UnionCF A f mf ay supf z) w
+{a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → 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
 supf-idem  mf< {b} b≤z sfb≤x = z52 where
 z54 :  {w : Ordinal} → odef (UnionCF A f mf ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
 z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
 z54 {w} ⟪ aw , ch-is-sup u u<x is-sup fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k ))
 (sym (supf-is-minsup b≤z))
-(MinSUP.x≤sup (minsup b≤z) ?) where
+(MinSUP.x≤sup (minsup b≤z) (cfcs mf< u<b b≤z ? fc )) where
 u<b : u o< b
 u<b = supf-inject ( subst (λ k → k o< supf b) (sym (ChainP.supu=u is-sup)) u<x )
 su<z : supf u o< z
 su<z = subst (λ k → k o< z ) (sym (ChainP.supu=u is-sup)) ( ordtrans<-≤ u<b b≤z )
 z52 : supf (supf b) ≡ supf b
 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.cfcs zc mf< b<x x≤A (ZChain.supf<A zc) fc
+m13 = ZChain.cfcs zc mf< b<x x≤A ? fc
 ... | 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 →
 b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
 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.cfcs zc mf< b<x x≤A (ZChain.supf<A zc) fc
+m13 = ZChain.cfcs zc mf< b<x x≤A ? 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 ))) }
 fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc
 -- this is a kind of maximality, so we cannot prove this without <-monotonicity
 --
 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal }
-→ a o< b → b o≤ x → supf1 a o< x  → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 x) w
+→ a o< b → b o≤ x → supf1 a o< b  → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
-cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with zc43 (supf0 a) px
+cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with zc43 (supf0 a) px
 ... | case2 px≤sa = z50 where
 a≤px : a o≤ px
 a≤px = subst (λ k → a o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)
 --  supf0 a ≡ px we cannot use previous cfcs, it is in the chain because
 --       supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x
-z50 : odef (UnionCF A f mf ay supf1 x) w
+z50 : odef (UnionCF A f mf ay supf1 b) w
 z50 with osuc-≡< px≤sa
 ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) ? ? (subst (λ k → FClosure A f k w) ? fc)  ⟫
-... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) sa<x ⟫  )
+... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) ? ⟫  )
 ... | case1 sa<px with trio< a px
 ... | tri< a<px ¬b ¬c = z50 where
-z50 : odef (UnionCF A f mf ay supf1 x) w
+z50 : odef (UnionCF A f mf ay supf1 b) w
 z50 with osuc-≡< b≤x
-... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<px fc
+... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) ? fc
 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-... | ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ⟪ az , ch-is-sup u ? cp1 (fcpu fc u≤px )  ⟫  where -- u o< px → u o< b ?
+... | ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc u≤px )  ⟫  where -- u o< px → u o< b ?
 u≤px : u o≤ px
-u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op))  (ordtrans<-≤ u<b ? )
+u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op))  (ordtrans<-≤ u<b b≤x )
 u<x : u o< x
-u<x = ordtrans<-≤ u<b ? --b≤x
+u<x = ordtrans<-≤ u<b b≤x
 cp1 : ChainP A f mf ay supf1 u
 cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) (ChainP.fcy<sup is-sup fc )
 ; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x)
 (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) ))
 (sym (sf=eq u<x)) s<u)
 (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc ))
 ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup)  }
 z50 | case1 eq with ZChain.cfcs zc mf< a<px o≤-refl sa<px fc
 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u ? cp1 (fcpu fc (o<→≤ u<px)) ⟫  where -- u o< px → u o< b ?
+... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc (o<→≤ u<px)) ⟫  where -- u o< px → u o< b ?
 u<b : u o< b
 u<b = subst (λ k → u o< k ) (trans (Oprev.oprev=x op) (sym eq) ) (ordtrans u<px <-osuc )
 u<x : u o< x
 u<x = subst (λ k → u o< k ) (Oprev.oprev=x op) ( ordtrans u<px <-osuc )
 cp1 : ChainP A f mf ay supf1 u
 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) --   x o< b
 z51 : FClosure A f (supf1 px) w
 z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc
 z53 : odef A w
 z53 = A∋fc {A} _ f mf fc
-csupf1 : odef (UnionCF A f mf ay supf1 x) w
+csupf1 : odef (UnionCF A f mf ay supf1 b) w
 csupf1 with trio< (supf0 px) x
-... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx ? cp1 fc1 ⟫  where
+... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) cp1 fc1 ⟫  where
 spx = supf0 px
 spx≤px : supf0 px o≤ px
 spx≤px = zc-b<x _ sfpx<x
 z52 : supf1 (supf0 px) ≡ supf0 px
 z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc mf< o≤-refl (zc-b<x _ sfpx<x ) )
 fc1 : FClosure A f (supf1 spx) w
 fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc
 order : {s z1 : Ordinal} → supf1 s o< supf1 spx → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 spx) ∨ (z1 << supf1 spx)
 order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k ))
 (trans (sym (ZChain.supf-is-minsup zc spx≤px )) (sym (sf1=sf0 spx≤px) ) )
-(MinSUP.x≤sup (ZChain.minsup zc spx≤px) ? )  where
+(MinSUP.x≤sup (ZChain.minsup zc spx≤px) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx)
--- (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx)
+spx≤px ? (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) ))) where
---    spx≤px ss<px (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) ))) where
 ss<px : supf0 s o< px
 ss<px = osucprev ( begin
 osuc (supf0 s)  ≡⟨ cong osuc (sym (sf1=sf0 ( begin
 s <⟨ supf-inject0 supf1-mono ss<spx ⟩
 supf0 px  ≤⟨ spx≤px ⟩
 --  supf0 px not is included by the chain
 --     supf1 x ≡ supf0 px because of supfmax
 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal }
-→ a o< b → b o≤ x →  supf0 a o< x → FClosure A f (supf0 a) w → odef (UnionCF A f mf ay supf0 x) w
+→ a o< b → b o≤ x →  supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f mf ay supf0 b) w
-cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with trio< b px
+cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with trio< b px
-... | tri< a ¬b ¬c = ? -- ZChain.cfcs zc mf< a<b (o<→≤ a) ? fc
+... | tri< a ¬b ¬c = ZChain.cfcs zc mf< a<b (o<→≤ a) ? fc
-... | tri≈ ¬a refl ¬c = ? -- ZChain.cfcs zc mf< a<b o≤-refl ? fc
+... | tri≈ ¬a refl ¬c = ZChain.cfcs zc mf< a<b o≤-refl ? fc
 ... | tri> ¬a ¬b px<b with trio< a px
-... | tri< a ¬b ¬c = ? -- chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) ( ZChain.cfcs zc mf< a o≤-refl ? fc )
+... | tri< a ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) ( ZChain.cfcs zc mf< a o≤-refl ? fc )
 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ? c )
 ... | tri≈ ¬a refl ¬c = ? --  supf0 px o< x  → odef (UnionCF A f mf ay supf0 x) (supf0 px)
 --  x o≤ supf0 px o≤ sp  →
 zc17 : {z : Ordinal } → supf0 z o≤ supf0 px
 ... | tri< a ¬b ¬c = ?
 ... | tri≈ ¬a b ¬c = ?
 ... | tri> ¬a ¬b c = ?
 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal }
-→ a o< b → b o≤ x →  supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 x) w
+→ a o< b → b o≤ x →  supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
-cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with osuc-≡< b≤x
+cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x
 ... | case1 b=x with trio< a x
 ... | tri< a<x ¬b ¬c = zc40 where
 sa = ZChain.supf (pzc  (ob<x lim a<x)) a
 m =  omax a sa
 m<x : m o< x
 m<x with trio< a sa | inspect (omax a) sa
-... | tri< a<sa ¬b ¬c | record { eq = eq } = ob<x lim sa<x
+... | tri< a<sa ¬b ¬c | record { eq = eq } = ob<x lim ?
 ... | tri≈ ¬a a=sa ¬c | record { eq = eq } = subst (λ k → k o< x) eq zc41 where
 zc41 : omax a sa o< x
 zc41 = osucprev ( begin
 osuc ( omax a sa ) ≡⟨ cong (λ k → osuc (omax a k)) (sym a=sa) ⟩
 osuc ( omax a a ) ≡⟨ cong osuc (omxx _) ⟩
 sam<m = subst (λ k → k o< m ) (supf-unique A f mf ay zc42 (pzc (ob<x lim a<x)) (pzc (ob<x lim m<x)) (o<→≤ <-osuc)) ( omax-y _ _ )
 fcm : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) a) w
 fcm = subst (λ k → FClosure A f k w ) (zeq (ob<x lim a<x) (ob<x lim m<x) zc42 (o<→≤ <-osuc) ) fc
 zcm : odef (UnionCF A f mf ay (ZChain.supf (pzc  (ob<x lim m<x))) (osuc (omax a sa))) w
 zcm = ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
-zc40 : odef (UnionCF A f mf ay supf1 x) w
+zc40 : odef (UnionCF A f mf ay supf1 b) w
 zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u ? ? fc2 ⟫  where -- u o< px → u o< b ?
+... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<b ? fc2 ⟫  where -- u o< px → u o< b ?
 zc55 : u o< osuc m
 zc55 = u<x
 u<b : u o< b --      b o≤ u → b o≤ a -- u ≡ supf1 a
 u<b = subst (λ k → u o< k ) (sym b=x) ( ordtrans u<x (ob<x lim m<x))
 fc1m : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) u) w
 fc2 = subst (λ k → FClosure A f k w) (trans (sym (zeq _ _ zc57 (o<→≤ <-osuc))) (sym (sf1=sf (ordtrans≤-< u<x m<x))) )  fc1 where
 zc57 : osuc u o≤ osuc m
 zc57 = osucc u<x
 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
-cfcs mf< {a} {b} {w} a<b b≤x sa<x fc | case2 b<x = zc40 where
+cfcs mf< {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where
 supfb =  ZChain.supf (pzc (ob<x lim b<x))
 fcb : FClosure A f (supfb a) w
 fcb = ?
 --  supfb a o≤ supfb b
---  supfb (supfb a) o≤ supfb b
 sa<b : supfb a o< osuc b
 sa<b = ?
-zcb : odef (UnionCF A f mf ay supfb x) w
+zcb : odef (UnionCF A f mf ay supfb b) w
-zcb = ? -- ZChain.cfcs (pzc (ob<x lim b<x)) mf< a<b (o<→≤ <-osuc) sa<b fcb
+zcb = ZChain.cfcs (pzc (ob<x lim b<x)) mf< a<b (o<→≤ <-osuc) ? fcb
-zc40 : odef (UnionCF A f mf ay supf1 x) w
+zc40 : odef (UnionCF A f mf ay supf1 b) w
 zc40 with zcb
 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
 ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<x ? ? ⟫
 ---

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

comparison src/zorn.agda @ 1018:c63f1fadd27f