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

comparison src/zorn.agda @ 735:5dacaf73eba8

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 Tue, 19 Jul 2022 13:44:33 +0900
parents 753780183ddf
children 3c3e3a1291bb
comparison
equal deleted inserted replaced
734:753780183ddf 735:5dacaf73eba8
304 field 304 field
305 supf : Ordinal → Ordinal 305 supf : Ordinal → Ordinal
306 chain : HOD 306 chain : HOD
307 chain = UnionCF A f mf ay supf z 307 chain = UnionCF A f mf ay supf z
308 field 308 field
309 -- chain-mono : {z1 : Ordinal} → z1 o≤ z → UnionCF A f mf ay supf z1 ⊆' UnionCF A f mf ay supf z
310 chain<A : {z : Ordinal } → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf (& A) 309 chain<A : {z : Ordinal } → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf (& A)
311 chain⊆A : chain ⊆' A 310 chain⊆A : chain ⊆' A
312 chain∋init : odef chain init 311 chain∋init : odef chain init
313 initial : {y : Ordinal } → odef chain y → * init ≤ * y 312 initial : {y : Ordinal } → odef chain y → * init ≤ * y
314 f-next : {a : Ordinal } → odef chain a → odef chain (f a) 313 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
315 f-total : IsTotalOrderSet chain 314 f-total : IsTotalOrderSet chain
315 sup=u : {b : Ordinal} → (ab : odef A b) → IsSup A chain ab → supf b ≡ b
316 316
317 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 317 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
318 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where 318 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
319 field 319 field
320 chain-mono2 : { a b c : Ordinal } → 320 chain-mono2 : { a b c : Ordinal } →
436 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → ZChain1 A f mf ay zc x 436 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → ZChain1 A f mf ay zc x
437 SZ1 A f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x where 437 SZ1 A f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x where
438 chain-mono2 : (x : Ordinal) {a b c : Ordinal} → a o≤ b → b o≤ x → 438 chain-mono2 : (x : Ordinal) {a b c : Ordinal} → a o≤ b → b o≤ x →
439 odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c 439 odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
440 chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , record { u = _ ; u<x = u<x ; uchain = ch-init .c fc } ⟫ = 440 chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , record { u = _ ; u<x = u<x ; uchain = ch-init .c fc } ⟫ =
441 ⟪ ua , record { u = _ ; u<x = case2 refl ; uchain = ch-init c fc } ⟫ 441 ⟪ ua , record { u = _ ; u<x = case2 refl ; uchain = ch-init c fc } ⟫
442 chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = 442 chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ =
443 ⟪ ua , record { u = u ; u<x = case1 (ordtrans<-≤ u<x a≤b) ; uchain = ch-is-sup is-sup fc } ⟫ 443 ⟪ ua , record { u = u ; u<x = case1 (ordtrans<-≤ u<x a≤b) ; uchain = ch-is-sup is-sup fc } ⟫
444 is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
445 b o< x → (ab : odef A b) →
446 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f →
447 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
448 is-max-hp x {a} {b} ua b<x ab has-prev a<b = m04 where
449 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
450 m04 = ⟪ m07 , record { u = UChain.u (proj2 m06) ; u<x = UChain.u<x (proj2 m06)
451 ; uchain = subst (λ k → Chain A f mf ay (ZChain.supf zc) (UChain.u (proj2 m06)) k) (sym (HasPrev.x=fy has-prev)) m08 } ⟫ where
452 m06 : odef (UnionCF A f mf ay (ZChain.supf zc) x) (HasPrev.y has-prev )
453 m06 = HasPrev.ay has-prev
454 m07 : odef A b
455 m07 = subst (λ k → odef A k ) (sym (HasPrev.x=fy has-prev)) (proj2 (mf _ (proj1 m06) ))
456 m08 : Chain A f mf ay (ZChain.supf zc) (UChain.u (proj2 m06)) (f ( HasPrev.y has-prev ))
457 m08 with proj2 m06
458 ... | record { u = _ ; u<x = u<x ; uchain = ch-init .(HasPrev.y has-prev) fc } =
459 ch-init (f (HasPrev.y has-prev)) (fsuc _ fc)
460 ... | record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } = ch-is-sup ? (fsuc _ fc)
444 zc1 : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x 461 zc1 : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
445 zc1 x prev with Oprev-p x 462 zc1 x prev with Oprev-p x
446 ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x } where 463 ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x } where
447 px = Oprev.oprev op 464 px = Oprev.oprev op
465 zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
466 zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt
448 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → 467 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
449 b o< x → (ab : odef A b) → 468 b o< x → (ab : odef A b) →
450 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 → 469 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 →
451 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b 470 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
452 is-max {a} {b} ua b<x ab (case1 has-prev) a<b = m04 where 471 is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b
453 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
454 m04 = ?
455 is-max {a} {b} ua b<x ab (case2 is-sup) a<b with ODC.p∨¬p O ( HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ) 472 is-max {a} {b} ua b<x ab (case2 is-sup) a<b with ODC.p∨¬p O ( HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f )
456 ... | case1 has-prev = m04 where 473 ... | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b
457 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
458 m04 = ⟪ m07 , record { u = UChain.u (proj2 m06) ; u<x = UChain.u<x (proj2 m06) ; uchain = ? } ⟫ where
459 m06 : odef (UnionCF A f mf ay (ZChain.supf zc) x) (HasPrev.y has-prev )
460 m06 = HasPrev.ay has-prev
461 m07 : odef A b
462 m07 = subst (λ k → odef A k ) (sym (HasPrev.x=fy has-prev)) (proj2 (mf _ (proj1 m06) ))
463 m08 : Chain A f mf ay (ZChain.supf zc) (UChain.u (proj2 m06)) (f ( HasPrev.y has-prev ))
464 m08 with proj2 m06
465 ... | record { u = _ ; u<x = u<x ; uchain = ch-init .(HasPrev.y has-prev) fc } =
466 ch-init (f (HasPrev.y has-prev)) (fsuc _ fc)
467 ... | record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } = ch-is-sup ? (fsuc _ fc)
468 ... | case2 ¬fy<x = m01 where 474 ... | case2 ¬fy<x = m01 where
475 px<x : px o< x
476 px<x = subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc
469 m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b 477 m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
470 m01 with trio< px b 478 m01 with trio< b px
471 ... | tri< a ¬b ¬c = ZChain1.chain-mono2 (prev px {!!}) {!!} {!!} m04 where 479 ... | tri> ¬a ¬b c = ⊥-eim ()
480 ... | tri< b<px ¬b ¬c = chain-mono2 x ( o<→≤ (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )) o≤-refl m04 where
481 m03 : odef (UnionCF A f mf ay (ZChain.supf zc) px) a
482 m03 = ?
472 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b 483 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
473 m04 = ZChain1.is-max (prev px {!!}) {!!} {!!} ab {!!} a<b 484 m04 = ZChain1.is-max (prev px px<x) m03 b<px ab
474 ... | tri≈ ¬a b ¬c = {!!} 485 (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
475 ... | tri> ¬a ¬b c = {!!} 486 ... | tri≈ ¬a b=px ¬c = {!!}
476 ... | no lim = record { is-max = {!!} ; chain-mono2 = chain-mono2 x } where 487 ... | no lim = record { is-max = is-max ; chain-mono2 = chain-mono2 x } where
477 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → 488 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
478 b o< x → (ab : odef A b) → 489 b o< x → (ab : odef A b) →
479 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 → 490 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 →
480 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b 491 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
481 is-max {a} {b} ua b<x ab (case1 has-prev) a<b = ? 492 is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b
482 is-max {a} {b} ua b<x ab (case2 is-sup) a<b = ? 493 is-max {a} {b} ua b<x ab (case2 is-sup) a<b = chain-mono2 x ? o≤-refl m04 where
483 --- with ODC.p∨¬p O ( HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ) 494 m05 : b ≡ ZChain.supf zc b
484 --- m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b 495 m05 = sym (ZChain.sup=u ? ab is-sup)
485 --- m04 = ZChain1.is-max (prev (osuc b) {!!} ) {!!} <-osuc ab {!!} a<b 496 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
497 m04 = ⟪ ab , record { u = b ; u<x = case1 <-osuc ; uchain = ch-is-sup ? (subst (λ k → FClosure A f k b) m05 (init ab)) } ⟫
486 498
487 --- 499 ---
488 --- the maximum chain has fix point of any ≤-monotonic function 500 --- the maximum chain has fix point of any ≤-monotonic function
489 --- 501 ---
490 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) 502 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) )