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

comparison src/zorn.agda @ 1046:e99e2bcb885c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 05 Dec 2022 15:09:41 +0900
parents 022d2ef3f20b
children aebab71cc386
comparison
equal deleted inserted replaced
1045:022d2ef3f20b 1046:e99e2bcb885c
330 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) 330 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f)
331 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where 331 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where
332 field 332 field
333 supf : Ordinal → Ordinal 333 supf : Ordinal → Ordinal
334 334
335 order : {x y w : Ordinal } → y o≤ z → x o< y → supf x o< z → FClosure A f (supf x) w → w ≤ supf y 335 cfcs : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w
336 336 order : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b
337 cfcs : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w
338 337
339 asupf : {x : Ordinal } → odef A (supf x) 338 asupf : {x : Ordinal } → odef A (supf x)
340 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y 339 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y
341 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z 340 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
342 341
395 f-total : IsTotalOrderSet chain 394 f-total : IsTotalOrderSet chain
396 f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = 395 f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ =
397 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso fc-total where 396 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso fc-total where
398 fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 397 fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
399 fc-total with trio< ua ub 398 fc-total with trio< ua ub
400 ... | tri< a₁ ¬b ¬c with ≤-ftrans (order (o<→≤ sub<x) a₁ (subst (λ k → k o< z) (sym sua=ua) sua<x) fca ) (s≤fc (supf ub) f mf fcb ) 399 ... | tri< a₁ ¬b ¬c with ≤-ftrans (order (o<→≤ sub<x) (subst₂ (λ j k → j o< k) (sym sua=ua) (sym sub=ub) a₁) fca ) (s≤fc (supf ub) f mf fcb )
401 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where 400 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
402 ct00 : * (& a) ≡ * (& b) 401 ct00 : * (& a) ≡ * (& b)
403 ct00 = cong (*) eq1 402 ct00 = cong (*) eq1
404 ... | case2 a<b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt) 403 ... | case2 a<b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)
405 fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb 404 fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb
406 fc-total | tri> ¬a ¬b c with ≤-ftrans (order (o<→≤ sua<x) c (subst (λ k → k o< z) (sym sub=ub) sub<x) fcb ) (s≤fc (supf ua) f mf fca ) 405 fc-total | tri> ¬a ¬b c with ≤-ftrans (order (o<→≤ sua<x) (subst₂ (λ j k → j o< k) (sym sub=ub) (sym sua=ua) c) fcb ) (s≤fc (supf ua) f mf fca )
407 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where 406 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
408 ct00 : * (& a) ≡ * (& b) 407 ct00 : * (& a) ≡ * (& b)
409 ct00 = cong (*) (sym eq1) 408 ct00 = cong (*) (sym eq1)
410 ... | case2 b<a = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a 409 ... | case2 b<a = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a
411 f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = ft00 where 410 f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = ft00 where
452 451
453 supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b 452 supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b
454 supf-idem {b} b≤z sfb≤x = z52 where 453 supf-idem {b} b≤z sfb≤x = z52 where
455 z54 : {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b) 454 z54 : {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
456 z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc 455 z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
457 z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z u<b (ordtrans<-≤ (subst (λ k → k o< b) (sym su=u) u<b) b≤z) fc where 456 z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z (subst (λ k → k o< supf b) (sym su=u) u<x) fc where
458 u<b : u o< b 457 u<b : u o< b
459 u<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x ) 458 u<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
460 z52 : supf (supf b) ≡ supf b 459 z52 : supf (supf b) ≡ supf b
461 z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf ; x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 460 z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf ; x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫
462 461
653 is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev 652 is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev
654 ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ 653 ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫
655 ... | ⟪ ab0 , ch-is-sup u u<x su=u fc ⟫ = ⟪ ab , subst (λ k → UChain ay x k ) 654 ... | ⟪ ab0 , ch-is-sup u u<x su=u fc ⟫ = ⟪ ab , subst (λ k → UChain ay x k )
656 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x su=u (fsuc _ fc)) ⟫ 655 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x su=u (fsuc _ fc)) ⟫
657 656
658
659 supf = ZChain.supf zc 657 supf = ZChain.supf zc
660 658
661 zc1 : (x : Ordinal ) → x o≤ & A → ZChain1 A f mf< ay zc x 659 zc1 : (x : Ordinal ) → x o≤ & A → ZChain1 A f mf< ay zc x
662 zc1 x x≤A with Oprev-p x 660 zc1 x x≤A with Oprev-p x
663 ... | yes op = record { is-max = is-max } where 661 ... | yes op = record { is-max = is-max } where
857 sfpx≤sp1 spx<x = MinSUP.x≤sup sup1 (case2 ⟪ init (ZChain.asupf zc {px}) refl , spx<x ⟫ ) 855 sfpx≤sp1 spx<x = MinSUP.x≤sup sup1 (case2 ⟪ init (ZChain.asupf zc {px}) refl , spx<x ⟫ )
858 856
859 m13 : supf0 px o< x → supf0 px o≤ sp1 857 m13 : supf0 px o< x → supf0 px o≤ sp1
860 m13 spx<x = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1) m14 where 858 m13 spx<x = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1) m14 where
861 m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1) 859 m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1)
862 m14 {z} ⟪ as , ch-init fc ⟫ = ≤-ftrans (ZChain.fcy<sup zc o≤-refl fc) (sfpx≤sp1 spx<x) 860 m14 {z} uz = MinSUP.x≤sup sup1 (case1 uz)
863 m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ =
864 ≤-ftrans (ZChain.order zc o≤-refl u<x (subst (λ k → k o< px) (sym (su=u)) u<x ) fc) (sfpx≤sp1 spx<x )
865 861
866 zc41 : ZChain A f mf< ay x 862 zc41 : ZChain A f mf< ay x
867 zc41 = record { supf = supf1 ; sup=u = sup=u ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order 863 zc41 = record { supf = supf1 ; sup=u = sup=u ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order
868 ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where 864 ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where
869 865
1094 z25 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = sup ⟪ ua , ch-is-sup u u<x 1090 z25 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = sup ⟪ ua , ch-is-sup u u<x
1095 (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where 1091 (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where
1096 u≤px : u o≤ px 1092 u≤px : u o≤ px
1097 u≤px = ordtrans u<x z≤px 1093 u≤px = ordtrans u<x z≤px
1098 1094
1099 order1 : {a b : Ordinal} {w : Ordinal} →
1100 b o≤ x → a o< b → supf1 a o< x → FClosure A f (supf1 a) w → w ≤ supf1 b
1101 order1 {a} {b} {w} b≤x a<b sa<x fc with cfcs a<b b≤x ? fc
1102 ... | t = ?
1103
1104 order : {a b : Ordinal} {w : Ordinal} → 1095 order : {a b : Ordinal} {w : Ordinal} →
1105 b o≤ x → a o< b → supf1 a o< x → FClosure A f (supf1 a) w → w ≤ supf1 b 1096 b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
1106 order {a} {b} {w} b≤x a<b sa<x fc with trio< b px 1097 order {a} {b} {w} b≤x sa<sb fc with osuc-≡< b≤x
1107 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b ? (fcup fc (o<→≤ (ordtrans a<b b<px) )) 1098 ... | case2 b<x =
1108 ... | tri≈ ¬a b=px ¬c = ZChain.order zc (o≤-refl0 b=px) a<b ? (fcup fc (o<→≤ (subst (λ k → a o< k) b=px a<b ))) 1099 subst ( λ k → w ≤ k ) (sym (sf1=sf0 ?)) ( ZChain.order zc (zc-b<x _ b<x)
1109 ... | tri> ¬a ¬b px<b with trio< a px 1100 (subst₂ (λ j k → j o< k ) (sf1=sf0 ?) (sf1=sf0 ?) sa<sb) (fcup fc ?) )
1110 ... | tri< a<px ¬b ¬c = ≤-ftrans (ZChain.order zc o≤-refl a<px ? fc) (sfpx≤sp1 ? ) -- supf1 a ≡ supf0 a 1101 ... | case1 eq with zc43 (supf1 a) b
1111 ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 ( 1102 ... | case1 sa<b = subst (λ k → w ≤ k ) (sym (sf1=sp1 ? )) ( MinSUP.x≤sup sup1 ?) where
1112 case2 ⟪ (subst (λ k → FClosure A f (supf0 k) w) a=px fc ) , subst (λ k → supf0 k o< x) a=px sa<x ⟫ ) 1103 z26 : odef pchainpx w
1113 ... | tri> ¬a ¬b px<a = ⊥-elim (¬p<x<op ⟪ px<a , zc22 ⟫ ) where -- supf1 a ≡ sp1 1104 z26 = zc11 (chain-mono f mf ay supf1 supf1-mono ? (cfcs ? b≤x ? fc))
1114 zc22 : a o< osuc px 1105 ... | case2 b≤sa = ⊥-elim ( o≤> z27 sa<sb ) where
1115 zc22 = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x) 1106 z28 : supf1 (supf0 a) ≡ supf1 a -- x o≤ supf1 a →
1107 z28 with zc43 (supf0 a) x
1108 ... | case1 sa<x = subst₂ (λ j k → j ≡ k) ? ? ( ZChain.supf-idem zc ? ? )
1109 ... | case2 x≤sa with osuc-≡< ( supf1-mono x≤sa ) -- = ? -- sp1 ≡ supf0 a --- sp1 o≤ supf0 a
1110 ... | case1 eq = sym (trans z29 eq ) where
1111 z30 : supf1 (supf0 a) ≡ supf1 (supf0 a)
1112 z30 = ?
1113 z29 : supf1 a ≡ supf1 x
1114 z29 = ?
1115 z32 : supf1 x ≡ supf1 (supf0 a) -- supf1 (supf0 a) ≡ supf1 a
1116 z32 = eq
1117 ... | case2 lt = ? where
1118 z31 : supf1 x o< supf1 (supf0 a)
1119 z31 = lt
1120
1121 z27 : supf1 b o≤ supf1 a
1122 z27 = begin
1123 supf1 b ≤⟨ ? ⟩
1124 supf1 (supf1 a) ≡⟨ ? ⟩
1125 supf1 a ∎ where open o≤-Reasoning O
1116 1126
1117 sup=u : {b : Ordinal} (ab : odef A b) → 1127 sup=u : {b : Ordinal} (ab : odef A b) →
1118 b o≤ x → IsSUP A (UnionCF A f ay supf1 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf1 b) f b ) → supf1 b ≡ b 1128 b o≤ x → IsSUP A (UnionCF A f ay supf1 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf1 b) f b ) → supf1 b ≡ b
1119 sup=u {b} ab b≤x is-sup with trio< b px 1129 sup=u {b} ab b≤x is-sup with trio< b px
1120 ... | tri< a ¬b ¬c = ? -- ZChain.sup=u zc ab (o<→≤ a) is-sup 1130 ... | tri< a ¬b ¬c = ? -- ZChain.sup=u zc ab (o<→≤ a) is-sup
1176 ptotalx : IsTotalOrderSet pchainx 1186 ptotalx : IsTotalOrderSet pchainx
1177 ptotalx {a} {b} ia ib = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 1187 ptotalx {a} {b} ia ib = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
1178 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 1188 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
1179 uz01 with trio< (IChain.i ia) (IChain.i ib) 1189 uz01 with trio< (IChain.i ia) (IChain.i ib)
1180 ... | tri< ia<ib ¬b ¬c with 1190 ... | tri< ia<ib ¬b ¬c with
1181 ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ia<ib ? (ifc≤ ia ib (o<→≤ ia<ib))) (s≤fc _ f mf (IChain.fc ib)) 1191 ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ? (ifc≤ ia ib (o<→≤ ia<ib))) (s≤fc _ f mf (IChain.fc ib))
1182 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where 1192 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
1183 ct00 : * (& a) ≡ * (& b) 1193 ct00 : * (& a) ≡ * (& b)
1184 ct00 = cong (*) eq1 1194 ct00 = cong (*) eq1
1185 ... | case2 lt = tri< lt (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1) 1195 ... | case2 lt = tri< lt (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1)
1186 uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib)) 1196 uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib))
1187 uz01 | tri> ¬a ¬b ib<ia with 1197 uz01 | tri> ¬a ¬b ib<ia with
1188 ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ? ib<ia ? (ifc≤ ib ia (o<→≤ ib<ia))) (s≤fc _ f mf (IChain.fc ia)) 1198 ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ? ? (ifc≤ ib ia (o<→≤ ib<ia))) (s≤fc _ f mf (IChain.fc ia))
1189 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where 1199 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
1190 ct00 : * (& a) ≡ * (& b) 1200 ct00 : * (& a) ≡ * (& b)
1191 ct00 = sym (cong (*) eq1) 1201 ct00 = sym (cong (*) eq1)
1192 ... | case2 lt = tri> (λ lt1 → <-irr (case2 lt) lt1) (λ eq → <-irr (case1 eq) lt) lt 1202 ... | case2 lt = tri> (λ lt1 → <-irr (case2 lt) lt1) (λ eq → <-irr (case1 eq) lt) lt
1193 1203