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

comparison OD.agda @ 199:68eecbb011ef

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
curry form
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Jul 2019 20:02:08 +0900
parents 8589660ee388
children 57be355d1336
comparison
equal deleted inserted replaced
198:8589660ee388 199:68eecbb011ef
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 = proj2 ( lemma-ord (od→ord X) ) 566 choice-func' X ∋-p not = lemma-ord (od→ord X) 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 lemma-init : (y : Ordinal) → od→ord X o< osuc y → ¬ (X ∋ ord→od y) 570 lemma-init : (y : Ordinal) → od→ord X o< osuc y → ¬ (X ∋ ord→od y)
571 lemma-init y lt lt2 with osuc-≡< lt 571 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 ) 572 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 ) 573 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 574 lemma-ord : ( ox : Ordinal {suc n} ) → <-not {X} ox → choiced X
575 lemma-ord ox = lemma1 (lv ox) (ord ox) where 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 576 lemma1 : (lx : Nat) ( ox : OrdinalD lx ) → <-not {X} record {lv = lx ; ord = ox} → choiced X
577 lemma1 lx ox with ∋-p X (ord→od record { lv = lx ; ord = ox}) 577 lemma1 lx ox not with ∋-p X (ord→od record { lv = lx ; ord = ox})
578 ... | yes p = record { proj2 = record { a-choice = ord→od record { lv = lx ; ord = ox} ; is-in = p }; proj1 = {!!} } 578 ... | yes p = record { a-choice = ord→od record { lv = lx ; ord = ox} ; is-in = p }
579 lemma1 Zero (Φ 0) | no ¬p = {!!} 579 lemma1 Zero (Φ 0) not | no ¬p = {!!}
580 lemma1 lx (OSuc lx ox) | no ¬p = record { proj2 = proj2 (lemma1 lx ox) ; proj1 = {!!} } 580 lemma1 lx (OSuc lx ox) not | no ¬p = lemma1 lx ox {!!}
581 lemma1 (Suc lx) (Φ (Suc lx)) | no ¬p = record { proj2 = proj2 ( lemma1 lx (Φ lx) ) ; proj1 = {!!} } where 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)) 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 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)) 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 ) 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 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) } 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 = {!!} 588 lemmaΦ y lt | tri> ¬a ¬b c = {!!}
589 589