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

comparison ordinal-definable.agda @ 40:9439ff020cbd

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, 23 May 2019 20:24:15 +0900
parents 457e6626e0b1
children b60db5903f01
comparison
equal deleted inserted replaced
39:457e6626e0b1 40:9439ff020cbd
34 _c<_ : { n : Level } → ( a x : OD {n} ) → Set n 34 _c<_ : { n : Level } → ( a x : OD {n} ) → Set n
35 x c< a = a ∋ x 35 x c< a = a ∋ x
36 36
37 _c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n) 37 _c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n)
38 a c≤ b = (a ≡ b) ∨ ( b ∋ a ) 38 a c≤ b = (a ≡ b) ∨ ( b ∋ a )
39
40 od∅ : {n : Level} → OD {n}
41 od∅ {n} = record { def = λ _ → Lift n ⊥ }
39 42
40 postulate 43 postulate
41 c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord y 44 c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord y
42 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y 45 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y
43 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x 46 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
44 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x 47 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
45 sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n} 48 sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n}
46 sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → ψ x c< sup-od ψ 49 sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → ψ x c< sup-od ψ
47 50 ∅-base-def : {n : Level} → def ( ord→od (o∅ {n}) ) ≡ def (od∅ {n})
48 HOD = OD
49
50 od∅ : {n : Level} → HOD {n}
51 od∅ {n} = record { def = λ _ → Lift n ⊥ }
52 51
53 ∅1 : {n : Level} → ( x : OD {n} ) → ¬ ( x c< od∅ {n} ) 52 ∅1 : {n : Level} → ( x : OD {n} ) → ¬ ( x c< od∅ {n} )
54 ∅1 {n} x (lift ()) 53 ∅1 {n} x (lift ())
55 54
56 ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n} 55 ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
115 ∅5 {n} record { lv = Zero ; ord = (OSuc .0 ord) } not = case2 Φ< 114 ∅5 {n} record { lv = Zero ; ord = (OSuc .0 ord) } not = case2 Φ<
116 ∅5 {n} record { lv = (Suc lv) ; ord = ord } not = case1 (s≤s z≤n) 115 ∅5 {n} record { lv = (Suc lv) ; ord = ord } not = case1 (s≤s z≤n)
117 116
118 postulate extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) 117 postulate extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
119 118
120 -- ∅7 : {n : Level} → { x : OD {n} } → ((z : OD {n}) → ¬ ( z c< x )) → x ≡ od∅
121 -- ∅7 {n} {x} not = cong ( λ k → record { def = k } ) lemma2 where
122
123 ∅6 : {n : Level } ( x : Ordinal {suc n}) → o∅ o< x → ¬ x ≡ o∅ 119 ∅6 : {n : Level } ( x : Ordinal {suc n}) → o∅ o< x → ¬ x ≡ o∅
124 ∅6 {n} x lt eq with trio< {n} (o∅ {suc n}) x 120 ∅6 {n} x lt eq with trio< {n} (o∅ {suc n}) x
125 ∅6 {n} x lt refl | tri< a ¬b ¬c = ¬b refl 121 ∅6 {n} x lt refl | tri< a ¬b ¬c = ¬b refl
126 ∅6 {n} x lt refl | tri≈ ¬a b ¬c = ¬a lt 122 ∅6 {n} x lt refl | tri≈ ¬a b ¬c = ¬a lt
127 ∅6 {n} x lt refl | tri> ¬a ¬b c = ¬b refl 123 ∅6 {n} x lt refl | tri> ¬a ¬b c = ¬b refl
128 124
129 ∅8 : {n : Level} → ( x : Ordinal {n} ) → ¬ x o< o∅ {n} 125 ∅8 : {n : Level} → ( x : Ordinal {n} ) → ¬ x o< o∅ {n}
130 ∅8 {n} x (case1 ()) 126 ∅8 {n} x (case1 ())
131 ∅8 {n} x (case2 ()) 127 ∅8 {n} x (case2 ())
132 128
133 ∅7'' : {n : Level} → o∅ {suc n} ≡ od→ord (od∅ {suc n}) 129 -- ∅10 : {n : Level} → (x : OD {n} ) → ¬ ( ( y : OD {n} ) → Lift (suc n) ( x ∋ y)) → x ≡ od∅
134 ∅7'' {n} = sym ( ∅3 lemma ) where 130 -- ∅10 {n} x not = ?
135 ⊥-leq : lift {_} {n} ⊥ ≡ lift {_} {n} ⊥
136 ⊥-leq = refl
137 lemma : {n : Level} (y : Ordinal {suc n}) → ¬ (y o< od→ord od∅)
138 lemma {n} y lt = {!!}
139 -- with ⊥-leq
140 -- ... | refl = ⊥-elim {!!} --- ∅1 (ord→od y) ( def-subst {suc n} {od∅} {y} {!!} {!!} {!!} )
141
142 ∅10 : {n : Level} → (x : OD {n} ) → ¬ ( ( y : OD {n} ) → Lift (suc n) ( x ∋ y)) → x ≡ od∅
143 ∅10 {n} x not = cong ( λ k → record { def = k }) ( extensionality {n} ( λ y → {!!} ) ) where
144 ⊥-leq : lift {_} {n} ⊥ ≡ lift {_} {n} ⊥
145 ⊥-leq = refl
146 lemma : (y : Ordinal {n} ) → def x y ≡ def od∅ y
147 lemma y with def x y | def od∅ y
148 ... | s | t = {!!}
149 131
150 open Ordinal 132 open Ordinal
151 133
152 134 ∋-subst : {n : Level} {X Y x y : OD {suc n} } → X ≡ x → Y ≡ y → X ∋ Y → x ∋ y
153 ∅77 : {n : Level} → (x : OD {suc n} ) → ¬ ( ord→od (o∅ {suc n}) ∋ x ) 135 ∋-subst refl refl x = x
154 ∅77 {n} x lt with od→ord x | c<→o< {suc n} {x} {ord→od (o∅ {suc n})} lt 136
155 ... | s | t = lemma0 s t where 137 -- ∅77 : {n : Level} → (x : OD {suc n} ) → ¬ ( ord→od (o∅ {suc n}) ∋ x )
156 lemma : ( ox : Ordinal {suc n} ) → ox o< o∅ {suc n} → ⊥ 138 -- ∅77 {n} x lt = {!!} where
157 lemma = ∅8
158 lemma1 : { y : Ordinal {suc n} } { la lA : Nat } { oa : OrdinalD {suc n} la }{ oA : OrdinalD {suc n} lA }
159 → ( record {lv = la ; ord = oa } ≡ record {lv = lA ; ord = oA } )
160 → (la < lv y ) ∨ ( oa d< ord y ) → (lA < lv y ) ∨ ( oA d< ord y )
161 lemma1 refl x = x
162 lemma0 : ( ox : Ordinal {suc n} ) → ox o< od→ord (ord→od (o∅ {suc n})) → ⊥
163 lemma0 = {!!}
164
165 -- lemma0 ox t = lemma ox ( lemma1 (diso {suc n} {o∅ {suc n}}) t )
166 --- ... | s | t = lemma s t (diso {suc n} {o∅ {suc n}}) where
167 -- with od→ord x | c<→o< {n} {x} {ord→od (o∅ {n})} lt
168 -- ∅8 {n} (od→ord x) ( def-subst {n} {ord→od (od→ord x) } {{!!}} ( c<→o< lt ) {!!} {!!} )
169 139
170 ∅7' : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n} 140 ∅7' : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n}
171 ∅7' {n} = cong ( λ k → record { def = k }) ( extensionality {n} lemma ) where 141 ∅7' {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) where
172 lemma : ( x : Ordinal {n} ) → def (ord→od o∅) x ≡ def od∅ x
173 lemma x = {!!}
174 142
175 ∅7 : {n : Level} → ( x : OD {n} ) → od→ord x ≡ o∅ {n} → x ≡ od∅ {n} 143 ∅7 : {n : Level} → ( x : OD {n} ) → od→ord x ≡ o∅ {n} → x ≡ od∅ {n}
176 ∅7 {n} x eq = trans ( trans (sym oiso)( cong ( λ k → ord→od k ) eq ) ) ∅7' 144 ∅7 {n} x eq = trans ( trans (sym oiso)( cong ( λ k → ord→od k ) eq ) ) ∅7'
177 145
178 ∅9 : {n : Level} → (x : OD {n} ) → ¬ x ≡ od∅ → o∅ o< od→ord x 146 ∅9 : {n : Level} → (x : OD {n} ) → ¬ x ≡ od∅ → o∅ o< od→ord x
179 ∅9 x not = ∅5 ( od→ord x) lemma where 147 ∅9 x not = ∅5 ( od→ord x) lemma where
180 lemma : ¬ od→ord x ≡ o∅ 148 lemma : ¬ od→ord x ≡ o∅
181 lemma eq = not ( ∅7 x eq ) 149 lemma eq = not ( ∅7 x eq )
182 150
183 HOD→ZF : {n : Level} → ZF {suc n} {suc n} 151 OD→ZF : {n : Level} → ZF {suc n} {suc n}
184 HOD→ZF {n} = record { 152 OD→ZF {n} = record {
185 ZFSet = OD {n} 153 ZFSet = OD {n}
186 ; _∋_ = λ a x → Lift (suc n) ( a ∋ x ) 154 ; _∋_ = λ a x → Lift (suc n) ( a ∋ x )
187 ; _≈_ = _≡_ 155 ; _≈_ = _≡_
188 ; ∅ = od∅ 156 ; ∅ = od∅
189 ; _,_ = _,_ 157 ; _,_ = _,_