Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison HOD.agda @ 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 | aa89d1b8ce96 |
comparison
equal
deleted
inserted
replaced
175:51189f7b9229 | 176:ecb329ba38ac |
---|---|
233 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α ) | 233 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α ) |
234 cseq ( Ord (od→ord (L {n} (record { lv = lx ; ord = Φ lx })))) | 234 cseq ( Ord (od→ord (L {n} (record { lv = lx ; ord = Φ lx })))) |
235 | 235 |
236 -- L0 : {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α | 236 -- L0 : {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α |
237 -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x | 237 -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x |
238 | |
239 -- another form of regularity | |
240 -- | |
241 -- {-# TERMINATING #-} | |
242 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} | |
243 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) | |
244 → (x : OD {suc n} ) → ψ x | |
245 ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x))) <-osuc) where | |
246 ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly } | |
247 → (ly < lx) ∨ (oy d< ox ) → ψ (ord→od (record { lv = ly ; ord = oy } ) ) | |
248 ε-induction-ord Zero (Φ 0) (case1 ()) | |
249 ε-induction-ord Zero (Φ 0) (case2 ()) | |
250 ε-induction-ord lx (OSuc lx ox) {ly} {oy} y<x = | |
251 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where | |
252 lemma : (y : OD) → ord→od record { lv = ly ; ord = oy } ∋ y → od→ord y o< record { lv = lx ; ord = ox } | |
253 lemma y lt with osuc-≡< y<x | |
254 lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso | |
255 lemma y lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 | |
256 ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) = | |
257 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt ) where | |
258 lemma0 : { lx ly : Nat } → ly < Suc lx → lx < ly → ⊥ | |
259 lemma0 {Suc lx} {Suc ly} (s≤s lt1) (s≤s lt2) = lemma0 lt1 lt2 | |
260 lemma1 : {n : Level } {ly : Nat} {oy : OrdinalD {suc n} ly} → lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) ≡ ly | |
261 lemma1 {n} {ly} {oy} = let open ≡-Reasoning in begin | |
262 lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) | |
263 ≡⟨ cong ( λ k → lv k ) diso ⟩ | |
264 lv (record { lv = ly ; ord = oy }) | |
265 ≡⟨⟩ | |
266 ly | |
267 ∎ | |
268 lemma2 : { lx : Nat } → lx < Suc lx | |
269 lemma2 {Zero} = s≤s z≤n | |
270 lemma2 {Suc lx} = s≤s (lemma2 {lx}) | |
271 -- lx Suc lx (1) z(a) <lx by case1 | |
272 -- ly(1) ly(2) (2) z(b) <lx by case1 | |
273 -- z(a) z(b) z(c) z(c) <lx by case2 ( ly==z==x) | |
274 -- | |
275 lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z | |
276 lemma z lt with c<→o< {suc n} {z} {ord→od (record { lv = ly ; ord = oy })} lt | |
277 lemma z lt | case1 lz<ly with <-cmp lx ly | |
278 lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen | |
279 lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- (1) | |
280 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) )) | |
281 lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- z(a) | |
282 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c)))) | |
283 lemma z lt | case2 lz=ly with <-cmp lx ly | |
284 lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen | |
285 lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- z(b) | |
286 ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) | |
287 lemma z lt | case2 lz=ly | tri≈ ¬a refl ¬c with d<→lv lz=ly -- z(c) | |
288 ... | eq = lemma6 {lx} {ly} {lv (od→ord z)} {Φ lx} {oy} {ord (od→ord z)} {!!} ? ? where | |
289 lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z | |
290 lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt ) | |
291 lemma6 : { lx ly lz : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } { oz : OrdinalD {suc n} lz } → | |
292 lx ≡ ly → ly ≡ lz → oz d< oy → ψ z | |
293 lemma6 {lx} {ly} {lz} {ox} {oy} {oz} refl refl _ = lemma5 {!!} (case2 {!!} ) | |
294 | 238 |
295 | 239 |
296 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} | 240 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} |
297 OD→ZF {n} = record { | 241 OD→ZF {n} = record { |
298 ZFSet = OD {suc n} | 242 ZFSet = OD {suc n} |
521 choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD | 465 choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD |
522 choice-func X {x} not X∋x = minimul x not | 466 choice-func X {x} not X∋x = minimul x not |
523 choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A | 467 choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A |
524 choice X {A} X∋A not = x∋minimul A not | 468 choice X {A} X∋A not = x∋minimul A not |
525 | 469 |
470 -- another form of regularity | |
471 -- | |
472 -- {-# TERMINATING #-} | |
473 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} | |
474 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) | |
475 → (x : OD {suc n} ) → ψ x | |
476 ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x))) <-osuc) where | |
477 ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly } | |
478 → (ly < lx) ∨ (oy d< ox ) → ψ (ord→od (record { lv = ly ; ord = oy } ) ) | |
479 ε-induction-ord Zero (Φ 0) (case1 ()) | |
480 ε-induction-ord Zero (Φ 0) (case2 ()) | |
481 ε-induction-ord lx (OSuc lx ox) {ly} {oy} y<x = | |
482 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where | |
483 lemma : (y : OD) → ord→od record { lv = ly ; ord = oy } ∋ y → od→ord y o< record { lv = lx ; ord = ox } | |
484 lemma y lt with osuc-≡< y<x | |
485 lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso | |
486 lemma y lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 | |
487 ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) = | |
488 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt ) where | |
489 lemma0 : { lx ly : Nat } → ly < Suc lx → lx < ly → ⊥ | |
490 lemma0 {Suc lx} {Suc ly} (s≤s lt1) (s≤s lt2) = lemma0 lt1 lt2 | |
491 lemma1 : {n : Level } {ly : Nat} {oy : OrdinalD {suc n} ly} → lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) ≡ ly | |
492 lemma1 {n} {ly} {oy} = let open ≡-Reasoning in begin | |
493 lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) | |
494 ≡⟨ cong ( λ k → lv k ) diso ⟩ | |
495 lv (record { lv = ly ; ord = oy }) | |
496 ≡⟨⟩ | |
497 ly | |
498 ∎ | |
499 lemma2 : { lx : Nat } → lx < Suc lx | |
500 lemma2 {Zero} = s≤s z≤n | |
501 lemma2 {Suc lx} = s≤s (lemma2 {lx}) | |
502 -- lx Suc lx (1) z(a) <lx by case1 | |
503 -- ly(1) ly(2) (2) z(b) <lx by case1 | |
504 -- z(a) z(b) z(c) z(c) <lx by case2 ( ly==z==x) | |
505 -- | |
506 lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z | |
507 lemma z lt with c<→o< {suc n} {z} {ord→od (record { lv = ly ; ord = oy })} lt | |
508 lemma z lt | case1 lz<ly with <-cmp lx ly | |
509 lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen | |
510 lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- (1) | |
511 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) )) | |
512 lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- z(a) | |
513 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c)))) | |
514 lemma z lt | case2 lz=ly with <-cmp lx ly | |
515 lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen | |
516 lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- z(b) | |
517 ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) | |
518 lemma z lt | case2 lz=ly | tri≈ ¬a refl ¬c with d<→lv lz=ly -- z(c) | |
519 ... | eq = lemma6 {ly} {Φ lx} {oy} refl (sym (subst (λ k → lv (od→ord z) ≡ k) lemma1 eq)) where | |
520 lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z | |
521 lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt ) | |
522 lemma6 : { ly : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } → | |
523 lx ≡ ly → ly ≡ lv (od→ord z) → ψ z | |
524 lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl) | |
525 |