Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 202:ed88384b5102
ε-induction like loop again
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 30 Jul 2019 17:52:15 +0900 |
| parents | a1a7caa8b305 |
| children | 8edd2a13a7f3 |
| files | OD.agda ordinal.agda |
| diffstat | 2 files changed, 10 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/OD.agda Tue Jul 30 01:12:24 2019 +0900 +++ b/OD.agda Tue Jul 30 17:52:15 2019 +0900 @@ -509,8 +509,6 @@ ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x))) <-osuc) where ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly } → (ly < lx) ∨ (oy d< ox ) → ψ (ord→od (record { lv = ly ; ord = oy } ) ) - ε-induction-ord Zero (Φ 0) (case1 ()) - ε-induction-ord Zero (Φ 0) (case2 ()) ε-induction-ord lx (OSuc lx ox) {ly} {oy} y<x = ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → od→ord z o< record { lv = lx ; ord = ox } @@ -563,23 +561,12 @@ a-choice : OD {suc n} is-in : X ∋ a-choice choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → choiced X - choice-func' X ∋-p not = lemma-ord (od→ord X) (subst (λ k → <-not {X} k ) (sym diso) lemma-init ) - where - <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n) - <-not {X} ox = ( y : Ordinal {suc n}) → ox o< osuc y → ¬ (X ∋ (ord→od y)) - ind : {x : OD} → ({y : OD} → x ∋ y → <-not {X} (od→ord y) → choiced X) → <-not {X} (od→ord x) → choiced X - ind {x} ψ nox = lemma (od→ord x) nox where - lemma : (ox : Ordinal {suc n}) → <-not {X} ox → choiced X - lemma ox nox with ∋-p X (ord→od ox) - ... | yes p = record { a-choice = ord→od ox ; is-in = p } - lemma record { lv = Zero ; ord = (Φ 0) } nox | no ¬p = {!!} - lemma record { lv = lx ; ord = (OSuc lx ox) } nox | no ¬p = lemma record { lv = lx ; ord = ox } {!!} - lemma record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } nox | no ¬p = lemma record { lv = lx ; ord = Φ lx } lemma2 where - lemma2 : ( y : Ordinal {suc n}) → record { lv = lx ; ord = Φ lx } o< osuc y → ¬ (X ∋ (ord→od y)) - lemma2 y lt = {!!} - lemma-ord : ( x : Ordinal {suc n} ) → (<-not {X} (od→ord (ord→od x))) → choiced X - lemma-ord x = ε-induction {n} {suc (suc n)} { λ x → (<-not {X} (od→ord x)) → choiced X} ind (ord→od x) - lemma-init : (y : Ordinal) → od→ord X o< osuc y → ¬ (X ∋ ord→od y) - lemma-init y lt lt2 with osuc-≡< lt - lemma-init y lt lt2 | case1 refl = o<¬≡ refl ( o<-subst (c<→o< {suc n} {_} {X} lt2) diso refl ) - lemma-init y lt lt2 | case2 lt1 = o<> lt1 ( o<-subst (c<→o< lt2) diso refl ) + choice-func' X ∋-p not = {!!} where + lemma-ord : ( lx : Nat ) (ox : OrdinalD lx ) → {ly : Nat} → {oy : OrdinalD ly } + → ordinal ly oy o< ordinal lx ox → choiced X ∨ ( ¬ ( def X (ordinal ly oy) )) + lemma-ord lx (OSuc lx ox) y<x with ∋-p X (ord→od (ordinal lx (OSuc lx ox))) + lemma-ord lx (OSuc lx ox) y<x | yes p = case1 ( record { a-choice = (ord→od (ordinal lx (OSuc lx ox))) ; is-in = p } ) + lemma-ord lx (OSuc lx ox) y<x | no ¬p with osuc-≡< y<x + lemma-ord lx (OSuc lx ox) y<x | no ¬p | case1 refl = {!!} + lemma-ord lx (OSuc lx ox) y<x | no ¬p | case2 t = lemma-ord lx ox t + lemma-ord (Suc lx) (Φ (Suc lx)) (case1 x) = {!!}