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

comparison src/zorn.agda @ 534:c9f80aea598e

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 Sat, 23 Apr 2022 18:05:12 +0900
parents 7325484fc491
children b83dde5dbd33
comparison
equal deleted inserted replaced
533:7325484fc491 534:c9f80aea598e
442 field 442 field
443 az : odef A z 443 az : odef A z
444 x<z : * x < * z 444 x<z : * x < * z
445 z<y : * z < * y 445 z<y : * z < * y
446 446
447 IndirectSet< : (A : HOD) → {x y : Ordinal } (xa : odef A x) (ya : odef A y) → HOD 447 record Prev< (A : HOD) {x : Ordinal } (xa : odef A x) ( f : Ordinal → Ordinal ) : Set n where
448 IndirectSet< A {x} {y} xa ya = record { od = record { def = λ z → odef A z ∧ Indirect< A xa ya z } ; odmax = & A ; <odmax = {!!} } 448 field
449 449 y : Ordinal
450 record Prev< (A : HOD) {x : Ordinal } (xa : odef A x) : Set n where 450 ay : odef A y
451 field 451 x=fy : x ≡ f y
452 prev : Ordinal
453 aprev : odef A prev
454 direct : & (IndirectSet< A aprev xa ) ≡ o∅
455 452
456 record SUP ( A B : HOD ) : Set (Level.suc n) where 453 record SUP ( A B : HOD ) : Set (Level.suc n) where
457 field 454 field
458 sup : HOD 455 sup : HOD
459 A∋maximal : A ∋ sup 456 A∋maximal : A ∋ sup
467 field 464 field
468 chain : HOD 465 chain : HOD
469 chain⊆A : chain ⊆ A 466 chain⊆A : chain ⊆ A
470 f-total : IsTotalOrderSet chain 467 f-total : IsTotalOrderSet chain
471 f-next : {a : Ordinal } → odef chain a → odef chain (f a) 468 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
472 is-max : {a b : Ordinal } → odef chain a → odef A b → a o< z → ( ? ∨ (sup (& chain) (subst ? ? f-total) ≡ b )) → * a < * b → odef chain b 469 is-max : {a b : Ordinal } → (ca : odef chain a ) → odef A b → a o< z
470 → ( Prev< A (incl chain⊆A (subst (λ k → odef chain k ) (sym &iso) ca)) f ∨ (sup (& chain) (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b ))
471 → * a < * b → odef chain b
473 472
474 Zorn-lemma : { A : HOD } 473 Zorn-lemma : { A : HOD }
475 → o∅ o< & A 474 → o∅ o< & A
476 → IsPartialOrderSet A 475 → IsPartialOrderSet A
477 → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B ) -- SUP condition 476 → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B ) -- SUP condition
505 ... | no not = & (ODC.minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))) 504 ... | no not = & (ODC.minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq)))
506 cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) → odef A x → ( * x < * (cf nmx x) ) ∧ odef A (cf nmx x ) 505 cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) → odef A x → ( * x < * (cf nmx x) ) ∧ odef A (cf nmx x )
507 cf-is-<-monotonic nmx x ax = ⟪ {!!} , {!!} ⟫ 506 cf-is-<-monotonic nmx x ax = ⟪ {!!} , {!!} ⟫
508 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx ) 507 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx )
509 cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ 508 cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫
510 zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc : ZChain A sa f mf ? (& A)) → SUP A (ZChain.chain zc) 509 zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc : ZChain A sa f mf {!!} (& A)) → SUP A (ZChain.chain zc)
511 zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc ) 510 zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc )
512 -- zsup zc f mf = & ( SUP.sup (supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf ) ) ) 511 -- zsup zc f mf = & ( SUP.sup (supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf ) ) )
513 A∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) ? (& A)) 512 A∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) {!!} (& A))
514 → A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )) 513 → A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) ))
515 A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) ) 514 A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )
516 z03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf ? (& A)) → f (& ( SUP.sup (zsup f mf zc ))) ≡ & (SUP.sup (zsup f mf zc )) 515 z03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf {!!} (& A)) → f (& ( SUP.sup (zsup f mf zc ))) ≡ & (SUP.sup (zsup f mf zc ))
517 z03 = {!!} 516 z03 = {!!}
518 z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) ? (& A)) → ⊥ 517 z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) {!!} (& A)) → ⊥
519 z04 nmx zc = z01 {* (cf nmx c)} {* c} {!!} (A∋zsup nmx zc ) (case1 ( cong (*)( z03 (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) 518 z04 nmx zc = z01 {* (cf nmx c)} {* c} {!!} (A∋zsup nmx zc ) (case1 ( cong (*)( z03 (cf nmx) (cf-is-≤-monotonic nmx ) zc )))
520 (proj1 (cf-is-<-monotonic nmx c ((subst λ k → odef A k ) &iso (A∋zsup nmx zc )))) where 519 (proj1 (cf-is-<-monotonic nmx c ((subst λ k → odef A k ) &iso (A∋zsup nmx zc )))) where
521 c = & (SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc )) 520 c = & (SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ))
522 -- ZChain is not compatible with the SUP condition 521 -- ZChain is not compatible with the SUP condition
523 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A sa f mf ? y ) 522 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A sa f mf {!!} y )
524 → ZChain A sa f mf ? x 523 → ZChain A sa f mf {!!} x
525 ind f mf x prev with Oprev-p x 524 ind f mf x prev with Oprev-p x
526 ... | yes op with ODC.∋-p O A (* x) 525 ... | yes op with ODC.∋-p O A (* x)
527 ... | no ¬Ax = zc1 where 526 ... | no ¬Ax = zc1 where
528 -- we have previous ordinal and ¬ A ∋ x, use previous Zchain 527 -- we have previous ordinal and ¬ A ∋ x, use previous Zchain
529 px = Oprev.oprev op 528 px = Oprev.oprev op
530 zc0 : ZChain A sa f mf ? (Oprev.oprev op) 529 zc0 : ZChain A sa f mf {!!} (Oprev.oprev op)
531 zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 530 zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc)
532 zc1 : ZChain A sa f mf ? x 531 zc1 : ZChain A sa f mf {!!} x
533 zc1 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; is-max = {!!} } 532 zc1 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; is-max = {!!} }
534 ... | yes ax = zc4 where -- we have previous ordinal and A ∋ x 533 ... | yes ax = zc4 where -- we have previous ordinal and A ∋ x
535 px = Oprev.oprev op 534 px = Oprev.oprev op
536 zc0 : ZChain A sa f mf ? (Oprev.oprev op) 535 zc0 : ZChain A sa f mf {!!} (Oprev.oprev op)
537 zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 536 zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc)
538 -- x is in the previous chain, use the same 537 -- x is in the previous chain, use the same
539 -- x has some y which y < x ∧ f y ≡ x 538 -- x has some y which y < x ∧ f y ≡ x
540 -- x has no y which y < x 539 -- x has no y which y < x
541 zc4 : ZChain A sa f mf ? x 540 zc4 : ZChain A sa f mf {!!} x
542 zc4 = record { chain = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; is-max = {!!} } 541 zc4 = record { chain = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; is-max = {!!} }
543 ind f mf x prev | no ¬ox with trio< (& A) x --- limit ordinal case 542 ind f mf x prev | no ¬ox with trio< (& A) x --- limit ordinal case
544 ... | tri< a ¬b ¬c = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 543 ... | tri< a ¬b ¬c = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
545 ; is-max = {!!} } where 544 ; is-max = {!!} } where
546 zc0 = prev (& A) a 545 zc0 = prev (& A) a
560 -- if we have no maximal, make ZChain, which contradict SUP condition 559 -- if we have no maximal, make ZChain, which contradict SUP condition
561 nmx : ¬ Maximal A 560 nmx : ¬ Maximal A
562 nmx mx = ∅< {HasMaximal} zc5 ( ≡o∅→=od∅ ¬Maximal ) where 561 nmx mx = ∅< {HasMaximal} zc5 ( ≡o∅→=od∅ ¬Maximal ) where
563 zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) → odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) 562 zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) → odef A y → ¬ (* (& (Maximal.maximal mx)) < * y))
564 zc5 = ⟪ Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫ 563 zc5 = ⟪ Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫
565 zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → ZChain A sa f mf ? (& A) 564 zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → ZChain A sa f mf {!!} (& A)
566 zorn03 f mf = TransFinite (ind f mf) (& A) 565 zorn03 f mf = TransFinite (ind f mf) (& A)
567 566
568 -- usage (see filter.agda ) 567 -- usage (see filter.agda )
569 -- 568 --
570 -- _⊆'_ : ( A B : HOD ) → Set n 569 -- _⊆'_ : ( A B : HOD ) → Set n