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

comparison HOD.agda @ 176:ecb329ba38ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ε-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