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

comparison OD.agda @ 259:f714fe999102

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 05 Sep 2019 01:28:52 +0900
parents 63df67b6281c
children 8b85949bde00
comparison
equal deleted inserted replaced
258:63df67b6281c 259:f714fe999102
68 od→ord : OD → Ordinal 68 od→ord : OD → Ordinal
69 ord→od : Ordinal → OD 69 ord→od : Ordinal → OD
70 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y 70 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y
71 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x 71 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
72 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 72 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
73 -- we should prove this in agda, but simply put here
74 ==→o≡ : { x y : OD } → (x == y) → x ≡ y 73 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
75 -- 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
76 -- 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
77 -- ord→od x ≡ Ord x results the same 76 -- ord→od x ≡ Ord x results the same
78 -- supermum as Replacement Axiom 77 -- supermum as Replacement Axiom
79 sup-o : ( Ordinal → Ordinal ) → Ordinal 78 sup-o : Ordinal → ( Ordinal → Ordinal ) → Ordinal
80 sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ 79 sup-o< : {X : Ordinal} → { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → x o< X → ψ x o< sup-o X ψ
81 -- contra-position of mimimulity of supermum required in Power Set Axiom 80 -- contra-position of mimimulity of supermum required in Power Set Axiom
82 -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal 81 -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal
83 -- 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 ψ))
84 -- mimimul and x∋minimal is an Axiom of choice 83 -- mimimul and x∋minimal is an Axiom of choice
85 minimal : (x : OD ) → ¬ (x == od∅ )→ OD 84 minimal : (x : OD ) → ¬ (x == od∅ )→ OD
105 cseq x = record { def = λ y → def x (osuc y) } where 104 cseq x = record { def = λ y → def x (osuc y) } where
106 105
107 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
108 def-subst df refl refl = df 107 def-subst df refl refl = df
109 108
110 sup-od : ( OD → OD ) → OD 109 sup-od : OD → ( OD → OD ) → OD
111 sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) ) 110 sup-od X ψ = Ord ( sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x ))) )
112 111
113 sup-c< : ( ψ : OD → OD ) → ∀ {x : OD } → def ( sup-od ψ ) (od→ord ( ψ x )) 112 sup-c< : {X : OD } ( ψ : OD → OD ) → ∀ {x : OD } → X ∋ x → def ( sup-od X ψ ) (od→ord ( ψ x ))
114 sup-c< ψ {x} = def-subst {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {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 )}
115 lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where 114 lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
116 lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x))) 115 lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (od→ord X) (λ x → od→ord (ψ (ord→od x)))
117 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) ) 116 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst (sup-o< (c<→o< lt) ) refl (sym diso) )
118 117
119 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
120 otrans x<a y<x = ordtrans y<x x<a 119 otrans x<a y<x = ordtrans y<x x<a
121 120
122 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
336 335
337 ZFSubset : (A x : OD ) → OD 336 ZFSubset : (A x : OD ) → OD
338 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
339 338
340 Def : (A : OD ) → OD 339 Def : (A : OD ) → OD
341 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) 340 Def A = Ord ( sup-o (osuc (od→ord A)) ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
342 341
343 342
344 _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n 343 _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n
345 _⊆_ A B {x} = A ∋ x → B ∋ x 344 _⊆_ A B {x} = A ∋ x → B ∋ x
346 345
368 } where 367 } where
369 ZFSet = OD 368 ZFSet = OD
370 Select : (X : OD ) → ((x : OD ) → Set n ) → OD 369 Select : (X : OD ) → ((x : OD ) → Set n ) → OD
371 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } 370 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) }
372 Replace : OD → (OD → OD ) → OD 371 Replace : OD → (OD → OD ) → OD
373 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } 372 Replace X ψ = record { def = λ x → (x o< sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
374 _∩_ : ( A B : ZFSet ) → ZFSet 373 _∩_ : ( A B : ZFSet ) → ZFSet
375 A ∩ B = record { def = λ x → def A x ∧ def B x } 374 A ∩ B = record { def = λ x → def A x ∧ def B x }
376 Union : OD → OD 375 Union : OD → OD
377 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } 376 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) }
378 _∈_ : ( A B : ZFSet ) → Set n 377 _∈_ : ( A B : ZFSet ) → Set n
448 selection {ψ} {X} {y} = record { 447 selection {ψ} {X} {y} = record {
449 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } 448 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) }
450 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } 449 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso }
451 } 450 }
452 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x 451 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x
453 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where 452 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} lt ; proj2 = lemma } where
454 lemma : def (in-codomain X ψ) (od→ord (ψ x)) 453 lemma : def (in-codomain X ψ) (od→ord (ψ x))
455 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) 454 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
456 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y)) 455 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
457 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where 456 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
458 lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y)))) 457 lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
491 proj1 = def-subst {_} {_} {(Ord a)} {z} 490 proj1 = def-subst {_} {_} {(Ord a)} {z}
492 ( t→A (def-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } 491 ( t→A (def-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso }
493 lemma1 : {a : Ordinal } { t : OD } 492 lemma1 : {a : Ordinal } { t : OD }
494 → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t 493 → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
495 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) 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 ))
496 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x))) 495 lemma3 : {x : OD} → (lt : t ∋ x ) → Ord (od→ord t) ∋ x
497 lemma = sup-o< 496 lemma3 lt = c<→o< lt
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)
498 505
499 -- 506 --
500 -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first 507 -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first
501 -- then replace of all elements of the Power set by A ∩ y 508 -- then replace of all elements of the Power set by A ∩ y
502 -- 509 --
521 a = od→ord A 528 a = od→ord A
522 lemma0 : {x : OD} → t ∋ x → Ord a ∋ x 529 lemma0 : {x : OD} → t ∋ x → Ord a ∋ x
523 lemma0 {x} t∋x = c<→o< (t→A t∋x) 530 lemma0 {x} t∋x = c<→o< (t→A t∋x)
524 lemma3 : Def (Ord a) ∋ t 531 lemma3 : Def (Ord a) ∋ t
525 lemma3 = ord-power← a t lemma0 532 lemma3 = ord-power← a t lemma0
526 lt1 : od→ord (A ∩ ord→od (od→ord t)) o< sup-o (λ x → od→ord (A ∩ ord→od x))
527 lt1 = sup-o< {λ x → od→ord (A ∩ ord→od x)} {od→ord t}
528 lemma4 : (A ∩ ord→od (od→ord t)) ≡ t 533 lemma4 : (A ∩ ord→od (od→ord t)) ≡ t
529 lemma4 = let open ≡-Reasoning in begin 534 lemma4 = let open ≡-Reasoning in begin
530 A ∩ ord→od (od→ord t) 535 A ∩ ord→od (od→ord t)
531 ≡⟨ cong (λ k → A ∩ k) oiso ⟩ 536 ≡⟨ cong (λ k → A ∩ k) oiso ⟩
532 A ∩ t 537 A ∩ t
533 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩ 538 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
534 t 539 t
535 ∎ 540 ∎
536 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x)) 541 lemma5 : od→ord t o< od→ord (Def (Ord (od→ord A)))
537 lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ ord→od x))) 542 lemma5 = {!!}
538 lemma4 (sup-o< {λ x → od→ord (A ∩ ord→od x)} {od→ord t}) 543 lemma1 : od→ord t o< sup-o (od→ord (Def (Ord (od→ord A)))) (λ x → od→ord (A ∩ ord→od x))
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 )
539 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) 546 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
540 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where 547 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
541 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 548 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
542 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) 549 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A )))
543 550