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

comparison OD.agda @ 194:2a5844398f1c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
emulate ε-induction proof
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Jul 2019 11:27:33 +0900
parents 0b9645a65542
children 0cefb1e4d2cc
comparison
equal deleted inserted replaced
193:0b9645a65542 194:2a5844398f1c
557 lemma6 : { ly : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } → 557 lemma6 : { ly : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } →
558 lx ≡ ly → ly ≡ lv (od→ord z) → ψ z 558 lx ≡ ly → ly ≡ lv (od→ord z) → ψ z
559 lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl) 559 lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl)
560 560
561 choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → OD {suc n} 561 choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → OD {suc n}
562 choice-func' X ∋-p not = c 562 choice-func' X ∋-p not = lemma-ord (lv (osuc (od→ord X))) (ord (osuc (od→ord X))) <-osuc
563 where 563 where
564 ψ : (y : OD {suc n} ) → Set (suc (suc n)) 564 lemma-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly }
565 ψ y = OD {suc n} 565 → (ly < lx) ∨ (oy d< ox ) → OD {suc n}
566 lemma : ( x : OD {suc n} ) → ({ y : OD {suc n} } → x ∋ y → ψ y) → ψ x 566 lemma-ord Zero (Φ 0) (case1 ())
567 lemma x prev = lemma1 (od→ord X) <-osuc where 567 lemma-ord Zero (Φ 0) (case2 ())
568 lemma1 : (ox : Ordinal {suc n}) → ox o< osuc (od→ord X) → OD {suc n} 568 lemma-ord Zero (OSuc 0 ox) lt with ∋-p X (ord→od record { lv = Zero ; ord = OSuc 0 ox })
569 lemma1 ox lt with ∋-p X (ord→od ox) 569 lemma-ord Zero (OSuc Zero ox) lt | yes p = ord→od record { lv = Zero ; ord = OSuc 0 ox }
570 lemma1 ox lt | yes p = ord→od ox 570 lemma-ord Zero (OSuc Zero ox) {ly} {oy} lt | no ¬p = lemma-ord Zero ox {!!}
571 lemma1 record { lv = Zero ; ord = (Φ .0) } lt | no ¬p = {!!} 571 lemma-ord (Suc lx) (OSuc (Suc lx) ox) lt with ∋-p X (ord→od record { lv = (Suc lx) ; ord = ox } )
572 lemma1 record { lv = Zero ; ord = (OSuc .0 ord₁) } lt | no ¬p = lemma1 record { lv = Zero ; ord = ord₁ } {!!} 572 lemma-ord (Suc lx) (OSuc (Suc lx) ox) lt | yes p = ord→od record { lv = (Suc lx) ; ord = ox }
573 lemma1 record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } lt | no ¬p = {!!} 573 lemma-ord (Suc lx) (OSuc (Suc lx) ox) {ly} {oy} lt | no ¬p = lemma-ord (Suc lx) ox {!!}
574 lemma1 record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } lt | no ¬p = lemma1 record { lv = Suc lv₁ ; ord = ord₁ } {!!} 574 lemma-ord (Suc lx) (Φ (Suc lx)) lt with ∋-p X (ord→od record { lv = Suc lx ; ord = Φ (Suc lx)})
575 c : OD {suc n} 575 lemma-ord (Suc lx) (Φ (Suc lx)) lt | yes p = ord→od record { lv = Suc lx ; ord = Φ (Suc lx)}
576 c = ε-induction (λ {x} → lemma x) X 576 lemma-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} lt | no ¬p = {!!}