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

comparison ordinal-definable.agda @ 45:33860eb44e47

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
od∅' {n} = ord→od (o∅ {n}) does not work
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 25 May 2019 04:58:38 +0900
parents fcac01485f32
children e584686a1307
comparison
equal deleted inserted replaced
44:fcac01485f32 45:33860eb44e47
25 open import Data.Unit 25 open import Data.Unit
26 26
27 open Ordinal 27 open Ordinal
28 28
29 postulate 29 postulate
30 od→lv : {n : Level} → OD {n} → Nat 30 od→ord : {n : Level} → OD {n} → Ordinal {n}
31 od→d : {n : Level} → (x : OD {n}) → OrdinalD {n} (od→lv x )
32 ord→od : {n : Level} → Ordinal {n} → OD {n} 31 ord→od : {n : Level} → Ordinal {n} → OD {n}
33
34 od→ord : {n : Level} → OD {n} → Ordinal {n}
35 od→ord x = record { lv = od→lv x ; ord = od→d x }
36 32
37 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n 33 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
38 _∋_ {n} a x = def a ( od→ord x ) 34 _∋_ {n} a x = def a ( od→ord x )
39 35
40 _c<_ : { n : Level } → ( a x : OD {n} ) → Set n 36 _c<_ : { n : Level } → ( a x : OD {n} ) → Set n
65 _c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n) 61 _c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n)
66 a c≤ b = (a ≡ b) ∨ ( b ∋ a ) 62 a c≤ b = (a ≡ b) ∨ ( b ∋ a )
67 63
68 od∅ : {n : Level} → OD {n} 64 od∅ : {n : Level} → OD {n}
69 od∅ {n} = record { def = λ _ → Lift n ⊥ } 65 od∅ {n} = record { def = λ _ → Lift n ⊥ }
66
70 67
71 postulate 68 postulate
72 c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord y 69 c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord y
73 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y 70 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y
74 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x 71 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
116 lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) 113 lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x )))
117 lemma xo<z = o<→c< xo<z 114 lemma xo<z = o<→c< xo<z
118 lemma0 : def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) → def z (od→ord x) 115 lemma0 : def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) → def z (od→ord x)
119 lemma0 dz = def-subst {n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso) 116 lemma0 dz = def-subst {n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso)
120 117
118 od∅' : {n : Level} → OD {n}
119 od∅' {n} = ord→od (o∅ {n})
120
121 ∅1' : {n : Level} → ( x : OD {n} ) → ¬ ( x c< od∅' {n} )
122 ∅1' {n} x xc<o with c<→o< {n} {x} {ord→od (o∅ {n})} xc<o
123 ∅1' {n} x xc<o | case1 x₁ = {!!}
124 ∅1' {n} x xc<o | case2 x₁ = {!!}
125 where
126 lemma : ( ox : Ordinal {n} ) → ox o< o∅ {n} → ⊥
127 lemma ox (case1 ())
128 lemma ox (case2 ())
129
130
121 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where 131 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where
122 field 132 field
123 mino : Ordinal {n} 133 mino : Ordinal {n}
124 min<x : mino o< x 134 min<x : mino o< x
125 135
167 177
168 -- ∅77 : {n : Level} → (x : OD {suc n} ) → ¬ ( ord→od (o∅ {suc n}) ∋ x ) 178 -- ∅77 : {n : Level} → (x : OD {suc n} ) → ¬ ( ord→od (o∅ {suc n}) ∋ x )
169 -- ∅77 {n} x lt = {!!} where 179 -- ∅77 {n} x lt = {!!} where
170 180
171 ∅7' : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n} 181 ∅7' : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n}
172 ∅7' {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) where 182 ∅7' {n} = cong ( λ k → record { def = k }) ( ∅-base-def )
173 183
174 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl) 184 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
175 185
176
177 ∅7'' : {n : Level} → ( x : OD {n} ) → od→lv {n} x ≡ Zero → od→d {n} x ≅ Φ {n} Zero → x == od∅ {n}
178 ∅7'' {n} x eq eq1 = {!!}
179 186
180 ∅7 : {n : Level} → ( x : OD {n} ) → od→ord x ≡ o∅ {n} → x == od∅ {n} 187 ∅7 : {n : Level} → ( x : OD {n} ) → od→ord x ≡ o∅ {n} → x == od∅ {n}
181 ∅7 {n} x eq = record { eq→ = e1 ; eq← = e2 } where 188 ∅7 {n} x eq = record { eq→ = e1 ; eq← = e2 } where
182 e0 : {y : Ordinal {n}} → y o< o∅ {n} → def od∅ y 189 e0 : {y : Ordinal {n}} → y o< o∅ {n} → def od∅ y
183 e0 {y} (case1 ()) 190 e0 {y} (case1 ())
186 e1 {y} y<x with c<→o< {n} {x} y<x 193 e1 {y} y<x with c<→o< {n} {x} y<x
187 e1 {y} y<x | case1 lt = {!!} 194 e1 {y} y<x | case1 lt = {!!}
188 e1 {y} y<x | case2 lt = {!!} 195 e1 {y} y<x | case2 lt = {!!}
189 e2 : {y : Ordinal {n}} → def od∅ y → def x y 196 e2 : {y : Ordinal {n}} → def od∅ y → def x y
190 e2 {y} (lift ()) 197 e2 {y} (lift ())
198
199 open _∧_
191 200
192 ∅9 : {n : Level} → (x : OD {n} ) → ¬ x == od∅ → o∅ o< od→ord x 201 ∅9 : {n : Level} → (x : OD {n} ) → ¬ x == od∅ → o∅ o< od→ord x
193 ∅9 x not = ∅5 ( od→ord x) lemma where 202 ∅9 x not = ∅5 ( od→ord x) lemma where
194 lemma : ¬ od→ord x ≡ o∅ 203 lemma : ¬ od→ord x ≡ o∅
195 lemma eq = not ( ∅7 x eq ) 204 lemma eq = not ( ∅7 x eq )