Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 176:ecb329ba38ac
ε-induction done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 20 Jul 2019 08:03:46 +0900 |
| parents | 51189f7b9229 |
| children | e75fad60cf8c f5b3f30fcb16 |
| files | HOD.agda |
| diffstat | 1 files changed, 56 insertions(+), 56 deletions(-) [+] |
line wrap: on
line diff
--- a/HOD.agda Fri Jul 19 17:16:43 2019 +0900 +++ b/HOD.agda Sat Jul 20 08:03:46 2019 +0900 @@ -236,62 +236,6 @@ -- L0 : {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x --- another form of regularity --- --- {-# TERMINATING #-} -ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} - → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) - → (x : OD {suc n} ) → ψ x -ε-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 : (y : OD) → ord→od record { lv = ly ; ord = oy } ∋ y → od→ord y o< record { lv = lx ; ord = ox } - lemma y lt with osuc-≡< y<x - lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso - lemma y lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 - ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) = - ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt ) where - lemma0 : { lx ly : Nat } → ly < Suc lx → lx < ly → ⊥ - lemma0 {Suc lx} {Suc ly} (s≤s lt1) (s≤s lt2) = lemma0 lt1 lt2 - lemma1 : {n : Level } {ly : Nat} {oy : OrdinalD {suc n} ly} → lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) ≡ ly - lemma1 {n} {ly} {oy} = let open ≡-Reasoning in begin - lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) - ≡⟨ cong ( λ k → lv k ) diso ⟩ - lv (record { lv = ly ; ord = oy }) - ≡⟨⟩ - ly - ∎ - lemma2 : { lx : Nat } → lx < Suc lx - lemma2 {Zero} = s≤s z≤n - lemma2 {Suc lx} = s≤s (lemma2 {lx}) - -- lx Suc lx (1) z(a) <lx by case1 - -- ly(1) ly(2) (2) z(b) <lx by case1 - -- z(a) z(b) z(c) z(c) <lx by case2 ( ly==z==x) - -- - lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z - lemma z lt with c<→o< {suc n} {z} {ord→od (record { lv = ly ; ord = oy })} lt - lemma z lt | case1 lz<ly with <-cmp lx ly - lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen - lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- (1) - subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) )) - lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- z(a) - subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c)))) - lemma z lt | case2 lz=ly with <-cmp lx ly - lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen - lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- z(b) - ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) - lemma z lt | case2 lz=ly | tri≈ ¬a refl ¬c with d<→lv lz=ly -- z(c) - ... | eq = lemma6 {lx} {ly} {lv (od→ord z)} {Φ lx} {oy} {ord (od→ord z)} {!!} ? ? where - lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z - lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt ) - lemma6 : { lx ly lz : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } { oz : OrdinalD {suc n} lz } → - lx ≡ ly → ly ≡ lz → oz d< oy → ψ z - lemma6 {lx} {ly} {lz} {ox} {oy} {oz} refl refl _ = lemma5 {!!} (case2 {!!} ) - OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} OD→ZF {n} = record { @@ -523,3 +467,59 @@ choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A choice X {A} X∋A not = x∋minimul A not + -- another form of regularity + -- + -- {-# TERMINATING #-} + ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} + → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) + → (x : OD {suc n} ) → ψ x + ε-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 : (y : OD) → ord→od record { lv = ly ; ord = oy } ∋ y → od→ord y o< record { lv = lx ; ord = ox } + lemma y lt with osuc-≡< y<x + lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso + lemma y lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 + ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) = + ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt ) where + lemma0 : { lx ly : Nat } → ly < Suc lx → lx < ly → ⊥ + lemma0 {Suc lx} {Suc ly} (s≤s lt1) (s≤s lt2) = lemma0 lt1 lt2 + lemma1 : {n : Level } {ly : Nat} {oy : OrdinalD {suc n} ly} → lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) ≡ ly + lemma1 {n} {ly} {oy} = let open ≡-Reasoning in begin + lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) + ≡⟨ cong ( λ k → lv k ) diso ⟩ + lv (record { lv = ly ; ord = oy }) + ≡⟨⟩ + ly + ∎ + lemma2 : { lx : Nat } → lx < Suc lx + lemma2 {Zero} = s≤s z≤n + lemma2 {Suc lx} = s≤s (lemma2 {lx}) + -- lx Suc lx (1) z(a) <lx by case1 + -- ly(1) ly(2) (2) z(b) <lx by case1 + -- z(a) z(b) z(c) z(c) <lx by case2 ( ly==z==x) + -- + lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z + lemma z lt with c<→o< {suc n} {z} {ord→od (record { lv = ly ; ord = oy })} lt + lemma z lt | case1 lz<ly with <-cmp lx ly + lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen + lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- (1) + subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) )) + lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- z(a) + subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c)))) + lemma z lt | case2 lz=ly with <-cmp lx ly + lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen + lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- z(b) + ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) + lemma z lt | case2 lz=ly | tri≈ ¬a refl ¬c with d<→lv lz=ly -- z(c) + ... | eq = lemma6 {ly} {Φ lx} {oy} refl (sym (subst (λ k → lv (od→ord z) ≡ k) lemma1 eq)) where + lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z + lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt ) + lemma6 : { ly : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } → + lx ≡ ly → ly ≡ lv (od→ord z) → ψ z + lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl) +