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

comparison OD.agda @ 210:2c7d45734e3b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
axiom of choice from exclusive middle done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 01 Aug 2019 12:23:07 +0900
parents e59e682ad120
children 22d435172d1a
comparison
equal deleted inserted replaced
209:e59e682ad120 210:2c7d45734e3b
557 lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt ) 557 lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt )
558 lemma6 : { ly : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } → 558 lemma6 : { ly : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } →
559 lx ≡ ly → ly ≡ lv (od→ord z) → ψ z 559 lx ≡ ly → ly ≡ lv (od→ord z) → ψ z
560 lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl) 560 lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl)
561 561
562 ---
563 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
564 ---
562 record choiced {n : Level} ( X : OD {suc n}) : Set (suc (suc n)) where 565 record choiced {n : Level} ( X : OD {suc n}) : Set (suc (suc n)) where
563 field 566 field
564 a-choice : OD {suc n} 567 a-choice : OD {suc n}
565 is-in : X ∋ a-choice 568 is-in : X ∋ a-choice
566 choice-func' : (X : OD {suc n} ) → (p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X 569 choice-func' : (X : OD {suc n} ) → (p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
587 caseΦ lx prev with ∋-p' X ( ord→od (ordinal lx (Φ lx) )) 590 caseΦ lx prev with ∋-p' X ( ord→od (ordinal lx (Φ lx) ))
588 caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } ) 591 caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
589 caseΦ lx prev | no ¬p = lemma where 592 caseΦ lx prev | no ¬p = lemma where
590 lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X) 593 lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X)
591 lemma1 x with trio< x (ordinal lx (Φ lx)) 594 lemma1 x with trio< x (ordinal lx (Φ lx))
592 lemma1 x | tri< a ¬b ¬c with prev x a 595 lemma1 x | tri< a ¬b ¬c with prev (osuc x) (lemma2 a) where
593 lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 {!!} 596 lemma2 : x o< (ordinal lx (Φ lx)) → osuc x o< ordinal lx (Φ lx)
597 lemma2 (case1 lt) = case1 lt
594 lemma1 x | tri< a ¬b ¬c | case2 found = case2 found 598 lemma1 x | tri< a ¬b ¬c | case2 found = case2 found
599 lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 ( λ lt df → not_found x <-osuc df )
595 lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt )) 600 lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt ))
596 lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c )) 601 lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c ))
597 lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X 602 lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X
598 lemma = ∀-imply-or lemma1 603 lemma = ∀-imply-or lemma1
599 caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) ) 604 caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) )
608 lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl ) 613 lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl )
609 lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 ) 614 lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 )
610 caseOSuc lx x (case2 found) | no ¬p = case2 found 615 caseOSuc lx x (case2 found) | no ¬p = case2 found
611 have_to_find : choiced X 616 have_to_find : choiced X
612 have_to_find with lemma-ord (od→ord X ) 617 have_to_find with lemma-ord (od→ord X )
613 have_to_find | t = dont-or t {!!} 618 have_to_find | t = dont-or t ¬¬X∋x where
614 619 ¬¬X∋x : ¬ ((x : Ordinal) → (Suc (lv x) ≤ lv (od→ord X)) ∨ (ord x d< ord (od→ord X)) → def X x → ⊥)
620 ¬¬X∋x nn = not record {
621 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
622 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
623 }
624