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

comparison HOD.agda @ 161:4c704b7a62e4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ininite done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 15 Jul 2019 18:26:56 +0900
parents ebac6fa116fa
children b06f5d2f34b1
comparison
equal deleted inserted replaced
160:ebac6fa116fa 161:4c704b7a62e4
245 -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x 245 -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x
246 246
247 omega : { n : Level } → Ordinal {n} 247 omega : { n : Level } → Ordinal {n}
248 omega = record { lv = Suc Zero ; ord = Φ 1 } 248 omega = record { lv = Suc Zero ; ord = Φ 1 }
249 249
250 od-infinite : {n : Level} → OD {suc n}
251 od-infinite = record { def = λ x → x o< sup-o ( λ y → od→ord (Ord y)) }
252
253 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} 250 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
254 OD→ZF {n} = record { 251 OD→ZF {n} = record {
255 ZFSet = OD {suc n} 252 ZFSet = OD {suc n}
256 ; _∋_ = _∋_ 253 ; _∋_ = _∋_
257 ; _≈_ = _==_ 254 ; _≈_ = _==_
259 ; _,_ = _,_ 256 ; _,_ = _,_
260 ; Union = Union 257 ; Union = Union
261 ; Power = Power 258 ; Power = Power
262 ; Select = Select 259 ; Select = Select
263 ; Replace = Replace 260 ; Replace = Replace
264 ; infinite = od-infinite 261 ; infinite = infinite
265 ; isZF = isZF 262 ; isZF = isZF
266 } where 263 } where
267 ZFSet = OD {suc n} 264 ZFSet = OD {suc n}
268 Select : (X : OD {suc n} ) → ((x : OD {suc n} ) → Set (suc n) ) → OD {suc n} 265 Select : (X : OD {suc n} ) → ((x : OD {suc n} ) → Set (suc n) ) → OD {suc n}
269 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } 266 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) }
282 Power : OD {suc n} → OD {suc n} 279 Power : OD {suc n} → OD {suc n}
283 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) 280 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
284 ｛_｝ : ZFSet → ZFSet 281 ｛_｝ : ZFSet → ZFSet
285 ｛ x ｝ = ( x , x ) 282 ｛ x ｝ = ( x , x )
286 283
284 data infinite-d : ( x : Ordinal {suc n} ) → Set (suc n) where
285 iφ : infinite-d o∅
286 isuc : {x : Ordinal {suc n} } → infinite-d x →
287 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
288
289 infinite : OD {suc n}
290 infinite = record { def = λ x → infinite-d x }
291
287 infixr 200 _∈_ 292 infixr 200 _∈_
288 -- infixr 230 _∩_ _∪_ 293 -- infixr 230 _∩_ _∪_
289 infixr 220 _⊆_ 294 infixr 220 _⊆_
290 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace od-infinite 295 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite
291 isZF = record { 296 isZF = record {
292 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } 297 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
293 ; pair = pair 298 ; pair = pair
294 ; union→ = union→ 299 ; union→ = union→
295 ; union← = union← 300 ; union← = union←
463 468
464 extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B 469 extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
465 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d 470 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
466 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d 471 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
467 472
468 uxxx-ord : {x : OD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) ) 473
469 uxxx-ord {x} {y} = subst (λ k → def (Union (k , (k , k))) y ⇔ ( y o< osuc (od→ord x) ) ) oiso lemma where 474 infinity∅ : infinite ∋ od∅ {suc n}
470 ordΦ : {lx : Nat } → Ordinal {suc n} 475 infinity∅ = def-subst {suc n} {_} {_} {infinite} {od→ord (od∅ {suc n})} iφ refl lemma where
471 ordΦ {lx} = record { lv = lx ; ord = Φ lx } 476 lemma : o∅ ≡ od→ord od∅
472 odΦ : {lx : Nat } → OD {suc n} 477 lemma = let open ≡-Reasoning in begin
473 odΦ {lx} = ord→od ordΦ 478 o∅
474 xord : {lx : Nat } → { ox : OrdinalD {suc n} lx } → Ordinal {suc n} 479 ≡⟨ sym diso ⟩
475 xord {lx} {ox} = record { lv = lx ; ord = ox } 480 od→ord ( ord→od o∅ )
476 xod : {lx : Nat } → { ox : OrdinalD {suc n} lx } → OD {suc n} 481 ≡⟨ cong ( λ k → od→ord k ) o∅≡od∅ ⟩
477 xod {lx} {ox} = ord→od (xord {lx} {ox}) 482 od→ord od∅
478 lemmaφ : (lx : Nat) → def (Union (odΦ {lx} , (odΦ {lx} , odΦ {lx} ))) y ⇔ (y o< osuc (record { lv = lx ; ord = Φ lx })) 483 ∎
479 proj1 (lemmaφ lx) df = TransFiniteExists _ df lemma where 484 infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
480 lemma : {y1 : Ordinal} → def (odΦ {lx} , (odΦ {lx} , odΦ {lx} )) y1 ∧ def (ord→od y1) y → y o< xord {lx} {OSuc lx (Φ lx)} 485 infinity x lt = def-subst {suc n} {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where
481 lemma {y1} xx with proj1 xx | c<→o< {suc n} {ord→od y} {ord→od y1} (def-subst {suc n} {ord→od y1} {y} (proj2 xx) refl (sym diso)) 486 lemma : od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x))))
482 -- x : lv y1 < lx , x₁ : lv (od→ord (ord→od y) < lv y1 -> lv y < lx 487 ≡ od→ord (Union (x , (x , x)))
483 lemma {y1} xx | case1 x | case1 x₁ = 488 lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso
484 case1 ( <-trans (subst (λ k → lv k < lv (od→ord (ord→od y1))) diso x₁) (subst (λ k → lv k < lx ) (sym diso) {!!}) ) 489
485 lemma {y1} xx | case1 x | case2 x₁ with d<→lv x₁
486 ... | eq = case1 {!!}
487 lemma {y1} xx | case2 x | lt = {!!}
488 proj2 (lemmaφ lx) lt not = not (ordΦ {lx}){!!}
489 lemma-suc : (lx : Nat) (ox : OrdinalD lx) →
490 def (Union (xod {lx} {ox} , (xod {lx} {ox} , xod {lx} {ox} ))) y ⇔ (y o< osuc (xord {lx} {ox})) →
491 def (Union (xod {lx} {OSuc lx ox} , (xod {lx} {OSuc lx ox} , xod {lx} {OSuc lx ox} ))) y
492 ⇔ (y o< osuc (xord {lx} {OSuc lx ox}))
493 proj1 (lemma-suc lx ox prev) df = TransFiniteExists _ df {!!}
494 proj2 (lemma-suc lx ox prev) lt not = not (xord {lx} {ox}) {!!}
495 lemma = TransFinite {suc n} {λ ox → def (Union (ord→od ox , (ord→od ox , ord→od ox))) y ⇔ ( y o< osuc ox ) }
496 lemmaφ lemma-suc (od→ord x) where
497
498 infinity∅ : od-infinite ∋ od∅ {suc n}
499 infinity∅ = {!!} -- o<-subst (case1 (s≤s z≤n) ) (sym ord-od∅) refl
500 infinity : (x : OD) → od-infinite ∋ x → od-infinite ∋ Union (x , (x , x ))
501 infinity x lt = {!!} where
502 lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega
503 lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n)
504 lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n)
505 lemma record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } (case1 (s≤s ()))
506 lemma record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } (case1 (s≤s ()))
507 lemma record { lv = 1 ; ord = (Φ 1) } (case2 c2) with d<→lv c2
508 lemma record { lv = (Suc Zero) ; ord = (Φ .1) } (case2 ()) | refl
509 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] -- this form is no good since X is a transitive set 490 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] -- this form is no good since X is a transitive set
510 -- ∀ z [ ∀ x ( x ∈ z → ¬ ( x ≈ ∅ ) ) ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y ) → x ∩ y ≈ ∅ ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ] 491 -- ∀ z [ ∀ x ( x ∈ z → ¬ ( x ≈ ∅ ) ) ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y ) → x ∩ y ≈ ∅ ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ]
511 record Choice (z : OD {suc n}) : Set (suc (suc n)) where 492 record Choice (z : OD {suc n}) : Set (suc (suc n)) where
512 field 493 field
513 u : {x : OD {suc n}} ( x∈z : x ∈ z ) → OD {suc n} 494 u : {x : OD {suc n}} ( x∈z : x ∈ z ) → OD {suc n}