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

comparison OD.agda @ 260:8b85949bde00

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sup with limit give up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 05 Sep 2019 10:58:06 +0900
parents f714fe999102
children d9d178d1457c
comparison
equal deleted inserted replaced
259:f714fe999102 260:8b85949bde00
73 ==→o≡ : { x y : OD } → (x == y) → x ≡ y 73 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
74 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD 74 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD
75 -- o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x 75 -- o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x
76 -- ord→od x ≡ Ord x results the same 76 -- ord→od x ≡ Ord x results the same
77 -- supermum as Replacement Axiom 77 -- supermum as Replacement Axiom
78 sup-o : Ordinal → ( Ordinal → Ordinal ) → Ordinal 78 sup-o : ( Ordinal → Ordinal ) → Ordinal
79 sup-o< : {X : Ordinal} → { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → x o< X → ψ x o< sup-o X ψ 79 sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ
80 -- contra-position of mimimulity of supermum required in Power Set Axiom 80 -- contra-position of mimimulity of supermum required in Power Set Axiom
81 -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal 81 -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal
82 -- sup-lb : {n : Level } → { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) 82 -- sup-lb : {n : Level } → { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
83 -- mimimul and x∋minimal is an Axiom of choice 83 -- mimimul and x∋minimal is an Axiom of choice
84 minimal : (x : OD ) → ¬ (x == od∅ )→ OD 84 minimal : (x : OD ) → ¬ (x == od∅ )→ OD
104 cseq x = record { def = λ y → def x (osuc y) } where 104 cseq x = record { def = λ y → def x (osuc y) } where
105 105
106 def-subst : {Z : OD } {X : Ordinal }{z : OD } {x : Ordinal }→ def Z X → Z ≡ z → X ≡ x → def z x 106 def-subst : {Z : OD } {X : Ordinal }{z : OD } {x : Ordinal }→ def Z X → Z ≡ z → X ≡ x → def z x
107 def-subst df refl refl = df 107 def-subst df refl refl = df
108 108
109 sup-od : OD → ( OD → OD ) → OD 109 sup-od : ( OD → OD ) → OD
110 sup-od X ψ = Ord ( sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x ))) ) 110 sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )
111 111
112 sup-c< : {X : OD } ( ψ : OD → OD ) → ∀ {x : OD } → X ∋ x → def ( sup-od X ψ ) (od→ord ( ψ x )) 112 sup-c< : ( ψ : OD → OD ) → ∀ {x : OD } → def ( sup-od ψ ) (od→ord ( ψ x ))
113 sup-c< {X} ψ {x} lt = def-subst {_} {_} {Ord ( sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )} 113 sup-c< ψ {x} = def-subst {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )}
114 lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where 114 lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
115 lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (od→ord X) (λ x → od→ord (ψ (ord→od x))) 115 lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x)))
116 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst (sup-o< (c<→o< lt) ) refl (sym diso) ) 116 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst (sup-o< ) refl (sym diso) )
117 117
118 otrans : {n : Level} {a x y : Ordinal } → def (Ord a) x → def (Ord x) y → def (Ord a) y 118 otrans : {n : Level} {a x y : Ordinal } → def (Ord a) x → def (Ord x) y → def (Ord a) y
119 otrans x<a y<x = ordtrans y<x x<a 119 otrans x<a y<x = ordtrans y<x x<a
120 120
121 def→o< : {X : OD } → {x : Ordinal } → def X x → x o< od→ord X 121 def→o< : {X : OD } → {x : Ordinal } → def X x → x o< od→ord X
335 335
336 ZFSubset : (A x : OD ) → OD 336 ZFSubset : (A x : OD ) → OD
337 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set 337 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set
338 338
339 Def : (A : OD ) → OD 339 Def : (A : OD ) → OD
340 Def A = Ord ( sup-o (osuc (od→ord A)) ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) 340 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
341
342 341
343 _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n 342 _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n
344 _⊆_ A B {x} = A ∋ x → B ∋ x 343 _⊆_ A B {x} = A ∋ x → B ∋ x
345 344
346 infixr 220 _⊆_ 345 infixr 220 _⊆_
367 } where 366 } where
368 ZFSet = OD 367 ZFSet = OD
369 Select : (X : OD ) → ((x : OD ) → Set n ) → OD 368 Select : (X : OD ) → ((x : OD ) → Set n ) → OD
370 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } 369 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) }
371 Replace : OD → (OD → OD ) → OD 370 Replace : OD → (OD → OD ) → OD
372 Replace X ψ = record { def = λ x → (x o< sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } 371 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
373 _∩_ : ( A B : ZFSet ) → ZFSet 372 _∩_ : ( A B : ZFSet ) → ZFSet
374 A ∩ B = record { def = λ x → def A x ∧ def B x } 373 A ∩ B = record { def = λ x → def A x ∧ def B x }
375 Union : OD → OD 374 Union : OD → OD
376 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } 375 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) }
377 _∈_ : ( A B : ZFSet ) → Set n 376 _∈_ : ( A B : ZFSet ) → Set n
447 selection {ψ} {X} {y} = record { 446 selection {ψ} {X} {y} = record {
448 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } 447 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) }
449 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } 448 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso }
450 } 449 }
451 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x 450 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x
452 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} lt ; proj2 = lemma } where 451 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where
453 lemma : def (in-codomain X ψ) (od→ord (ψ x)) 452 lemma : def (in-codomain X ψ) (od→ord (ψ x))
454 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) 453 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
455 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y)) 454 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
456 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where 455 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
457 lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y)))) 456 lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
490 proj1 = def-subst {_} {_} {(Ord a)} {z} 489 proj1 = def-subst {_} {_} {(Ord a)} {z}
491 ( t→A (def-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } 490 ( t→A (def-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso }
492 lemma1 : {a : Ordinal } { t : OD } 491 lemma1 : {a : Ordinal } { t : OD }
493 → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t 492 → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
494 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) 493 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
495 lemma3 : {x : OD} → (lt : t ∋ x ) → Ord (od→ord t) ∋ x 494 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
496 lemma3 lt = c<→o< lt 495 lemma = sup-o<
497 lemma2 : ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → od→ord t o< osuc (od→ord (Ord a))
498 lemma2 t→A = lemma5 t→A where
499 lemma6 : {t s : OD } → ({x : OD} → (t ∋ x → s ∋ x)) → {x : OD} → Ord (od→ord t) ∋ x → Ord ( od→ord s) ∋ x
500 lemma6 = {!!}
501 lemma5 : {t s : OD } → ({x : OD} → (t ∋ x → s ∋ x)) → od→ord t o< osuc ( od→ord s)
502 lemma5 t→A = ⊆→o< ( λ z → lemma6 t→A )
503 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (osuc (od→ord (Ord a))) (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
504 lemma = sup-o< (lemma2 t→A)
505 496
506 -- 497 --
507 -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first 498 -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first
508 -- then replace of all elements of the Power set by A ∩ y 499 -- then replace of all elements of the Power set by A ∩ y
509 -- 500 --
536 ≡⟨ cong (λ k → A ∩ k) oiso ⟩ 527 ≡⟨ cong (λ k → A ∩ k) oiso ⟩
537 A ∩ t 528 A ∩ t
538 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩ 529 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
539 t 530 t
540 ∎ 531 ∎
541 lemma5 : od→ord t o< od→ord (Def (Ord (od→ord A))) 532 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x))
542 lemma5 = {!!} 533 lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ ord→od x)))
543 lemma1 : od→ord t o< sup-o (od→ord (Def (Ord (od→ord A)))) (λ x → od→ord (A ∩ ord→od x)) 534 lemma4 (sup-o< {λ x → od→ord (A ∩ ord→od x)} {od→ord t} )
544 lemma1 = subst (λ k → od→ord k o< sup-o (od→ord (Def (Ord (od→ord A)))) (λ x → od→ord (A ∩ ord→od x)))
545 lemma4 (sup-o< {od→ord (Def (Ord (od→ord A)))} {λ x → od→ord (A ∩ ord→od x)} {od→ord t} lemma5 )
546 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) 535 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
547 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where 536 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
548 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 537 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
549 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) 538 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A )))
550 539