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

comparison HOD.agda @ 151:b5a337fb7a6d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
recovering...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 09 Jul 2019 09:56:38 +0900
parents ebcbfd9d9c8e
children 996a67042f50
comparison
equal deleted inserted replaced
150:ebcbfd9d9c8e 151:b5a337fb7a6d
309 309
310 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) 310 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x)
311 empty x (case1 ()) 311 empty x (case1 ())
312 empty x (case2 ()) 312 empty x (case2 ())
313 313
314 ord-⊆ : ( t x : OD {suc n} ) → _⊆_ t (Ord (od→ord t )) {x}
315 ord-⊆ t x lt = c<→o< lt
316
314 union-d : (X : OD {suc n}) → OD {suc n} 317 union-d : (X : OD {suc n}) → OD {suc n}
315 union-d X = record { def = λ y → def X (osuc y) } 318 union-d X = record { def = λ y → def X (osuc y) }
316 union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n} 319 union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
317 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) ) 320 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
318 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 321 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
361 --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A 364 --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A
362 --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A 365 --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A
363 -- 366 --
364 -- if Power A ∋ t, from a propertiy of minimum sup there is osuc ZFSubset A ∋ t 367 -- if Power A ∋ t, from a propertiy of minimum sup there is osuc ZFSubset A ∋ t
365 -- then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x 368 -- then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x
366 -- In case of later, ZFSubset A ∋ t and t ∋ x implies A ∋ x by transitivity 369 -- In case of later, ZFSubset A ∋ t and t ∋ x implies A ∋ x by transitivity of Ordinals
367 -- 370 --
368 POrd : {a : Ordinal } {t : OD} → Def (Ord a) ∋ t → Def (Ord a) ∋ Ord (od→ord t)
369 POrd {a} {t} P∋t = {!!}
370 ∩-≡ : { a b : OD {suc n} } → ({x : OD {suc n} } → (a ∋ x → b ∋ x)) → a == ( b ∩ a ) 371 ∩-≡ : { a b : OD {suc n} } → ({x : OD {suc n} } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
371 ∩-≡ {a} {b} inc = record { 372 ∩-≡ {a} {b} inc = record {
372 eq→ = λ {x} x<a → record { proj2 = x<a ; 373 eq→ = λ {x} x<a → record { proj2 = x<a ;
373 proj1 = def-subst {suc n} {_} {_} {b} {x} (inc (def-subst {suc n} {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; 374 proj1 = def-subst {suc n} {_} {_} {b} {x} (inc (def-subst {suc n} {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ;
374 eq← = λ {x} x<a∩b → proj2 x<a∩b } 375 eq← = λ {x} x<a∩b → proj2 x<a∩b }
375 ord-power→ : (a : Ordinal ) ( t : OD) → Def (Ord a) ∋ t → {x : OD} → t ∋ x → Ord a ∋ x 376 ord-power→ : (a : Ordinal ) ( t : OD) → Def (Ord a) ∋ t → {x : OD} → t ∋ x → Ord a ∋ x
376 ord-power→ a t P∋t {x} t∋x with osuc-≡< (sup-lb (POrd P∋t)) 377 ord-power→ a t P∋t {x} t∋x with osuc-≡< (sup-lb P∋t )
377 ... | case1 eq = proj1 (def-subst (Ltx t∋x) (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl ) where 378 ... | case1 eq = proj1 (def-subst t∋x (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl )
378 Ltx : {n : Level} → {x t : OD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
379 Ltx {n} {x} {t} lt = c<→o< lt
380 ... | case2 lt = lemma3 where 379 ... | case2 lt = lemma3 where
381 sp = sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))) 380 sp = sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))
382 minsup : OD 381 minsup : OD
383 minsup = ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) 382 minsup = ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))))
384 Ltx : {n : Level} → {x t : OD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x 383 Ltx : {n : Level} → {x t : OD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
385 Ltx {n} {x} {t} lt = c<→o< lt 384 Ltx {n} {x} {t} lt = c<→o< lt
386 -- lemma1 hold because minsup is Ord (minα a sp) 385 -- lemma1 hold because a subset of ordinals is ordinal
387 lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t) 386 lemma1 : od→ord t o< od→ord minsup → minsup ∋ Ord (od→ord t)
388 lemma1 lt with OrdSubset a ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))) 387 lemma1 lt = {!!}
389 ... | eq with subst ( λ k → ZFSubset (Ord a) k ≡ Ord (minα a sp)) {!!} eq
390 ... | eq1 = def-subst {suc n} {_} {_} {minsup} {od→ord (Ord (od→ord t))} {!!} lemma2 {!!} where
391 lemma2 : Ord (od→ord (ZFSubset (Ord a) (ord→od sp))) ≡ minsup
392 lemma2 = let open ≡-Reasoning in begin
393 Ord (od→ord (ZFSubset (Ord a) (ord→od sp)))
394 ≡⟨ cong (λ k → Ord (od→ord k)) eq1 ⟩
395 Ord (od→ord (Ord (minα a sp)))
396 ≡⟨ cong (λ k → Ord (od→ord k)) {!!} ⟩
397 Ord (od→ord (ord→od (minα a sp)))
398 ≡⟨ cong (λ k → Ord k) diso ⟩
399 Ord (minα a sp)
400 ≡⟨ sym eq1 ⟩
401 minsup
402 ∎
403 lemma3 : od→ord x o< a 388 lemma3 : od→ord x o< a
404 lemma3 = otrans (proj1 (lemma1 lt) ) (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) 389 lemma3 = otrans (proj1 (lemma1 lt)) (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) )
405 -- 390 --
406 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t 391 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
407 -- Power A is a sup of ZFSubset A t, so Power A ∋ t 392 -- Power A is a sup of ZFSubset A t, so Power A ∋ t
408 -- 393 --
409 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t 394 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
442 lemma0 : {x : OD} → t ∋ x → Ord a ∋ x 427 lemma0 : {x : OD} → t ∋ x → Ord a ∋ x
443 lemma0 {x} t∋x = c<→o< (t→A t∋x) 428 lemma0 {x} t∋x = c<→o< (t→A t∋x)
444 lemma3 : Def (Ord a) ∋ t 429 lemma3 : Def (Ord a) ∋ t
445 lemma3 = ord-power← a t lemma0 430 lemma3 = ord-power← a t lemma0
446 lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t)) 431 lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t))
447 lemma4 = cong ( λ k → od→ord k ) ( ==→o≡ (subst (λ k → t == (A ∩ k)) {!!} {!!} )) 432 lemma4 = {!!}
448 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x)) 433 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x))
449 lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t} 434 lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t}
450 ... | lt = o<-subst {suc n} {_} {_} {_} {_} lt (sym (subst (λ k → od→ord t ≡ k) lemma5 lemma4 )) refl where 435 ... | lt = o<-subst {suc n} {_} {_} {_} {_} lt (sym (subst (λ k → od→ord t ≡ k) lemma5 lemma4 )) refl where
451 lemma5 : od→ord (A ∩ Ord (od→ord t)) ≡ od→ord (A ∩ ord→od (od→ord t)) 436 lemma5 : od→ord (A ∩ Ord (od→ord t)) ≡ od→ord (A ∩ ord→od (od→ord t))
452 lemma5 = cong (λ k → od→ord (A ∩ k )) {!!} 437 lemma5 = cong (λ k → od→ord (A ∩ k )) {!!}
453 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) 438 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
454 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = {!!} }) ) where 439 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
440 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
441 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A )))
455 442
456 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 443 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
457 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq 444 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq
458 regularity : (x : OD) (not : ¬ (x == od∅)) → 445 regularity : (x : OD) (not : ¬ (x == od∅)) →
459 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) 446 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)