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

comparison src/zorn.agda @ 761:9307f895891c

edge case done

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 25 Jul 2022 08:29:15 +0900
parents	0dc7999b1d50
children	eb68d0870cc6

comparison

equal deleted inserted replaced

-:0dc7999b1d50
+:9307f895891c
 initial : {y : Ordinal } → odef chain y → * init ≤ * y
 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
 f-total : IsTotalOrderSet chain
 csupf : {z : Ordinal } → odef chain (supf z)
-sup=u : {b : Ordinal} → {ab : odef A b} → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b
+sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b
 fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → w << supf u     -- different from order because y o< supf
-order : {b sup1 z1 : Ordinal} → b o< z → sup1 o≤ b → FClosure A f (supf sup1) z1 → z1 << supf b
+order : {b sup1 z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f (supf sup1) z1 → z1 << supf b
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {init : Ordinal} (ay : odef A init)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
 field
 px<x = subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc
 m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
 m01 with trio< b px    --- px  < b < x
 ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫)
 ... | tri< b<px ¬b ¬c = chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl m04 where
-m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a
+m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a -- if a ∈ chain of px, is-max of px can be used
 m03 with proj2 ua
 ... | ch-init fc = ⟪ proj1 ua ,  ch-init fc ⟫
-... | ch-is-sup u u≤x is-sup fc with trio< u px
+... | ch-is-sup u u≤x is-sup-a fc with trio< u px
-... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u (o<→≤ a) is-sup fc ⟫ -- u o< osuc x
+... | tri< a ¬b ¬c    = ⟪ proj1 ua , ch-is-sup u (o<→≤ a) is-sup-a fc ⟫ -- u o< osuc x
-... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u (o≤-refl0 u=px) is-sup fc ⟫
+... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u (o≤-refl0 u=px) is-sup-a fc ⟫
-... | tri> ¬a ¬b c = ?   -- u = x → u = sup →  (b o< x →  b  < a ) → ⊥
+... | tri> ¬a ¬b c = ⊥-elim (<-irr u≤a (ptrans a<b b<u) ) where
+su=u : ZChain.supf zc u ≡ u
+su=u = ChainP.supfu=u is-sup-a
+u<A : u o< & A
+u<A = z09 (subst (λ k → odef A k ) su=u (proj1 (ZChain.csupf zc )))
+u≤a : (* u ≡ * a) ∨ (u << a)
+u≤a = s≤fc u f mf (subst (λ k → FClosure A f k a) su=u fc )
+m07 : osuc b o≤ x
+m07 = osucc (ordtrans b<px px<x )
+fcb : FClosure A f (ZChain.supf zc b) b
+fcb = subst (λ k → FClosure A f k b ) (sym (ZChain.sup=u zc ab (z09 ab)
+(record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x m07 o≤-refl lt)  } ) )) ( init ab )
+b<u : b << u
+b<u = subst (λ k → b << k ) su=u ( ZChain.order zc u<A (ordtrans b<px c)  fcb )
 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
 m04 = ZChain1.is-max (prev px px<x) m03 b<px ab
 (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b (o<→≤ b<x) m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫   where
 m06 : ChainP A f mf ay (ZChain.supf zc) b b
 m06 = ?
 m05 : b ≡ ZChain.supf zc b
-m05 = sym ( ZChain.sup=u zc {b} {ab} (z09 ab)
+m05 = sym ( ZChain.sup=u zc ab (z09 ab)
 record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono2 x (osucc b<x) o≤-refl uz )  }  )
--- b = px case,  u = px  u< osuc x
 ... | no lim = record { is-max = is-max }  where
 is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
 b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
 m09 : b o< & A
 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
 m07 : {z : Ordinal} → FClosure A f y z → z << ZChain.supf zc b
 m07 {z} fc = ZChain.fcy<sup zc m09 fc
 m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
-m08 {sup1} {z1} s<b fc = ZChain.order zc m09 (o<→≤ s<b) fc
+m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
 m05 : b ≡ ZChain.supf zc b
-m05 = sym (ZChain.sup=u zc {_} {ab} m09
+m05 = sym (ZChain.sup=u zc ab m09
 record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ (ob<x lim b<x)) o≤-refl lt )} )   -- ZChain on x
 m06 : ChainP A f mf ay (ZChain.supf zc) b b
 m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08
 ; supfu=u = sym m05 }
 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
 →  SUP A (uchain f mf ay)
 ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay)
 inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
 inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; csupf = ? ; fcy<sup = ?
-; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
+; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
 isupf : Ordinal → Ordinal
 isupf z =  & (SUP.sup (ysup f mf ay))
 cy : odef (UnionCF A f mf ay isupf o∅) y
 cy = ⟪ ay , ch-init (init ay)  ⟫
 y<sup : * y ≤ SUP.sup (ysup f mf ay)

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

comparison src/zorn.agda @ 761:9307f895891c