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

comparison src/zorn.agda @ 690:33f90b483211

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Chain with chainf
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 11 Jul 2022 04:53:45 +0900
parents 34650e39e553
children 46d05d12df57
comparison
equal deleted inserted replaced
689:34650e39e553 690:33f90b483211
251 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p ))) 251 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
252 252
253 UnionCF : (A : HOD) (x : Ordinal) (chainf : (z : Ordinal ) → z o< x → HOD ) → HOD 253 UnionCF : (A : HOD) (x : Ordinal) (chainf : (z : Ordinal ) → z o< x → HOD ) → HOD
254 UnionCF A x chainf = record { od = record { def = λ z → odef A z ∧ UChain x chainf z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } 254 UnionCF A x chainf = record { od = record { def = λ z → odef A z ∧ UChain x chainf z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
255 255
256 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) : Ordinal → Ordinal → Set n where 256 --
257 ch-init : (z : Ordinal) → FClosure A f y z → Chain A f mf ay y z 257 -- sup and its fclosure is in a chain HOD
258 ch-is-sup : {x z : Ordinal } (init<x : y << x) (lty : y o< x ) ( ax : odef A x ) 258 -- chain HOD is sorted by sup as Ordinal and <-ordered
259 → ( is-sup : (x1 w : Ordinal) → ( x1 ≡ y ) ∨ ( (y << x1) ∧ (x1 o< x) ) → Chain A f mf ay x1 w → w << x ) 259 -- whole chain is a union of separated Chain
260 → ( fc : FClosure A f x z ) → Chain A f mf ay x z 260 -- minimum index is y not ϕ
261 --
262
263 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {x y : Ordinal} (ay : odef A y) (chainf : (z : Ordinal ) → z o< x → HOD) (sup z : Ordinal) : Set n where
264 field
265 asup : odef A sup
266 y<sup : y o< sup
267 y<<sup : y << sup
268 sup<x : sup o< x
269 csupz : odef (chainf sup sup<x) z
270 order : (sup1 z1 : Ordinal) → (lt : sup1 o< sup ) → odef (chainf sup1 (ordtrans lt sup<x ) ) z1 → z1 << z
271
272 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {x y : Ordinal} (ay : odef A y) (chainf : (z : Ordinal ) → z o< x → HOD) : Ordinal → Ordinal → Set n where
273 ch-init : (z : Ordinal) → FClosure A f y z → Chain A f mf ay chainf y z
274 ch-is-sup : {sup z : Ordinal }
275 → ( is-sup : ChainP A f mf ay chainf sup z)
276 → ( fc : FClosure A f sup z ) → Chain A f mf ay chainf sup z
261 277
262 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where 278 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
263 field 279 field
264 psup : Ordinal → Ordinal 280 psup : Ordinal → Ordinal
265 p≤z : (x : Ordinal ) → odef A (psup x) 281 p≤z : (x : Ordinal ) → odef A (psup x)
266 chainf : (x : Ordinal) → HOD 282 chainf : (x : Ordinal) → x o< z → HOD
267 is-chain : (x w : Ordinal) → odef (chainf x) w → Chain A f mf ay (psup x) w 283 is-chain : (x w : Ordinal) → (x<z : x o< z) → odef (chainf x x<z) w → Chain A f mf ay chainf (psup x) w
268 284
269 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) 285 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)
270 (zc0 : (x : Ordinal) → ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where 286 (zc0 : (x : Ordinal) → ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where
271 chain : HOD 287 chain : HOD
272 chain = UnionCF A (& A) ( λ x _ → ZChain1.chainf (zc0 (& A)) x ) 288 chain = UnionCF A (& A) ( λ x _ → ZChain1.chainf (zc0 (& A)) x ? )
273 field 289 field
274 chain⊆A : chain ⊆' A 290 chain⊆A : chain ⊆' A
275 chain∋init : odef chain init 291 chain∋init : odef chain init
276 initial : {y : Ordinal } → odef chain y → * init ≤ * y 292 initial : {y : Ordinal } → odef chain y → * init ≤ * y
277 f-next : {a : Ordinal } → odef chain a → odef chain (f a) 293 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
291 307
292 -- data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) : Ordinal → Ordinal → Set n where 308 -- data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) : Ordinal → Ordinal → Set n where
293 -- 309 --
294 -- data Chain is total 310 -- data Chain is total
295 311
296 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) 312 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {x y : Ordinal} (ay : odef A y) (chainf : (z : Ordinal ) → z o< x → HOD)
297 {s s1 a b : Ordinal } ( ca : Chain A f mf ay s a ) ( cb : Chain A f mf ay s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a ) 313 {s s1 a b : Ordinal } ( ca : Chain A f mf ay chainf s a ) ( cb : Chain A f mf ay chainf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
298 chain-total A f mf {y} ay {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where 314 chain-total A f mf {x} {y} ay chainf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
299 ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay xa a → Chain A f mf ay xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a) 315 ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay chainf xa a → Chain A f mf ay chainf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
300 ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb 316 ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb
301 ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup y<xb ltyb axb supb fcb) = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where 317 ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup supb fcb) = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where
302 ct00 : * a < * xb 318 ct00 : * a < * xb
303 ct00 = supb _ _ (case1 refl) (ch-init a fca) 319 ct00 = ?
304 ct01 : * a < * b 320 ct01 : * a < * b
305 ct01 with s≤fc xb f mf fcb 321 ct01 with s≤fc xb f mf fcb
306 ... | case1 eq = subst (λ k → * a < k ) eq ct00 322 ... | case1 eq = subst (λ k → * a < k ) eq ct00
307 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt 323 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt
308 ct-ind xa xb {a} {b} (ch-is-sup y<x ltya ax supa fca) (ch-init b fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where 324 ct-ind xa xb {a} {b} (ch-is-sup supa fca) (ch-init b fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where
309 ct00 : * b < * xa 325 ct00 : * b < * xa
310 ct00 = supa _ _ (case1 refl) (ch-init b fcb) 326 ct00 = ?
311 ct01 : * b < * a 327 ct01 : * b < * a
312 ct01 with s≤fc xa f mf fca 328 ct01 with s≤fc xa f mf fca
313 ... | case1 eq = subst (λ k → * b < k ) eq ct00 329 ... | case1 eq = subst (λ k → * b < k ) eq ct00
314 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt 330 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt
315 ct-ind xa xb {a} {b} (ch-is-sup y<xa ltya axa supa fca) (ch-is-sup y<xb ltyb axb supb fcb) with trio< xa xb 331 ct-ind xa xb {a} {b} (ch-is-sup supa fca) (ch-is-sup supb fcb) with trio< xa xb
316 ... | tri< a₁ ¬b ¬c = tri< ct02 (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt) where 332 ... | tri< a₁ ¬b ¬c = tri< ct02 (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt) where
317 ct03 : * a < * xb 333 ct03 : * a < * xb
318 ct03 = supb _ _ (case2 ⟪ y<xa , a₁ ⟫) (ch-is-sup y<xa ltya axa supa fca) 334 ct03 = ?
319 ct02 : * a < * b 335 ct02 : * a < * b
320 ct02 with s≤fc xb f mf fcb 336 ct02 with s≤fc xb f mf fcb
321 ... | case1 eq = subst (λ k → * a < k ) eq ct03 337 ... | case1 eq = subst (λ k → * a < k ) eq ct03
322 ... | case2 lt = IsStrictPartialOrder.trans POO ct03 lt 338 ... | case2 lt = IsStrictPartialOrder.trans POO ct03 lt
323 ... | tri≈ ¬a refl ¬c = fcn-cmp xa f mf fca fcb 339 ... | tri≈ ¬a refl ¬c = fcn-cmp xa f mf fca fcb
324 ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04 where 340 ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04 where
325 ct05 : * b < * xa 341 ct05 : * b < * xa
326 ct05 = supa _ _ (case2 ⟪ y<xb , c ⟫) (ch-is-sup y<xb ltyb axb supb fcb) 342 ct05 = ?
327 ct04 : * b < * a 343 ct04 : * b < * a
328 ct04 with s≤fc xa f mf fca 344 ct04 with s≤fc xa f mf fca
329 ... | case1 eq = subst (λ k → * b < k ) eq ct05 345 ... | case1 eq = subst (λ k → * b < k ) eq ct05
330 ... | case2 lt = IsStrictPartialOrder.trans POO ct05 lt 346 ... | case2 lt = IsStrictPartialOrder.trans POO ct05 lt
331 347
464 px<x : px o< x 480 px<x : px o< x
465 px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc 481 px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
466 sc : ZChain1 A f mf ay px 482 sc : ZChain1 A f mf ay px
467 sc = prev px px<x 483 sc = prev px px<x
468 pchain : HOD 484 pchain : HOD
469 pchain = chainf sc px 485 pchain = chainf sc px ?
470 486
471 no-ext : ZChain1 A f mf ay x 487 no-ext : ZChain1 A f mf ay x
472 no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 } where 488 no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 } where
473 psup1 : Ordinal → Ordinal 489 psup1 : Ordinal → Ordinal
474 psup1 z with o≤? z x 490 psup1 z with o≤? z x
476 ... | no _ = ZChain1.psup sc x 492 ... | no _ = ZChain1.psup sc x
477 p≤z1 : (z : Ordinal ) → odef A (psup1 z) 493 p≤z1 : (z : Ordinal ) → odef A (psup1 z)
478 p≤z1 z with o≤? z x 494 p≤z1 z with o≤? z x
479 ... | yes _ = ZChain1.p≤z sc z 495 ... | yes _ = ZChain1.p≤z sc z
480 ... | no _ = ZChain1.p≤z sc x 496 ... | no _ = ZChain1.p≤z sc x
481 chainf1 : (z : Ordinal ) → HOD 497 chainf1 : (z : Ordinal ) → z o< x → HOD
482 chainf1 z with o≤? z x 498 chainf1 z z<x with o≤? z x
483 ... | yes _ = ZChain1.chainf sc z 499 ... | yes _ = ZChain1.chainf sc z ?
484 ... | no _ = ZChain1.chainf sc x 500 ... | no _ = ZChain1.chainf sc x ?
485 is-chain1 : {!!} 501 is-chain1 : {!!}
486 is-chain1 = {!!} 502 is-chain1 = {!!}
487 sc4 : ZChain1 A f mf ay x 503 sc4 : ZChain1 A f mf ay x
488 sc4 with ODC.∋-p O A (* x) 504 sc4 with ODC.∋-p O A (* x)
489 ... | no noax = no-ext 505 ... | no noax = no-ext
495 schain = {!!} -- record { od = record { def = λ z → odef A z ∧ ( odef (ZChain1.chain sc ) z ∨ (FClosure A f x z)) } 511 schain = {!!} -- record { od = record { def = λ z → odef A z ∧ ( odef (ZChain1.chain sc ) z ∨ (FClosure A f x z)) }
496 -- ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } 512 -- ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
497 ... | case2 ¬x=sup = no-ext 513 ... | case2 ¬x=sup = no-ext
498 ... | no ¬ox = sc4 where 514 ... | no ¬ox = sc4 where
499 pchainf : (z : Ordinal) → z o< x → HOD 515 pchainf : (z : Ordinal) → z o< x → HOD
500 pchainf z z<x = ZChain1.chainf (prev z z<x) z 516 pchainf z z<x = ZChain1.chainf (prev z z<x) z ?
501 pzc : (z : Ordinal) → z o< x → ZChain1 A f mf ay z 517 pzc : (z : Ordinal) → z o< x → ZChain1 A f mf ay z
502 pzc z z<x = prev z z<x 518 pzc z z<x = prev z z<x
503 UZ : HOD 519 UZ : HOD
504 UZ = UnionCF A x pchainf 520 UZ = UnionCF A x pchainf
505 total-UZ : IsTotalOrderSet UZ 521 total-UZ : IsTotalOrderSet UZ
506 total-UZ {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 522 total-UZ {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
507 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 523 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
508 uz01 = chain-total A f mf ay (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) _ _ (UChain.chain∋z (proj2 ca))) 524 uz01 = chain-total A f mf ay pchainf
509 (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) _ _ (UChain.chain∋z (proj2 cb))) 525 (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) _ _ ? (UChain.chain∋z (proj2 ca)))
526 (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) _ _ ? (UChain.chain∋z (proj2 cb)))
510 usup : SUP A UZ 527 usup : SUP A UZ
511 usup = supP UZ (λ lt → proj1 lt) total-UZ 528 usup = supP UZ (λ lt → proj1 lt) total-UZ
512 spu = & (SUP.sup usup) 529 spu = & (SUP.sup usup)
513 sc4 : ZChain1 A f mf ay x 530 sc4 : ZChain1 A f mf ay x
514 sc4 = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 } where 531 sc4 = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 } where
525 ... | yes _ = record { od = record { def = λ w → odef A w ∧ FClosure A f spu w } ; odmax = & A ; <odmax = {!!} } 542 ... | yes _ = record { od = record { def = λ w → odef A w ∧ FClosure A f spu w } ; odmax = & A ; <odmax = {!!} }
526 ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z 543 ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z
527 is-chain1 : (z w : Ordinal) → odef (chainf1 z) w → Chain A f mf ay (psup1 z ) w 544 is-chain1 : (z w : Ordinal) → odef (chainf1 z) w → Chain A f mf ay (psup1 z ) w
528 is-chain1 z w lt with o≤? x z 545 is-chain1 z w lt with o≤? x z
529 ... | no z<x = ZChain1.is-chain (pzc z (o¬≤→< z<x)) z w lt 546 ... | no z<x = ZChain1.is-chain (pzc z (o¬≤→< z<x)) z w lt
530 is-chain1 z w ⟪ ax , ux ⟫ | yes _ = ch-is-sup y<spu lty aspu {!!} ux where 547 is-chain1 z w ⟪ ax , ux ⟫ | yes _ = ch-is-sup {!!} ux where
531 y<spu : y << spu 548 y<spu : y << spu
532 y<spu = {!!} 549 y<spu = {!!}
533 lty : y o< spu 550 lty : y o< spu
534 lty = {!!} 551 lty = {!!}
535 aspu : odef A spu 552 aspu : odef A spu