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

comparison ordinal-definable.agda @ 90:38d139b5edac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
def ord conversion
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 05 Jun 2019 14:35:32 +0900
parents dccc9e2d1804
children b4742cf4ef97
comparison
equal deleted inserted replaced
89:dccc9e2d1804 90:38d139b5edac
31 ord→od : {n : Level} → Ordinal {n} → OD {n} 31 ord→od : {n : Level} → Ordinal {n} → OD {n}
32 32
33 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n 33 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
34 _∋_ {n} a x = def a ( od→ord x ) 34 _∋_ {n} a x = def a ( od→ord x )
35 35
36 _c<_ : { n : Level } → ( a x : OD {n} ) → Set n 36 _c<_ : { n : Level } → ( x a : OD {n} ) → Set n
37 x c< a = a ∋ x 37 x c< a = a ∋ x
38 38
39 record _==_ {n : Level} ( a b : OD {n} ) : Set n where 39 record _==_ {n : Level} ( a b : OD {n} ) : Set n where
40 field 40 field
41 eq→ : ∀ { x : Ordinal {n} } → def a x → def b x 41 eq→ : ∀ { x : Ordinal {n} } → def a x → def b x
134 lemma ox ox refl = eq-refl 134 lemma ox ox refl = eq-refl
135 135
136 o≡→== : {n : Level} → { x y : Ordinal {n} } → x ≡ y → ord→od x == ord→od y 136 o≡→== : {n : Level} → { x y : Ordinal {n} } → x ≡ y → ord→od x == ord→od y
137 o≡→== {n} {x} {.x} refl = eq-refl 137 o≡→== {n} {x} {.x} refl = eq-refl
138 138
139
139 =→¬< : {x : Nat } → ¬ ( x < x ) 140 =→¬< : {x : Nat } → ¬ ( x < x )
140 =→¬< {Zero} () 141 =→¬< {Zero} ()
141 =→¬< {Suc x} (s≤s lt) = =→¬< lt 142 =→¬< {Suc x} (s≤s lt) = =→¬< lt
142 143
143 >→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x ) 144 >→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x )
163 ==→o≡ : {n : Level} → { x y : Ordinal {suc n} } → ord→od x == ord→od y → x ≡ y 164 ==→o≡ : {n : Level} → { x y : Ordinal {suc n} } → ord→od x == ord→od y → x ≡ y
164 ==→o≡ {n} {x} {y} eq with trio< {n} x y 165 ==→o≡ {n} {x} {y} eq with trio< {n} x y
165 ==→o≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq (o<-subst a (sym ord-iso) (sym ord-iso ))) 166 ==→o≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq (o<-subst a (sym ord-iso) (sym ord-iso )))
166 ==→o≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b 167 ==→o≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
167 ==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso ))) 168 ==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso )))
169
170 ≡-def : {n : Level} → { x : Ordinal {suc n} } → x ≡ od→ord (record { def = λ z → z o< x } )
171 ≡-def {n} {x} = ==→o≡ {n} (subst (λ k → ord→od x == k ) (sym oiso) lemma ) where
172 lemma : ord→od x == record { def = λ z → z o< x }
173 eq→ lemma {w} z = subst₂ (λ k j → k o< j ) diso diso t where
174 t : (od→ord ( ord→od w)) o< (od→ord (ord→od x))
175 t = c<→o< {suc n} {ord→od w} {ord→od x} (def-subst {suc n} {_} {_} {ord→od x} {_} z refl (sym diso))
176 eq← lemma {w} z = def-subst {suc n} {_} {_} {ord→od x} {w} ( o<→c< {suc n} {_} {_} z ) refl diso
177
178 od≡-def : {n : Level} → { x : Ordinal {suc n} } → ord→od x ≡ record { def = λ z → z o< x }
179 od≡-def {n} {x} = subst (λ k → ord→od x ≡ k ) oiso (cong ( λ k → ord→od k ) (≡-def {n} {x} ))
168 180
169 ¬x<0 : {n : Level} → { x : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} ) 181 ¬x<0 : {n : Level} → { x : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
170 ¬x<0 {n} {x} (case1 ()) 182 ¬x<0 {n} {x} (case1 ())
171 ¬x<0 {n} {x} (case2 ()) 183 ¬x<0 {n} {x} (case2 ())
172 184
350 xx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) (omxx (od→ord x)) 362 xx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) (omxx (od→ord x))
351 xxx-union : {x : OD {suc n}} → (x , (x , x)) ≡ record { def = λ z → z o< osuc (osuc (od→ord x))} 363 xxx-union : {x : OD {suc n}} → (x , (x , x)) ≡ record { def = λ z → z o< osuc (osuc (od→ord x))}
352 xxx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) lemma where 364 xxx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) lemma where
353 lemma : {x : OD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x)) 365 lemma : {x : OD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x))
354 lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) {!!} ) ) ( cong ( λ k → osuc k ) {!!} ) 366 lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) {!!} ) ) ( cong ( λ k → osuc k ) {!!} )
367 uxxx-union : {x : OD {suc n}} → Union (x , (x , x)) ≡ record { def = λ z → osuc z o< osuc (osuc (od→ord x)) }
368 uxxx-union {x} = cong ( λ k → record { def = λ z → osuc z o< k } ) lemma where
369 lemma : od→ord (x , (x , x)) ≡ osuc (osuc (od→ord x))
370 lemma = {!!}
355 infinite : OD {suc n} 371 infinite : OD {suc n}
356 infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } ) 372 infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } )
357 infinity∅ : ord→od ( record { lv = Suc Zero ; ord = Φ 1 } ) ∋ od∅ {suc n} 373 infinity∅ : ord→od ( record { lv = Suc Zero ; ord = Φ 1 } ) ∋ od∅ {suc n}
358 infinity∅ = def-subst {suc n} {_} {od→ord (ord→od o∅)} {infinite} {od→ord od∅} 374 infinity∅ = def-subst {suc n} {_} {od→ord (ord→od o∅)} {infinite} {od→ord od∅}
359 (o<→c< ( case1 (s≤s z≤n ))) refl (cong (λ k → od→ord k) o∅≡od∅ ) 375 (o<→c< ( case1 (s≤s z≤n ))) refl (cong (λ k → od→ord k) o∅≡od∅ )