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

comparison cardinal.agda @ 288:4fcac1eebc74 release

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
axiom of choice clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jun 2020 20:31:30 +0900
parents d9d3654baee1
children 12071f79f3cf
comparison
equal deleted inserted replaced
256:6e1c60866788 288:4fcac1eebc74
3 module cardinal {n : Level } (O : Ordinals {n}) where 3 module cardinal {n : Level } (O : Ordinals {n}) where
4 4
5 open import zf 5 open import zf
6 open import logic 6 open import logic
7 import OD 7 import OD
8 import ODC
9 import OPair
8 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) 10 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
9 open import Relation.Binary.PropositionalEquality 11 open import Relation.Binary.PropositionalEquality
10 open import Data.Nat.Properties 12 open import Data.Nat.Properties
11 open import Data.Empty 13 open import Data.Empty
12 open import Relation.Nullary 14 open import Relation.Nullary
14 open import Relation.Binary.Core 16 open import Relation.Binary.Core
15 17
16 open inOrdinal O 18 open inOrdinal O
17 open OD O 19 open OD O
18 open OD.OD 20 open OD.OD
21 open OPair O
22 open ODAxiom odAxiom
19 23
20 open _∧_ 24 open _∧_
21 open _∨_ 25 open _∨_
22 open Bool 26 open Bool
23 open _==_ 27 open _==_
24 28
25 -- we have to work on Ordinal to keep OD Level n 29 -- we have to work on Ordinal to keep OD Level n
26 -- since we use p∨¬p which works only on Level n 30 -- since we use p∨¬p which works only on Level n
27 -- < x , y > = (x , x) , (x , y)
28
29 data ord-pair : (p : Ordinal) → Set n where
30 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
31
32 ZFProduct : OD
33 ZFProduct = record { def = λ x → ord-pair x }
34
35 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
36 -- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
37 -- eq-pair refl refl = HE.refl
38
39 pi1 : { p : Ordinal } → ord-pair p → Ordinal
40 pi1 ( pair x y) = x
41
42 π1 : { p : OD } → ZFProduct ∋ p → Ordinal
43 π1 lt = pi1 lt
44
45 pi2 : { p : Ordinal } → ord-pair p → Ordinal
46 pi2 ( pair x y ) = y
47
48 π2 : { p : OD } → ZFProduct ∋ p → Ordinal
49 π2 lt = pi2 lt
50
51 p-cons : ( x y : OD ) → ZFProduct ∋ < x , y >
52 p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
53 let open ≡-Reasoning in begin
54 od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
55 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
56 od→ord < x , y >
57 ∎ )
58
59
60 p-iso1 : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >
61 p-iso1 {ox} {oy} = pair ox oy
62
63 p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
64 p-iso {x} p = ord≡→≡ (lemma p) where
65 lemma : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
66 lemma (pair ox oy) = refl
67 31
68 32
69 ∋-p : (A x : OD ) → Dec ( A ∋ x ) 33 ∋-p : (A x : OD ) → Dec ( A ∋ x )
70 ∋-p A x with p∨¬p ( A ∋ x ) 34 ∋-p A x with ODC.p∨¬p O ( A ∋ x )
71 ∋-p A x | case1 t = yes t 35 ∋-p A x | case1 t = yes t
72 ∋-p A x | case2 t = no t 36 ∋-p A x | case2 t = no t
73 37
74 _⊗_ : (A B : OD) → OD 38 _⊗_ : (A B : OD) → OD
75 A ⊗ B = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } where 39 A ⊗ B = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } where
86 Func : ( A B : OD ) → OD 50 Func : ( A B : OD ) → OD
87 Func A B = record { def = λ x → def (Power (A ⊗ B)) x } 51 Func A B = record { def = λ x → def (Power (A ⊗ B)) x }
88 52
89 -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) 53 -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
90 54
91
92 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 55 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD
93 func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > ) 56 func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > )
94 57
95 record Func←cd { dom cod : OD } {f : Ordinal } : Set n where 58 record Func←cd { dom cod : OD } {f : Ordinal } : Set n where
96 field 59 field
97 func-1 : Ordinal → Ordinal 60 func-1 : Ordinal → Ordinal
98 func→od∈Func-1 : Func dom cod ∋ func→od func-1 dom 61 func→od∈Func-1 : Func dom cod ∋ func→od func-1 dom
99 62
100 od→func : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → Func←cd {dom} {cod} {f} 63 od→func : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → Func←cd {dom} {cod} {f}
101 od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where 64 od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x {!!} ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where
102 lemma : Ordinal → Ordinal → Ordinal 65 lemma : Ordinal → Ordinal → Ordinal
103 lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y) 66 lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
104 lemma x y | p | no n = o∅ 67 lemma x y | p | no n = o∅
105 lemma x y | p | yes f∋y = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) 68 lemma x y | p | yes f∋y = lemma2 (proj1 (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y)
106 lemma2 : {p : Ordinal} → ord-pair p → Ordinal 69 lemma2 : {p : Ordinal} → ord-pair p → Ordinal
107 lemma2 (pair x1 y1) with decp ( x1 ≡ x) 70 lemma2 (pair x1 y1) with ODC.decp O ( x1 ≡ x)
108 lemma2 (pair x1 y1) | yes p = y1 71 lemma2 (pair x1 y1) | yes p = y1
109 lemma2 (pair x1 y1) | no ¬p = o∅ 72 lemma2 (pair x1 y1) | no ¬p = o∅
110 fod : OD 73 fod : OD
111 fod = Replace dom ( λ x → < x , ord→od (sup-o ( λ y → lemma (od→ord x) y )) > ) 74 fod = Replace dom ( λ x → < x , ord→od (sup-o ( λ y → lemma (od→ord x) {!!} )) > )
112 75
113 76
114 open Func←cd 77 open Func←cd
115 78
116 -- contra position of sup-o< 79 -- contra position of sup-o<
137 onto-iso : {y : Ordinal } → (lty : def Y y ) → 100 onto-iso : {y : Ordinal } → (lty : def Y y ) →
138 func-1 ( od→func {X} {Y} {xmap} xfunc ) ( func-1 (od→func yfunc) y ) ≡ y 101 func-1 ( od→func {X} {Y} {xmap} xfunc ) ( func-1 (od→func yfunc) y ) ≡ y
139 102
140 open Onto 103 open Onto
141 104
142 onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z 105 onto-restrict : {X Y Z : OD} → Onto X Y → Z ⊆ Y → Onto X Z
143 onto-restrict {X} {Y} {Z} onto Z⊆Y = record { 106 onto-restrict {X} {Y} {Z} onto Z⊆Y = record {
144 xmap = xmap1 107 xmap = xmap1
145 ; ymap = zmap 108 ; ymap = zmap
146 ; xfunc = xfunc1 109 ; xfunc = xfunc1
147 ; yfunc = zfunc 110 ; yfunc = zfunc
165 conto : Onto X (Ord cardinal) 128 conto : Onto X (Ord cardinal)
166 cmax : ( y : Ordinal ) → cardinal o< y → ¬ Onto X (Ord y) 129 cmax : ( y : Ordinal ) → cardinal o< y → ¬ Onto X (Ord y)
167 130
168 cardinal : (X : OD ) → Cardinal X 131 cardinal : (X : OD ) → Cardinal X
169 cardinal X = record { 132 cardinal X = record {
170 cardinal = sup-o ( λ x → proj1 ( cardinal-p x) ) 133 cardinal = sup-o ( λ x → proj1 ( cardinal-p {!!}) )
171 ; conto = onto 134 ; conto = onto
172 ; cmax = cmax 135 ; cmax = cmax
173 } where 136 } where
174 cardinal-p : (x : Ordinal ) → ( Ordinal ∧ Dec (Onto X (Ord x) ) ) 137 cardinal-p : (x : Ordinal ) → ( Ordinal ∧ Dec (Onto X (Ord x) ) )
175 cardinal-p x with p∨¬p ( Onto X (Ord x) ) 138 cardinal-p x with ODC.p∨¬p O ( Onto X (Ord x) )
176 cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True } 139 cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True }
177 cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False } 140 cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
178 S = sup-o (λ x → proj1 (cardinal-p x)) 141 S = sup-o (λ x → proj1 (cardinal-p {!!}))
179 lemma1 : (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc S) → Onto X (Ord y))) → 142 lemma1 : (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc S) → Onto X (Ord y))) →
180 Lift (suc n) (x o< (osuc S) → Onto X (Ord x) ) 143 Lift (suc n) (x o< (osuc S) → Onto X (Ord x) )
181 lemma1 x prev with trio< x (osuc S) 144 lemma1 x prev with trio< x (osuc S)
182 lemma1 x prev | tri< a ¬b ¬c with osuc-≡< a 145 lemma1 x prev | tri< a ¬b ¬c with osuc-≡< a
183 lemma1 x prev | tri< a ¬b ¬c | case1 x=S = lift ( λ lt → {!!} ) 146 lemma1 x prev | tri< a ¬b ¬c | case1 x=S = lift ( λ lt → {!!} )
190 onto : Onto X (Ord S) 153 onto : Onto X (Ord S)
191 onto with TransFinite {λ x → Lift (suc n) ( x o< osuc S → Onto X (Ord x) ) } lemma1 S 154 onto with TransFinite {λ x → Lift (suc n) ( x o< osuc S → Onto X (Ord x) ) } lemma1 S
192 ... | lift t = t <-osuc 155 ... | lift t = t <-osuc
193 cmax : (y : Ordinal) → S o< y → ¬ Onto X (Ord y) 156 cmax : (y : Ordinal) → S o< y → ¬ Onto X (Ord y)
194 cmax y lt ontoy = o<> lt (o<-subst {_} {_} {y} {S} 157 cmax y lt ontoy = o<> lt (o<-subst {_} {_} {y} {S}
195 (sup-o< {λ x → proj1 ( cardinal-p x)}{y} ) lemma refl ) where 158 (sup-o< {λ x → proj1 ( cardinal-p {!!})}{{!!}} ) lemma refl ) where
196 lemma : proj1 (cardinal-p y) ≡ y 159 lemma : proj1 (cardinal-p y) ≡ y
197 lemma with p∨¬p ( Onto X (Ord y) ) 160 lemma with ODC.p∨¬p O ( Onto X (Ord y) )
198 lemma | case1 x = refl 161 lemma | case1 x = refl
199 lemma | case2 not = ⊥-elim ( not ontoy ) 162 lemma | case2 not = ⊥-elim ( not ontoy )
200 163
201 164
202 ----- 165 -----