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

comparison HOD.agda @ 144:3ba37037faf4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Union again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 Jul 2019 13:21:14 +0900
parents 21b9e78e9359
children f0fa9a755513
comparison
equal deleted inserted replaced
143:21b9e78e9359 144:3ba37037faf4
290 ; Select = Select 290 ; Select = Select
291 ; Replace = Replace 291 ; Replace = Replace
292 ; infinite = Ord omega 292 ; infinite = Ord omega
293 ; isZF = isZF 293 ; isZF = isZF
294 } where 294 } where
295 ZFSet = OD {suc n}
295 Select : (X : OD {suc n} ) → ((x : OD {suc n} ) → Set (suc n) ) → OD {suc n} 296 Select : (X : OD {suc n} ) → ((x : OD {suc n} ) → Set (suc n) ) → OD {suc n}
296 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } 297 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) }
297 Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n} 298 Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
298 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } 299 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
299 _,_ : OD {suc n} → OD {suc n} → OD {suc n} 300 _,_ : OD {suc n} → OD {suc n} → OD {suc n}
300 x , y = Ord (omax (od→ord x) (od→ord y)) 301 x , y = Ord (omax (od→ord x) (od→ord y))
302 _∩_ : ( A B : ZFSet ) → ZFSet
303 A ∩ B = record { def = λ x → def A x ∧ def B x } -- Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) )
301 Union : OD {suc n} → OD {suc n} 304 Union : OD {suc n} → OD {suc n}
302 Union U = cseq U 305 Union U = Replace ( record { def = λ x → osuc x o< od→ord U } ) ( λ x → U ∩ x )
303 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) 306 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x )
304 ZFSet = OD {suc n}
305 _∈_ : ( A B : ZFSet ) → Set (suc n) 307 _∈_ : ( A B : ZFSet ) → Set (suc n)
306 A ∈ B = B ∋ A 308 A ∈ B = B ∋ A
307 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n) 309 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n)
308 _⊆_ A B {x} = A ∋ x → B ∋ x 310 _⊆_ A B {x} = A ∋ x → B ∋ x
309 _∩_ : ( A B : ZFSet ) → ZFSet
310 A ∩ B = record { def = λ x → def A x ∧ def B x } -- Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) )
311 Power : OD {suc n} → OD {suc n} 311 Power : OD {suc n} → OD {suc n}
312 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) 312 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
313 -- _∪_ : ( A B : ZFSet ) → ZFSet 313 -- _∪_ : ( A B : ZFSet ) → ZFSet
314 -- A ∪ B = Select (A , B) ( λ x → (A ∋ x) ∨ ( B ∋ x ) ) 314 -- A ∪ B = Select (A , B) ( λ x → (A ∋ x) ∨ ( B ∋ x ) )
315 ｛_｝ : ZFSet → ZFSet 315 ｛_｝ : ZFSet → ZFSet
344 344
345 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) 345 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x)
346 empty x (case1 ()) 346 empty x (case1 ())
347 empty x (case2 ()) 347 empty x (case2 ())
348 348
349 union-lemma : {n : Level } {X z u : OD {suc n} } → (X ∋ u) → (u ∋ z) → osuc ( od→ord z ) o< od→ord u → X ∋ Ord (osuc ( od→ord z ) )
350 union-lemma = {!!}
351 union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
352 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
353 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
354 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))
355 union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx))
356 union→ X z u xx | tri< a ¬b ¬c | ()
357 union→ X z u xx | tri≈ ¬a b ¬c = {!!}
358 union→ X z u xx | tri> ¬a ¬b c = {!!} --- osuc ( od→ord z )) o< od→ord u o< od→ord X
359 -- def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (union-lemma {n} {X} {z} {u} (proj1 xx) (proj2 xx) c ) refl (sym ord-Ord)
360 union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
361 union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
362 lemma : X ∋ union-u {X} {z} X∋z
363 lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} {!!} refl ord-Ord
364
365 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y
366 ψiso {ψ} t refl = t
367 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
368 selection {ψ} {X} {y} = record {
369 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) }
370 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso }
371 }
372 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x
373 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where
374 lemma : def (in-codomain X ψ) (od→ord (ψ x))
375 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k))
376 (sym (subst (λ k → Ord (od→ord x) ≡ k) oiso (Ord-ord) )) } ))
377 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
378 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
379 lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y))))
380 → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)))
381 lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
382 lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (Ord y))) → (ord→od (od→ord x) == ψ (Ord y))
383 lemma3 {y} eq = subst (λ k → ord→od (od→ord x) == k ) oiso (o≡→== eq )
384 lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) )
385 lemma not y not2 = not (Ord y) (subst (λ k → k == ψ (Ord y)) oiso ( proj2 not2 ))
386
387 ---
388 --- Power Set
389 ---
390 --- First consider ordinals in OD
349 --- 391 ---
350 --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A 392 --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A
351 --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A 393 --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A
352 -- 394 --
353 -- if Power A ∋ t, from a propertiy of minimum sup there is osuc ZFSubset A ∋ t 395 -- if Power A ∋ t, from a propertiy of minimum sup there is osuc ZFSubset A ∋ t
407 → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t 449 → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
408 lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq )) 450 lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq ))
409 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x))) 451 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
410 lemma = sup-o< 452 lemma = sup-o<
411 453
412 union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n} 454 --
413 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) ) 455 -- Every set in OD is a subset of Ordinals
414 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 456 --
415 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))
416 union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx))
417 union→ X z u xx | tri< a ¬b ¬c | ()
418 union→ X z u xx | tri≈ ¬a b ¬c = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b
419 union→ X z u xx | tri> ¬a ¬b c = {!!} --- osuc ( od→ord z )) o< od→ord u o< od→ord X
420
421 union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
422 union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
423 lemma : X ∋ union-u {X} {z} X∋z
424 lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} X∋z refl ord-Ord
425
426 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y
427 ψiso {ψ} t refl = t
428 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
429 selection {ψ} {X} {y} = record {
430 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) }
431 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso }
432 }
433 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x
434 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where
435 lemma : def (in-codomain X ψ) (od→ord (ψ x))
436 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k))
437 (sym (subst (λ k → Ord (od→ord x) ≡ k) oiso (Ord-ord) )) } ))
438 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
439 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
440 lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y))))
441 → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)))
442 lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
443 lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (Ord y))) → (ord→od (od→ord x) == ψ (Ord y))
444 lemma3 {y} eq = subst (λ k → ord→od (od→ord x) == k ) oiso (o≡→== eq )
445 lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) )
446 lemma not y not2 = not (Ord y) (subst (λ k → k == ψ (Ord y)) oiso ( proj2 not2 ))
447
448 -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y ) 457 -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y )
449 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x 458 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
450 power→ A t P∋t {x} t∋x = TransFiniteExists {suc n} {λ y → (t == (A ∩ ord→od y))} 459 power→ A t P∋t {x} t∋x = TransFiniteExists {suc n} {λ y → (t == (A ∩ ord→od y))}
451 lemma4 lemma5 where 460 lemma4 lemma5 where
452 a = od→ord A 461 a = od→ord A
497 uxxx-ord : {x : OD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) ) 506 uxxx-ord : {x : OD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) )
498 uxxx-ord {x} {y} = subst (λ k → k ⇔ ( y o< osuc (od→ord x) )) (sym lemma) ( osuc2 y (od→ord x)) where 507 uxxx-ord {x} {y} = subst (λ k → k ⇔ ( y o< osuc (od→ord x) )) (sym lemma) ( osuc2 y (od→ord x)) where
499 lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x)) 508 lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x))
500 lemma {y} = let open ≡-Reasoning in begin 509 lemma {y} = let open ≡-Reasoning in begin
501 def (Union (x , (x , x))) y 510 def (Union (x , (x , x))) y
502 ≡⟨⟩ 511 ≡⟨ {!!} ⟩
503 def ( Ord ( omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) ))) ( osuc y ) 512 def ( Ord ( omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) ))) ( osuc y )
504 ≡⟨⟩ 513 ≡⟨⟩
505 osuc y o< omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) ) 514 osuc y o< omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) )
506 ≡⟨ cong (λ k → osuc y o< omax (od→ord x) k ) (sym ord-Ord) ⟩ 515 ≡⟨ cong (λ k → osuc y o< omax (od→ord x) k ) (sym ord-Ord) ⟩
507 osuc y o< omax (od→ord x) (omax (od→ord x) (od→ord x) ) 516 osuc y o< omax (od→ord x) (omax (od→ord x) (od→ord x) )