Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 200:57be355d1336
ε-induction again
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 29 Jul 2019 23:50:00 +0900 |
parents | 68eecbb011ef |
children | a1a7caa8b305 |
comparison
equal
deleted
inserted
replaced
199:68eecbb011ef | 200:57be355d1336 |
---|---|
561 record choiced {n : Level} ( X : OD {suc n}) : Set (suc (suc n)) where | 561 record choiced {n : Level} ( X : OD {suc n}) : Set (suc (suc n)) where |
562 field | 562 field |
563 a-choice : OD {suc n} | 563 a-choice : OD {suc n} |
564 is-in : X ∋ a-choice | 564 is-in : X ∋ a-choice |
565 choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → choiced X | 565 choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → choiced X |
566 choice-func' X ∋-p not = lemma-ord (od→ord X) lemma-init | 566 choice-func' X ∋-p not = lemma-ord (od→ord X) (subst (λ k → <-not {X} k ) (sym diso) lemma-init ) |
567 where | 567 where |
568 <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n) | 568 <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n) |
569 <-not {X} ox = ( y : Ordinal {suc n}) → ox o< osuc y → ¬ (X ∋ (ord→od y)) | 569 <-not {X} ox = ( y : Ordinal {suc n}) → ox o< osuc y → ¬ (X ∋ (ord→od y)) |
570 ind : {x : OD} → ({y : OD} → x ∋ y → <-not {X} (od→ord y) → choiced X) → <-not {X} (od→ord x) → choiced X | |
571 ind {y} ψ nox with ∋-p X y | |
572 ind {y} ψ nox | yes p = record { a-choice = y ; is-in = p } | |
573 ind {y} ψ nox | no ¬p = {!!} | |
574 lemma-ord : ( x : Ordinal {suc n} ) → (<-not {X} (od→ord (ord→od x))) → choiced X | |
575 lemma-ord x = ε-induction {n} {suc (suc n)} { λ x → (<-not {X} (od→ord x)) → choiced X} ind (ord→od x) | |
570 lemma-init : (y : Ordinal) → od→ord X o< osuc y → ¬ (X ∋ ord→od y) | 576 lemma-init : (y : Ordinal) → od→ord X o< osuc y → ¬ (X ∋ ord→od y) |
571 lemma-init y lt lt2 with osuc-≡< lt | 577 lemma-init y lt lt2 with osuc-≡< lt |
572 lemma-init y lt lt2 | case1 refl = o<¬≡ refl ( o<-subst (c<→o< {suc n} {_} {X} lt2) diso refl ) | 578 lemma-init y lt lt2 | case1 refl = o<¬≡ refl ( o<-subst (c<→o< {suc n} {_} {X} lt2) diso refl ) |
573 lemma-init y lt lt2 | case2 lt1 = o<> lt1 ( o<-subst (c<→o< lt2) diso refl ) | 579 lemma-init y lt lt2 | case2 lt1 = o<> lt1 ( o<-subst (c<→o< lt2) diso refl ) |
574 lemma-ord : ( ox : Ordinal {suc n} ) → <-not {X} ox → choiced X | |
575 lemma-ord ox not = lemma1 (lv ox) (ord ox) not where | |
576 lemma1 : (lx : Nat) ( ox : OrdinalD lx ) → <-not {X} record {lv = lx ; ord = ox} → choiced X | |
577 lemma1 lx ox not with ∋-p X (ord→od record { lv = lx ; ord = ox}) | |
578 ... | yes p = record { a-choice = ord→od record { lv = lx ; ord = ox} ; is-in = p } | |
579 lemma1 Zero (Φ 0) not | no ¬p = {!!} | |
580 lemma1 lx (OSuc lx ox) not | no ¬p = lemma1 lx ox {!!} | |
581 lemma1 (Suc lx) (Φ (Suc lx)) not | no ¬p = lemma1 lx (Φ lx) lemmaΦ where | |
582 -- not : ( y : Ordinal {suc n}) → (record { lv = Suc lx ; ord = Φ (Suc lx) }) o< osuc y → ¬ (X ∋ (ord→od y)) | |
583 -- we also have lemma1 lx any | |
584 lemmaΦ : ( y : Ordinal {suc n}) → (record { lv = lx ; ord = Φ lx }) o< osuc y → ¬ (X ∋ (ord→od y)) | |
585 lemmaΦ y lt with trio< (record { lv = Suc lx ; ord = Φ (Suc lx) }) (osuc y ) | |
586 lemmaΦ y lt | tri< a ¬b ¬c = not y a | |
587 -- record { lv = lx ; ord = Φ lx } o< osuc y o< record { lv = Suc lx ; ord = Φ (Suc lx) } | |
588 lemmaΦ y lt | tri> ¬a ¬b c = {!!} | |
589 |