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

comparison HOD.agda @ 159:3675bd617ac8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
infinite continue...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 15 Jul 2019 09:31:32 +0900
parents b97b4ee06f01
children ebac6fa116fa
comparison
equal deleted inserted replaced
158:b97b4ee06f01 159:3675bd617ac8
61 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x 61 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
62 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x 62 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
63 -- we should prove this in agda, but simply put here 63 -- we should prove this in agda, but simply put here
64 ==→o≡ : {n : Level} → { x y : OD {suc n} } → (x == y) → x ≡ y 64 ==→o≡ : {n : Level} → { x y : OD {suc n} } → (x == y) → x ≡ y
65 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set 65 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
66 -- o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → def (ord→od y) x 66 -- o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → def (ord→od y) x
67 -- ord→od x ≡ Ord x results the same
67 -- supermum as Replacement Axiom 68 -- supermum as Replacement Axiom
68 sup-o : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} 69 sup-o : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n}
69 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ 70 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ
70 -- contra-position of mimimulity of supermum required in Power Set Axiom 71 -- contra-position of mimimulity of supermum required in Power Set Axiom
71 sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} 72 sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n}
285 infixr 220 _⊆_ 286 infixr 220 _⊆_
286 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (Ord omega) 287 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (Ord omega)
287 isZF = record { 288 isZF = record {
288 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } 289 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
289 ; pair = pair 290 ; pair = pair
290 ; union-u = λ X z UX∋z → union-u {X} {z} UX∋z
291 ; union→ = union→ 291 ; union→ = union→
292 ; union← = union← 292 ; union← = union←
293 ; empty = empty 293 ; empty = empty
294 ; power→ = power→ 294 ; power→ = power→
295 ; power← = power← 295 ; power← = power←
321 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc 321 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc
322 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc 322 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
323 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl ) 323 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl )
324 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) 324 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
325 325
326 Union-o : (X : Ordinal {suc n}) → OD {suc n}
327 Union-o X = record { def = λ y → osuc y o< X }
328
329 union-ou : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
330 union-ou {X} {z} U>z = ord→od ( osuc ( od→ord z ) )
331 ord-union→ : (x : Ordinal) (z u : OD) → (Ord x ∋ u) ∧ (u ∋ z) → Union-o x ∋ z
332 ord-union→ x z u plt with trio< ( od→ord u ) ( osuc ( od→ord z ))
333 ord-union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx))
334 ord-union→ X z u xx | tri< a ¬b ¬c | ()
335 ord-union→ X z u xx | tri≈ ¬a b ¬c = def-subst (c<→o< (proj1 xx )) refl refl where
336 ord-union→ X z u xx | tri> ¬a ¬b c = {!!}
337
338 ord-union← : (x : Ordinal) (z : OD) (UX∋z : Union-o x ∋ z)
339 → (Ord x ∋ union-ou {Ord x} {z} {!!} ) ∧ (union-ou {Ord x} {z} {!!} ∋ z )
340 ord-union← x z UX∋z = record { proj1 = lemma ; proj2 = {!!} } where
341 lemma : Ord x ∋ union-ou {Ord x} {z} {!!}
342 lemma = def-subst {suc n} {_} {_} {Ord x} {_} UX∋z refl (sym diso)
343
344 union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n} 326 union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
345 union-u {X} {z} U>z = ord→od ( osuc ( od→ord z ) ) 327 union-u {X} {z} U>z = ord→od ( osuc ( od→ord z ) )
346 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 328 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
347 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx 329 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
348 ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) 330 ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
349 331
350 union←' : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) 332 union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
351 union←' X z UX∋z = TransFiniteExists _ UX∋z 333 union← X z UX∋z = TransFiniteExists _ UX∋z
352 ( λ {y} xx not → not (ord→od y) (record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } )) 334 ( λ {y} xx not → not (ord→od y) (record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } ))
353 union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
354 union← X z UX∋z = record { proj1 = lemma ; proj2 = lemma2 } where
355 lemma : X ∋ union-u {X} {z} UX∋z
356 lemma = {!!} -- def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} UX∋z refl {!!}
357 lemma2 : union-u {X} UX∋z ∋ z
358 lemma2 = {!!}
359 335
360 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y 336 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y
361 ψiso {ψ} t refl = t 337 ψiso {ψ} t refl = t
362 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) 338 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
363 selection {ψ} {X} {y} = record { 339 selection {ψ} {X} {y} = record {
484 460
485 extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B 461 extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
486 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d 462 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
487 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d 463 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
488 464
489 open import Relation.Binary.PropositionalEquality
490 uxxx-ord : {x : OD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) ) 465 uxxx-ord : {x : OD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) )
491 uxxx-ord {x} {y} = subst (λ k → k ⇔ ( y o< osuc (od→ord x) )) (sym lemma) ( osuc2 y (od→ord x)) where 466 uxxx-ord {x} {y} = subst (λ k → def (Union (k , (k , k))) y ⇔ ( y o< osuc (od→ord x) ) ) oiso lemma where
492 lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x)) 467 ordΦ : {lx : Nat } → Ordinal {suc n}
493 lemma {y} = let open ≡-Reasoning in begin 468 ordΦ {lx} = record { lv = lx ; ord = Φ lx }
494 def (Union (x , (x , x))) y 469 odΦ : {lx : Nat } → OD {suc n}
495 ≡⟨ {!!} ⟩ 470 odΦ {lx} = ord→od ordΦ
496 def ( Ord ( omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) ))) ( osuc y ) 471 xord : {lx : Nat } → { ox : OrdinalD {suc n} lx } → Ordinal {suc n}
497 ≡⟨⟩ 472 xord {lx} {ox} = record { lv = lx ; ord = ox }
498 osuc y o< omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) ) 473 xod : {lx : Nat } → { ox : OrdinalD {suc n} lx } → OD {suc n}
499 ≡⟨ cong (λ k → osuc y o< omax (od→ord x) k ) {!!} ⟩ 474 xod {lx} {ox} = ord→od (xord {lx} {ox})
500 osuc y o< omax (od→ord x) (omax (od→ord x) (od→ord x) ) 475 lemmaφ : (lx : Nat) → def (Union (odΦ {lx} , (odΦ {lx} , odΦ {lx} ))) y ⇔ (y o< osuc (record { lv = lx ; ord = Φ lx }))
501 ≡⟨ cong (λ k → osuc y o< k ) (omxxx (od→ord x) ) ⟩ 476 proj1 (lemmaφ lx) = {!!}
502 osuc y o< osuc (osuc (od→ord x)) 477 proj2 (lemmaφ lx) lt not = not (ordΦ {lx}){!!}
503 ∎ 478 lemma-suc : (lx : Nat) (ox : OrdinalD lx) →
479 def (Union (xod {lx} {ox} , (xod {lx} {ox} , xod {lx} {ox} ))) y ⇔ (y o< osuc (xord {lx} {ox})) →
480 def (Union (xod {lx} {OSuc lx ox} , (xod {lx} {OSuc lx ox} , xod {lx} {OSuc lx ox} ))) y
481 ⇔ (y o< osuc (xord {lx} {OSuc lx ox}))
482 proj1 (lemma-suc lx ox prev) = {!!}
483 proj2 (lemma-suc lx ox prev) lt not = not (xord {lx} {ox}) {!!}
484 lemma = TransFinite {suc n} {λ ox → def (Union (ord→od ox , (ord→od ox , ord→od ox))) y ⇔ ( y o< osuc ox ) }
485 lemmaφ lemma-suc (od→ord x) where
486
504 infinite : OD {suc n} 487 infinite : OD {suc n}
505 infinite = Ord omega 488 infinite = Ord omega
506 infinity∅ : Ord omega ∋ od∅ {suc n} 489 infinity∅ : Ord omega ∋ od∅ {suc n}
507 infinity∅ = o<-subst (case1 (s≤s z≤n) ) (sym ord-od∅) refl 490 infinity∅ = o<-subst (case1 (s≤s z≤n) ) (sym ord-od∅) refl
508 infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x )) 491 infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
509 infinity x lt = o<-subst ( lemma (od→ord x) lt ) eq refl where 492 infinity x lt = o<-subst ( lemma (od→ord x) lt ) eq refl where
510 eq : osuc (od→ord x) ≡ od→ord (Union (x , (x , x))) 493 eq : osuc (od→ord x) ≡ od→ord (Union (x , (x , x)))
511 eq = let open ≡-Reasoning in begin 494 eq = let open ≡-Reasoning in begin
512 osuc (od→ord x) 495 osuc (od→ord x)
513 ≡⟨ {!!} ⟩ 496 ≡⟨ {!!} ⟩
514 od→ord (Ord (osuc (od→ord x)))
515 ≡⟨ cong ( λ k → od→ord k ) ( sym (==→o≡ ( ⇔→== uxxx-ord ))) ⟩
516 od→ord (Union (x , (x , x))) 497 od→ord (Union (x , (x , x)))
517 ∎ 498 ∎
518 lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega 499 lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega
519 lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n) 500 lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n)
520 lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n) 501 lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n)