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

comparison OD.agda @ 271:2169d948159b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix incl
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Dec 2019 23:45:59 +0900
parents 53744836020b
children 985a1af11bce
comparison
equal deleted inserted replaced
270:fc3d4bc1dc5e 271:2169d948159b
34 eq← : ∀ { x : Ordinal } → def b x → def a x 34 eq← : ∀ { x : Ordinal } → def b x → def a x
35 35
36 id : {A : Set n} → A → A 36 id : {A : Set n} → A → A
37 id x = x 37 id x = x
38 38
39 eq-refl : { x : OD } → x == x 39 ==-refl : { x : OD } → x == x
40 eq-refl {x} = record { eq→ = id ; eq← = id } 40 ==-refl {x} = record { eq→ = id ; eq← = id }
41 41
42 open _==_ 42 open _==_
43 43
44 eq-sym : { x y : OD } → x == y → y == x 44 ==-trans : { x y z : OD } → x == y → y == z → x == z
45 eq-sym eq = record { eq→ = eq← eq ; eq← = eq→ eq } 45 ==-trans x=y y=z = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← = λ {m} t → eq← x=y (eq← y=z t) }
46 46
47 eq-trans : { x y z : OD } → x == y → y == z → x == z 47 ==-sym : { x y : OD } → x == y → y == x
48 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) } 48 ==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t }
49
49 50
50 ⇔→== : { x y : OD } → ( {z : Ordinal } → def x z ⇔ def y z) → x == y 51 ⇔→== : { x y : OD } → ( {z : Ordinal } → def x z ⇔ def y z) → x == y
51 eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m 52 eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m
52 eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m 53 eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m
53 54
72 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 73 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
73 ==→o≡ : { x y : OD } → (x == y) → x ≡ y 74 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
74 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD 75 -- 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 76 -- o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x
76 -- ord→od x ≡ Ord x results the same 77 -- ord→od x ≡ Ord x results the same
77 -- supermum as Replacement Axiom 78 -- supermum as Replacement Axiom ( this assumes Ordinal has some upper bound )
78 sup-o : ( Ordinal → Ordinal ) → Ordinal 79 sup-o : ( Ordinal → Ordinal ) → Ordinal
79 sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ 80 sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ
80 -- contra-position of mimimulity of supermum required in Power Set Axiom 81 -- contra-position of mimimulity of supermum required in Power Set Axiom
81 -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal 82 -- 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 ψ)) 83 -- sup-lb : {n : Level } → { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
138 =-iso {_} {y} = cong ( λ k → k == y ) (sym oiso) 139 =-iso {_} {y} = cong ( λ k → k == y ) (sym oiso)
139 140
140 ord→== : { x y : OD } → od→ord x ≡ od→ord y → x == y 141 ord→== : { x y : OD } → od→ord x ≡ od→ord y → x == y
141 ord→== {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where 142 ord→== {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where
142 lemma : ( ox oy : Ordinal ) → ox ≡ oy → (ord→od ox) == (ord→od oy) 143 lemma : ( ox oy : Ordinal ) → ox ≡ oy → (ord→od ox) == (ord→od oy)
143 lemma ox ox refl = eq-refl 144 lemma ox ox refl = ==-refl
144 145
145 o≡→== : { x y : Ordinal } → x ≡ y → ord→od x == ord→od y 146 o≡→== : { x y : Ordinal } → x ≡ y → ord→od x == ord→od y
146 o≡→== {x} {.x} refl = eq-refl 147 o≡→== {x} {.x} refl = ==-refl
147 148
148 o∅≡od∅ : ord→od (o∅ ) ≡ od∅ 149 o∅≡od∅ : ord→od (o∅ ) ≡ od∅
149 o∅≡od∅ = ==→o≡ lemma where 150 o∅≡od∅ = ==→o≡ lemma where
150 lemma0 : {x : Ordinal} → def (ord→od o∅) x → def od∅ x 151 lemma0 : {x : Ordinal} → def (ord→od o∅) x → def od∅ x
151 lemma0 {x} lt = o<-subst (c<→o< {ord→od x} {ord→od o∅} (def-subst {ord→od o∅} {x} lt refl (sym diso)) ) diso diso 152 lemma0 {x} lt = o<-subst (c<→o< {ord→od x} {ord→od o∅} (def-subst {ord→od o∅} {x} lt refl (sym diso)) ) diso diso
160 ∅0 : record { def = λ x → Lift n ⊥ } == od∅ 161 ∅0 : record { def = λ x → Lift n ⊥ } == od∅
161 eq→ ∅0 {w} (lift ()) 162 eq→ ∅0 {w} (lift ())
162 eq← ∅0 {w} lt = lift (¬x<0 lt) 163 eq← ∅0 {w} lt = lift (¬x<0 lt)
163 164
164 ∅< : { x y : OD } → def x (od→ord y ) → ¬ ( x == od∅ ) 165 ∅< : { x y : OD } → def x (od→ord y ) → ¬ ( x == od∅ )
165 ∅< {x} {y} d eq with eq→ (eq-trans eq (eq-sym ∅0) ) d 166 ∅< {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d
166 ∅< {x} {y} d eq | lift () 167 ∅< {x} {y} d eq | lift ()
167 168
168 ∅6 : { x : OD } → ¬ ( x ∋ x ) -- no Russel paradox 169 ∅6 : { x : OD } → ¬ ( x ∋ x ) -- no Russel paradox
169 ∅6 {x} x∋x = o<¬≡ refl ( c<→o< {x} {x} x∋x ) 170 ∅6 {x} x∋x = o<¬≡ refl ( c<→o< {x} {x} x∋x )
170 171
188 left (case1 t) = case2 t 189 left (case1 t) = case2 t
189 left (case2 t) = case1 t 190 left (case2 t) = case1 t
190 right : {z : Ordinal} → def (y , x) z → def (x , y) z 191 right : {z : Ordinal} → def (y , x) z → def (x , y) z
191 right (case1 t) = case2 t 192 right (case1 t) = case2 t
192 right (case2 t) = case1 t 193 right (case2 t) = case1 t
193
194 ==-trans : { x y z : OD } → x == y → y == z → x == z
195 ==-trans x=y y=z = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← = λ {m} t → eq← x=y (eq← y=z t) }
196
197 ==-sym : { x y : OD } → x == y → y == x
198 ==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t }
199 194
200 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y 195 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
201 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq ) 196 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )
202 197
203 od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y 198 od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y
337 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set 332 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set
338 333
339 Def : (A : OD ) → OD 334 Def : (A : OD ) → OD
340 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) 335 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
341 336
342 _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n 337 -- _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n
343 _⊆_ A B {x} = A ∋ x → B ∋ x 338 -- _⊆_ A B {x} = A ∋ x → B ∋ x
339
340 record _⊆_ ( A B : OD ) : Set (suc n) where
341 field
342 incl : { x : OD } → A ∋ x → B ∋ x
343
344 open _⊆_
344 345
345 infixr 220 _⊆_ 346 infixr 220 _⊆_
346 347
347 subset-lemma : {A x y : OD } → ( x ∋ y → ZFSubset A x ∋ y ) ⇔ ( _⊆_ x A {y} ) 348 subset-lemma : {A x : OD } → ( {y : OD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A )
348 subset-lemma {A} {x} {y} = record { 349 subset-lemma {A} {x} = record {
349 proj1 = λ z lt → proj1 (z lt) 350 proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) }
350 ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt } 351 ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt }
351 } 352 }
352 353
353 open import Data.Unit 354 open import Data.Unit
354 355
355 ε-induction : { ψ : OD → Set (suc n)} 356 ε-induction : { ψ : OD → Set (suc n)}
404 405
405 infixr 200 _∈_ 406 infixr 200 _∈_
406 -- infixr 230 _∩_ _∪_ 407 -- infixr 230 _∩_ _∪_
407 isZF : IsZF (OD ) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite 408 isZF : IsZF (OD ) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite
408 isZF = record { 409 isZF = record {
409 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } 410 isEquivalence = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans }
410 ; pair→ = pair→ 411 ; pair→ = pair→
411 ; pair← = pair← 412 ; pair← = pair←
412 ; union→ = union→ 413 ; union→ = union→
413 ; union← = union← 414 ; union← = union←
414 ; empty = empty 415 ; empty = empty
434 pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y)) 435 pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y))
435 436
436 empty : (x : OD ) → ¬ (od∅ ∋ x) 437 empty : (x : OD ) → ¬ (od∅ ∋ x)
437 empty x = ¬x<0 438 empty x = ¬x<0
438 439
439 o<→c< : {x y : Ordinal } {z : OD }→ x o< y → _⊆_ (Ord x) (Ord y) {z} 440 o<→c< : {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y)
440 o<→c< lt lt1 = ordtrans lt1 lt 441 o<→c< lt = record { incl = λ z → ordtrans z lt }
441 442
442 ⊆→o< : {x y : Ordinal } → (∀ (z : OD) → _⊆_ (Ord x) (Ord y) {z} ) → x o< osuc y 443 ⊆→o< : {x y : Ordinal } → (Ord x) ⊆ (Ord y) → x o< osuc y
443 ⊆→o< {x} {y} lt with trio< x y 444 ⊆→o< {x} {y} lt with trio< x y
444 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc 445 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc
445 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc 446 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
446 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl ) 447 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym diso) refl )
447 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) 448 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
448 449
449 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 450 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
450 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx 451 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
451 ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) 452 ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
549 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) 550 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
550 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where 551 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
551 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 552 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
552 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) 553 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A )))
553 554
554 ord⊆power : (a : Ordinal) → (x : OD) → _⊆_ (Ord (osuc a)) (Power (Ord a)) {x} 555 ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a))
555 ord⊆power a x lt = power← (Ord a) x lemma where 556 ord⊆power a = record { incl = λ {x} lt → power← (Ord a) x (lemma lt) } where
556 lemma : {y : OD} → x ∋ y → Ord a ∋ y 557 lemma : {x y : OD} → od→ord x o< osuc a → x ∋ y → Ord a ∋ y
557 lemma y<x with osuc-≡< lt 558 lemma lt y<x with osuc-≡< lt
558 lemma y<x | case1 refl = c<→o< y<x 559 lemma lt y<x | case1 refl = c<→o< y<x
559 lemma y<x | case2 x<a = ordtrans (c<→o< y<x) x<a 560 lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a
560 561
561 -- continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_ (Power (Ord a)) (Ord (osuc a)) {x} 562 -- continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
562 -- continuum-hyphotheis a x = ? 563 -- continuum-hyphotheis a = ?
563 564
564 -- assuming axiom of choice 565 -- assuming axiom of choice
565 regularity : (x : OD) (not : ¬ (x == od∅)) → 566 regularity : (x : OD) (not : ¬ (x == od∅)) →
566 (x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) 567 (x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
567 proj1 (regularity x not ) = x∋minimal x not 568 proj1 (regularity x not ) = x∋minimal x not
618 ψ : ( ox : Ordinal ) → Set (suc n) 619 ψ : ( ox : Ordinal ) → Set (suc n)
619 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X 620 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X
620 lemma-ord : ( ox : Ordinal ) → ψ ox 621 lemma-ord : ( ox : Ordinal ) → ψ ox
621 lemma-ord ox = TransFinite {ψ} induction ox where 622 lemma-ord ox = TransFinite {ψ} induction ox where
622 ∋-p : (A x : OD ) → Dec ( A ∋ x ) 623 ∋-p : (A x : OD ) → Dec ( A ∋ x )
623 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) 624 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
624 ∋-p A x | case1 (lift t) = yes t 625 ∋-p A x | case1 (lift t) = yes t
625 ∋-p A x | case2 t = no (λ x → t (lift x )) 626 ∋-p A x | case2 t = no (λ x → t (lift x ))
626 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } 627 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) }
627 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B 628 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B
628 ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) 629 ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM
629 ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t 630 ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t
630 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where 631 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where
631 lemma : ¬ ((x : Ordinal ) → A x) → B 632 lemma : ¬ ((x : Ordinal ) → A x) → B
632 lemma not with p∨¬p B 633 lemma not with p∨¬p B
633 lemma not | case1 b = b 634 lemma not | case1 b = b
641 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) 642 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
642 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) ) 643 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) )
643 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X 644 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
644 lemma = ∀-imply-or lemma1 645 lemma = ∀-imply-or lemma1
645 have_to_find : choiced X 646 have_to_find : choiced X
646 have_to_find with lemma-ord (od→ord X ) 647 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where
647 have_to_find | t = dont-or t ¬¬X∋x where
648 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) 648 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
649 ¬¬X∋x nn = not record { 649 ¬¬X∋x nn = not record {
650 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) 650 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
651 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) 651 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
652 } 652 }