Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ordinal.agda @ 261:d9d178d1457c
ε-induction from TransFinite induction
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 17 Sep 2019 09:29:27 +0900 |
| parents | c10048d69614 |
| children | 53744836020b |
comparison
equal
deleted
inserted
replaced
| 260:8b85949bde00 | 261:d9d178d1457c |
|---|---|
| 239 import OD | 239 import OD |
| 240 -- open inOrdinal C-Ordinal | 240 -- open inOrdinal C-Ordinal |
| 241 open OD (C-Ordinal {n}) | 241 open OD (C-Ordinal {n}) |
| 242 open OD.OD | 242 open OD.OD |
| 243 | 243 |
| 244 -- | |
| 245 -- another form of regularity | |
| 246 -- | |
| 247 ε-induction : {m : Level} { ψ : OD → Set m} | |
| 248 → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) | |
| 249 → (x : OD ) → ψ x | |
| 250 ε-induction {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x))) <-osuc) where | |
| 251 ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly } | |
| 252 → (ly < lx) ∨ (oy d< ox ) → ψ (ord→od (record { lv = ly ; ord = oy } ) ) | |
| 253 ε-induction-ord lx (OSuc lx ox) {ly} {oy} y<x = | |
| 254 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where | |
| 255 lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → od→ord z o< record { lv = lx ; ord = ox } | |
| 256 lemma z lt with osuc-≡< y<x | |
| 257 lemma z lt | case1 refl = o<-subst (c<→o< lt) refl diso | |
| 258 lemma z lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 | |
| 259 ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) = | |
| 260 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt ) where | |
| 261 -- | |
| 262 -- if lv of z if less than x Ok | |
| 263 -- else lv z = lv x. We can create OSuc of z which is larger than z and less than x in lemma | |
| 264 -- | |
| 265 -- lx Suc lx (1) lz(a) <lx by case1 | |
| 266 -- ly(1) ly(2) (2) lz(b) <lx by case1 | |
| 267 -- lz(a) lz(b) lz(c) lz(c) <lx by case2 ( ly==lz==lx) | |
| 268 -- | |
| 269 lemma0 : { lx ly : Nat } → ly < Suc lx → lx < ly → ⊥ | |
| 270 lemma0 {Suc lx} {Suc ly} (s≤s lt1) (s≤s lt2) = lemma0 lt1 lt2 | |
| 271 lemma1 : {ly : Nat} {oy : OrdinalD {suc n} ly} → lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) ≡ ly | |
| 272 lemma1 {ly} {oy} = let open ≡-Reasoning in begin | |
| 273 lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) | |
| 274 ≡⟨ cong ( λ k → lv k ) diso ⟩ | |
| 275 lv (record { lv = ly ; ord = oy }) | |
| 276 ≡⟨⟩ | |
| 277 ly | |
| 278 ∎ | |
| 279 lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z | |
| 280 lemma z lt with c<→o< {z} {ord→od (record { lv = ly ; ord = oy })} lt | |
| 281 lemma z lt | case1 lz<ly with <-cmp lx ly | |
| 282 lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen | |
| 283 lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- ly(1) | |
| 284 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) )) | |
| 285 lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- lz(a) | |
| 286 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c)))) | |
| 287 lemma z lt | case2 lz=ly with <-cmp lx ly | |
| 288 lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen | |
| 289 lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- lz(b) | |
| 290 ... | eq = subst (λ k → ψ k ) oiso | |
| 291 (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) | |
| 292 lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly -- lz(c) | |
| 293 ... | eq = subst (λ k → ψ k ) oiso ( ε-induction-ord lx (dz oz=lx) {lv (od→ord z)} {ord (od→ord z)} (case2 (dz<dz oz=lx) )) where | |
| 294 oz=lx : lv (od→ord z) ≡ lx | |
| 295 oz=lx = let open ≡-Reasoning in begin | |
| 296 lv (od→ord z) | |
| 297 ≡⟨ eq ⟩ | |
| 298 lv (od→ord (ord→od (ordinal ly oy))) | |
| 299 ≡⟨ cong ( λ k → lv k ) diso ⟩ | |
| 300 lv (ordinal ly oy) | |
| 301 ≡⟨ sym lx=ly ⟩ | |
| 302 lx | |
| 303 ∎ | |
| 304 dz : lv (od→ord z) ≡ lx → OrdinalD lx | |
| 305 dz refl = OSuc lx (ord (od→ord z)) | |
| 306 dz<dz : (z=x : lv (od→ord z) ≡ lx ) → ord (od→ord z) d< dz z=x | |
| 307 dz<dz refl = s<refl | |
| 308 |