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

comparison ordinal-definable.agda @ 80:461690d60d07

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove ∅-base-def
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Jun 2019 12:29:33 +0900
parents c07c548b2ac1
children 96c932d0145d
comparison
equal deleted inserted replaced
79:c07c548b2ac1 80:461690d60d07
66 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y 66 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y
67 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x 67 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
68 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x 68 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
69 sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n} 69 sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n}
70 sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → ψ x c< sup-od ψ 70 sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → ψ x c< sup-od ψ
71 ∅-base-def : {n : Level} → def ( ord→od (o∅ {n}) ) ≡ def (od∅ {n})
72
73 congf : {n : Level} {x y : OD {n}} → { f g : OD {n} → OD {n} } → x ≡ y → f ≡ g → f x ≡ g y
74 congf refl refl = refl
75
76 o∅→od∅ : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n}
77 o∅→od∅ {n} = cong ( λ k → record { def = k }) ( ∅-base-def )
78 71
79 ∅1 : {n : Level} → ( x : OD {n} ) → ¬ ( x c< od∅ {n} ) 72 ∅1 : {n : Level} → ( x : OD {n} ) → ¬ ( x c< od∅ {n} )
80 ∅1 {n} x (lift ()) 73 ∅1 {n} x (lift ())
81 74
82 ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n} 75 ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
187 ==→o≡ {n} {x} {y} eq with trio< {n} x y 180 ==→o≡ {n} {x} {y} eq with trio< {n} x y
188 ==→o≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq (o<-subst a (sym ord-iso) (sym ord-iso ))) 181 ==→o≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq (o<-subst a (sym ord-iso) (sym ord-iso )))
189 ==→o≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b 182 ==→o≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
190 ==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso ))) 183 ==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso )))
191 184
185 ¬x<0 : {n : Level} → { x : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
186 ¬x<0 {n} {x} (case1 ())
187 ¬x<0 {n} {x} (case2 ())
188
189 -- o∅≡od∅0 : {n : Level} → ord→od (o∅ {suc n}) == od∅ {suc n}
190 -- eq→ (o∅≡od∅0 {n} ) {x} y with c<→o< {suc n} {ord→od x} {ord→od (o∅ {suc n})} (def-subst {suc n} {_} {_} {ord→od o∅} {od→ord (ord→od x)} y refl (sym diso) )
191 -- eq→ (o∅≡od∅0 {n}) {x} y | lt = ⊥-elim ( ¬x<0 (o<-subst lt ord-iso diso ) )
192 -- eq← (o∅≡od∅0 {n}) {x} (lift ())
193 --
194 -- o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
195 -- o∅≡od∅ {n} = trans (cong (λ k → ord→od k ) ( ==→o≡ {n} (eq-trans o∅≡od∅0 (subst (λ k → od∅ == k ) (sym oiso) eq-refl )) ) ) oiso
196
197 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
198 o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} ))
199 o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
200 lemma : o∅ {suc n } o< (od→ord (od∅ {suc n} )) → ⊥
201 lemma lt with def-subst (o<→c< lt) oiso refl
202 lemma lt | lift ()
203 o∅≡od∅ {n} | tri≈ ¬a b ¬c = trans (cong (λ k → ord→od k ) b ) oiso
204 o∅≡od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
205
192 o<→¬== : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (x == y ) 206 o<→¬== : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (x == y )
193 o<→¬== {n} {x} {y} lt eq = o<→o> eq lt 207 o<→¬== {n} {x} {y} lt eq = o<→o> eq lt
194 208
195 o<→¬c> : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (y c< x ) 209 o<→¬c> : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (y c< x )
196 o<→¬c> {n} {x} {y} olt clt = o<> (od→ord x) (od→ord y) olt (c<→o< clt ) where 210 o<→¬c> {n} {x} {y} olt clt = o<> (od→ord x) (od→ord y) olt (c<→o< clt ) where
237 ¬∅=→∅∈ {n} {x} ne = def-subst (lemma (od→ord x) (subst (λ k → ¬ (k == od∅ {suc n} )) (sym oiso) ne )) oiso refl where 251 ¬∅=→∅∈ {n} {x} ne = def-subst (lemma (od→ord x) (subst (λ k → ¬ (k == od∅ {suc n} )) (sym oiso) ne )) oiso refl where
238 lemma : (ox : Ordinal {suc n}) → ¬ (ord→od ox == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n} 252 lemma : (ox : Ordinal {suc n}) → ¬ (ord→od ox == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n}
239 lemma ox ne with is-o∅ ox 253 lemma ox ne with is-o∅ ox
240 lemma ox ne | yes refl with ne ( ord→== lemma1 ) where 254 lemma ox ne | yes refl with ne ( ord→== lemma1 ) where
241 lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅ 255 lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅
242 lemma1 = cong ( λ k → od→ord k ) o∅→od∅ 256 lemma1 = cong ( λ k → od→ord k ) o∅≡od∅
243 lemma o∅ ne | yes refl | () 257 lemma o∅ ne | yes refl | ()
244 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p)) 258 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅≡od∅ (o<→c< (∅5 ¬p))
245 259
246 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 260 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
247 261
248 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} 262 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
249 OD→ZF {n} = record { 263 OD→ZF {n} = record {
358 eq← (next x ) {y} z = {!!} 372 eq← (next x ) {y} z = {!!}
359 infinite : OD {suc n} 373 infinite : OD {suc n}
360 infinite = ord→od ( record { lv = Suc Zero ; ord = ℵ Zero } ) 374 infinite = ord→od ( record { lv = Suc Zero ; ord = ℵ Zero } )
361 infinity∅ : ord→od ( record { lv = Suc Zero ; ord = ℵ Zero } ) ∋ od∅ {suc n} 375 infinity∅ : ord→od ( record { lv = Suc Zero ; ord = ℵ Zero } ) ∋ od∅ {suc n}
362 infinity∅ = def-subst {suc n} {_} {od→ord (ord→od o∅)} {infinite} {od→ord od∅} 376 infinity∅ = def-subst {suc n} {_} {od→ord (ord→od o∅)} {infinite} {od→ord od∅}
363 (o<→c< ( case1 (s≤s z≤n ))) refl (cong (λ k → od→ord k) o∅→od∅ ) 377 (o<→c< ( case1 (s≤s z≤n ))) refl (cong (λ k → od→ord k) o∅≡od∅ )
364 infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x )) 378 infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
365 infinity x ∞∋x = {!!} 379 infinity x ∞∋x = {!!}
366 replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x 380 replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x
367 replacement {ψ} X x = {!!} 381 replacement {ψ} X x = {!!}
368 382