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

comparison src/zorn.agda @ 1016:aeda5d0537d7

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Thu, 24 Nov 2022 08:48:38 +0900
parents	c804e302f110
children	ffdfd8d1303a

comparison

equal deleted inserted replaced

-:c804e302f110
+:aeda5d0537d7
 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
 z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫
-fc-inject : {x y : Ordinal }  →  (mf< : <-monotonic-f A f) → x o≤ z → y o≤ z → supf x o< z → supf y o< z
-→  { wx wy  : Ordinal} →  FClosure A f (supf x) wx  →  FClosure A f (supf y) wy → wx ≡ wy → supf x ≡ supf y
-fc-inject mf< x≤z y≤z sx<z sy<z = ? where
-z53 : {x y : Ordinal } →  supf x o< supf y → FClosure A f (supf x) wx  →  wx << supf y
-z53 = ?
 supf-unique :  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {y xa xb : Ordinal} → (ay : odef A y) →  (xa o≤ xb ) → (za : ZChain A f mf ay xa ) (zb : ZChain A f mf ay xb )
 → {z : Ordinal } → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z
 supf-unique A f mf {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa  where
 --
 -- maximality of chain
 --
 --     supf is fixed for z ≡ & A , we can prove order and is-max
---
+--     we have supf-unique now, it is provable in the first Tranfinte induction
 SZ1 : ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) (mf< : <-monotonic-f A f)
 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → x o≤ & A → ZChain1 A f mf ay zc x
 SZ1 f mf mf< {y} ay zc x x≤A = zc1 x x≤A  where
 chain-mono1 :  {a b c : Ordinal} → a o≤ b
 ... | refl = ⊥-elim (¬sp=x zcsup )
 zc31 (case2 hasPrev ) with zc30
 ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev
 ; ay = ? ; x=fy = HasPrev.x=fy hasPrev } )
-... | no lim = zc5 where
+... | no lim = ? where
 pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z
 pzc {z} z<x = prev z z<x
 ysp =  MinSUP.sup (ysup f mf ay)
 supf-mono {x} {y} x≤y with trio< y x
 ... | tri< a ¬b ¬c = ?
 ... | tri≈ ¬a b ¬c = ?
 ... | tri> ¬a ¬b c = ?
-zc5 : ZChain A f mf ay x
+cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal }
-zc5 = ? where
+→ a o< b → b o≤ x →  supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
-cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal }
+cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with osuc-≡< b≤x
-→ a o< b → b o≤ x →  supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
+... | case1 b=x with trio< a x
-cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with trio< a x
+... | tri< a<x ¬b ¬c = zc40 where
-... | tri< a<x ¬b ¬c = zc40 where
+sa = ZChain.supf (pzc  (ob<x lim a<x)) a
-sa = ZChain.supf (pzc  (ob<x lim a<x)) a
+m =  omax a sa
-m =  omax a sa
+m<x : m o< x
-m<x : m o< x
+m<x with trio< a sa | inspect (omax a) sa
-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 sa<x
+... | tri≈ ¬a a=sa ¬c | record { eq = eq } = subst (λ k → k o< x) eq zc41 where
-... | tri≈ ¬a a=sa ¬c | record { eq = eq } = subst (λ k → k o< x) eq zc41 where
+zc41 : omax a sa o< x
-zc41 : omax a sa o< x
+zc41 = osucprev ( begin
-zc41 = osucprev ( begin
+osuc ( omax a sa ) ≡⟨ cong (λ k → osuc (omax a k)) (sym a=sa) ⟩
-osuc ( omax a sa ) ≡⟨ cong (λ k → osuc (omax a k)) (sym a=sa) ⟩
+osuc ( omax a a ) ≡⟨ cong osuc (omxx _) ⟩
-osuc ( omax a a ) ≡⟨ cong osuc (omxx _) ⟩
+osuc ( osuc  a ) ≤⟨ o<→≤ (ob<x lim (ob<x lim a<x))  ⟩
-osuc ( osuc  a ) ≤⟨ o<→≤ (ob<x lim (ob<x lim a<x))  ⟩
+x ∎ ) where open o≤-Reasoning O
-x ∎ ) where open o≤-Reasoning O
+... | tri> ¬a ¬b c | record { eq = eq } = ob<x lim a<x
-... | tri> ¬a ¬b c | record { eq = eq } = ob<x lim a<x
+sam = ZChain.supf (pzc (ob<x lim m<x)) a
-sam = ZChain.supf (pzc (ob<x lim m<x)) a
+zc42 : osuc a o≤ osuc m
-zc42 : osuc a o≤ osuc m
+zc42 = osucc (o<→≤ ( omax-x _ _ ) )
-zc42 = osucc (o<→≤ ( omax-x _ _ ) )
+sam<m : sam o< m
-sam<m : sam o< m
+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 _ _ )
-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 : 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
-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
-zc40 : odef (UnionCF A f mf ay supf1 b) w
+zcm = ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
-zc40 with 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 b) w
-... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
+zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
-... | ⟪ 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 ?
+... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-zc55 : u o< osuc m
+... | ⟪ 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<x
+zc55 : u o< osuc m
-zc56 : u ≡ supf1 a
+zc55 = u<x
-zc56 = ?
+zc56 : u ≡ supf1 a
-u<b : u o< b --      b o≤ u → b o≤ a -- u ≡ supf1 a
+zc56 = ?
-u<b = ?
+u<b : u o< b --      b o≤ u → b o≤ a -- u ≡ supf1 a
-fc1m : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) u) w
+u<b = ?
-fc1m = fc1
+fc1m : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) u) w
-fc2 : FClosure A f (supf1 u) w
+fc1m = fc1
-fc2 = subst (λ k → FClosure A f k w) (trans (sym (zeq _ _ zc57 (o<→≤ <-osuc))) (sym (sf1=sf (ordtrans≤-< u<x m<x))) )  fc1 where
+fc1a : FClosure A f (ZChain.supf (pzc (ob<x lim a<x)) a) w
-zc57 : osuc u o≤ osuc m
+fc1a = fc
-zc57 = osucc u<x
+fc2 : FClosure A f (supf1 u) w
-fc1a : FClosure A f (ZChain.supf (pzc (ob<x lim a<x)) a) 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
-fc1a = fc
+zc57 : osuc u o≤ osuc m
-... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
+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))
+... | 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
+zcb : odef (UnionCF A f mf ay (ZChain.supf (pzc  (ob<x lim b<x))) b) w
+zcb = ZChain.cfcs (pzc (ob<x lim b<x)) mf< ? ? ? ?
+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 ? ? ? ⟫
 ---
 --- the maximum chain  has fix point of any ≤-monotonic function
 ---
 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf ay x

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

comparison src/zorn.agda @ 1016:aeda5d0537d7