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

comparison src/zorn.agda @ 1012:6f6daf464616

maxα

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Wed, 23 Nov 2022 09:55:38 +0900
parents	66154af40f89
children	2362c2d89d36

comparison

equal deleted inserted replaced

-:66154af40f89
+:6f6daf464616
 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
 -- this is a kind of maximality, so we cannot prove this without <-monotonicity
 --
---  supf0 a ≡ px we cannot use previous cfcs, it is in the chain because
---       supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x
---
 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 b) w
-cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with trio< a px
+cfcs mf< {a} {b} {w} a<b b≤x sa<x 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 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 ⟫  )
+... | case1 sa<px with trio< a px
 ... | tri< a<px ¬b ¬c = z50 where
 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) ? fc
+... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<px fc
 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
 ... | ⟪ 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 b≤x )
 u<x : u o< x
 ; 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 ? fc
+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 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
 ... | 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 ? )
+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) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx)
-spx≤px ? (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) )))
+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 ⟩
+px ∎ ) )) ⟩
+osuc (supf1 s)  ≤⟨ osucc ss<spx ⟩
+supf1 spx  ≡⟨ sf1=sf0 spx≤px  ⟩
+supf0 spx  ≤⟨ ZChain.supf-mono zc spx≤px ⟩
+supf0 px  ≤⟨ spx≤px ⟩
+px ∎  ) where open o≤-Reasoning O
 cp1 : ChainP A f mf ay supf1 spx
 cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 spx≤px ))
 ( ZChain.fcy<sup zc spx≤px fc )
 ; order =  order
 ; supu=u = z52 }
 pchainx : HOD
 pchainx = record { od = record { def = λ z → IChain A f supfz z } ; odmax = & A ; <odmax = zc00 } where
 zc00 : {z : Ordinal } → IChain A f supfz z → z o< & A
 zc00 {z} ic = z09 ( A∋fc (supfz (IChain.i<x ic)) f mf (IChain.fc ic) )
+aic : {z : Ordinal } → IChain A f supfz z → odef A z
+aic {z} ic = ?
 zeq : {xa xb z : Ordinal }
 → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa
 → ZChain.supf (pzc  xa<x) z ≡  ZChain.supf (pzc  xb<x) z
 zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa =  spuf-unique A f mf ay xa≤xb
 (pzc xa<x)  (pzc xb<x)  z≤xa
 ... | tri< a ¬b ¬c = ?
 ... | tri≈ ¬a b ¬c = ?
 ... | tri> ¬a ¬b c = ?
 zc5 : ZChain A f mf ay x
-zc5 with zc43 x spu
+zc5 = ? where
-zc5 | (case2 sp≤x ) =  ? where
+cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal }
-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 b) w
-cfcs mf< {a} {b} {w} a<b b≤x sa<x fc = ?
+cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with trio< a x
-zc5 | (case1 x<sp ) =  ? where
+... | tri< a<x ¬b ¬c = ? where
-cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal }
+sa = ZChain.supf (pzc  (ob<x lim a<x)) a
-→ 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
+m =  omax a sa
-cfcs mf< {a} {b} {w} a<b b≤x sa<x fc = ?
+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 b ¬c | record { eq = eq } = subst ( λ k → k o< x ) ( begin
+sa ≡⟨ ? ⟩
+? ≡⟨ sym eq ⟩
+_ ∎ ) ( ob<x lim sa<x ) where open ≡-Reasoning
+... | tri> ¬a ¬b c | record { eq = eq } = ob<x lim a<x
+zc40 : odef (UnionCF A f mf ay supf1 b) w
+zc40 with ZChain.cfcs (pzc  (ob<x lim sa<x)) mf< ? o≤-refl ? ?
+... | t = ?
+... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
+... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
 ---
 --- the maximum chain  has fix point of any ≤-monotonic function
 ---

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

comparison src/zorn.agda @ 1012:6f6daf464616