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

comparison Ordinals.agda @ 348:08d94fec239c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Limit ordinal and possible OD bound
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Jul 2020 07:59:17 +0900
parents cfecd05a4061
children adc3c3a37308 e27769992399
comparison
equal deleted inserted replaced
347:cfecd05a4061 348:08d94fec239c
18 Otrans : {x y z : ord } → x o< y → y o< z → x o< z 18 Otrans : {x y z : ord } → x o< y → y o< z → x o< z
19 OTri : Trichotomous {n} _≡_ _o<_ 19 OTri : Trichotomous {n} _≡_ _o<_
20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) 20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ )
21 <-osuc : { x : ord } → x o< osuc x 21 <-osuc : { x : ord } → x o< osuc x
22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) 22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
23 not-limit : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) )) 23 not-limit-p : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
24 next-limit : { y : ord } → (y o< next y ) ∧ ((x : ord) → x o< next y → osuc x o< next y ) ∧
25 ( (x : ord) → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z) ))
26 TransFinite : { ψ : ord → Set n } 24 TransFinite : { ψ : ord → Set n }
27 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) 25 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
28 → ∀ (x : ord) → ψ x 26 → ∀ (x : ord) → ψ x
29 TransFinite1 : { ψ : ord → Set (suc n) } 27 TransFinite1 : { ψ : ord → Set (suc n) }
30 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) 28 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
31 → ∀ (x : ord) → ψ x 29 → ∀ (x : ord) → ψ x
32 30
31 record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
32 field
33 x<nx : { y : ord } → (y o< next y )
34 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y
35 ¬nx<nx : {x y : ord} → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z))
33 36
34 record Ordinals {n : Level} : Set (suc (suc n)) where 37 record Ordinals {n : Level} : Set (suc (suc n)) where
35 field 38 field
36 ord : Set n 39 ord : Set n
37 o∅ : ord 40 o∅ : ord
38 osuc : ord → ord 41 osuc : ord → ord
39 _o<_ : ord → ord → Set n 42 _o<_ : ord → ord → Set n
40 next : ord → ord 43 next : ord → ord
41 isOrdinal : IsOrdinals ord o∅ osuc _o<_ next 44 isOrdinal : IsOrdinals ord o∅ osuc _o<_ next
45 isNext : IsNext ord o∅ osuc _o<_ next
42 46
43 module inOrdinal {n : Level} (O : Ordinals {n} ) where 47 module inOrdinal {n : Level} (O : Ordinals {n} ) where
44 48
45 Ordinal : Set n 49 Ordinal : Set n
46 Ordinal = Ordinals.ord O 50 Ordinal = Ordinals.ord O
60 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O) 64 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
61 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) 65 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O)
62 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) 66 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O)
63 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) 67 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)
64 TransFinite1 = IsOrdinals.TransFinite1 (Ordinals.isOrdinal O) 68 TransFinite1 = IsOrdinals.TransFinite1 (Ordinals.isOrdinal O)
65 next-limit = IsOrdinals.next-limit (Ordinals.isOrdinal O) 69
70 x<nx = IsNext.x<nx (Ordinals.isNext O)
71 osuc<nx = IsNext.osuc<nx (Ordinals.isNext O)
72 ¬nx<nx = IsNext.¬nx<nx (Ordinals.isNext O)
66 73
67 o<-dom : { x y : Ordinal } → x o< y → Ordinal 74 o<-dom : { x y : Ordinal } → x o< y → Ordinal
68 o<-dom {x} _ = x 75 o<-dom {x} _ = x
69 76
70 o<-cod : { x y : Ordinal } → x o< y → Ordinal 77 o<-cod : { x y : Ordinal } → x o< y → Ordinal
221 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 228 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
222 229
223 next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z 230 next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z
224 next< {x} {y} {z} x<nz y<nx with trio< y (next z) 231 next< {x} {y} {z} x<nz y<nx with trio< y (next z)
225 next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a 232 next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
226 next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim ((proj2 (proj2 next-limit)) (next z) x<nz (subst (λ k → k o< next x) b y<nx) 233 next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx)
227 (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (proj1 (proj2 next-limit) w (subst (λ k → w o< k ) (sym nz=ow) <-osuc) )))) 234 (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
228 next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (proj2 (proj2 next-limit) (next z) x<nz (ordtrans c y<nx ) 235 next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx )
229 (λ w nz=ow → o<¬≡ (sym nz=ow) (proj1 (proj2 next-limit) _ (subst (λ k → w o< k ) (sym nz=ow) <-osuc )))) 236 (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
230 237
231 osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y 238 osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
232 osuc< {x} {y} refl = <-osuc 239 osuc< {x} {y} refl = <-osuc
233 240
234 nexto=n : {x y : Ordinal} → x o< next (osuc y) → x o< next y 241 nexto=n : {x y : Ordinal} → x o< next (osuc y) → x o< next y
235 nexto=n {x} {y} x<noy = next< (proj1 (proj2 next-limit) _ (proj1 next-limit)) x<noy 242 nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy
236 243
237 nexto≡ : {x : Ordinal} → next x ≡ next (osuc x) 244 nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)
238 nexto≡ {x} with trio< (next x) (next (osuc x) ) 245 nexto≡ {x} with trio< (next x) (next (osuc x) )
239 -- next x o< next (osuc x ) -> osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x 246 -- next x o< next (osuc x ) -> osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
240 nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim ((proj2 (proj2 next-limit)) _ (proj1 (proj2 next-limit) _ (proj1 next-limit) ) a 247 nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx x<nx ) a
241 (λ z eq → o<¬≡ (sym eq) ((proj1 (proj2 next-limit)) _ (osuc< (sym eq))))) 248 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq)))))
242 nexto≡ {x} | tri≈ ¬a b ¬c = b 249 nexto≡ {x} | tri≈ ¬a b ¬c = b
243 -- next (osuc x) o< next x -> osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ... 250 -- next (osuc x) o< next x -> osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
244 nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim ((proj2 (proj2 next-limit)) _ (ordtrans <-osuc (proj1 next-limit)) c 251 nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
245 (λ z eq → o<¬≡ (sym eq) ((proj1 (proj2 next-limit)) _ (osuc< (sym eq))))) 252 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq)))))
246
247 record prev-choiced ( x : Ordinal ) : Set (suc n) where
248 field
249 prev : Ordinal
250 is-prev : osuc prev ≡ x
251 not-limit-p : ( x : Ordinal ) → Dec ( ¬ ((y : Ordinal) → ¬ (x ≡ osuc y) ))
252 not-limit-p x = {!!} where
253 ψ : ( ox : Ordinal ) → Set (suc n)
254 ψ ox = (( y : Ordinal ) → y o< ox → ( ¬ (osuc y ≡ x) )) ∨ prev-choiced x
255 ind : (ox : Ordinal) → ((y : Ordinal) → y o< ox → ψ y) → ψ ox
256 ind ox prev with trio< (osuc ox) x
257 ind ox prev | tri≈ ¬a b ¬c = case2 (record { prev = ox ; is-prev = b })
258 ind ox prev | tri< a ¬b ¬c = case1 (λ y y<ox oy=x → o<> (subst (λ k → k o< osuc ox) oy=x (osucc y<ox )) a )
259 -- osuc y = x < osuc ox, y < ox
260 ind ox prev | tri> ¬a ¬b c = {!!}
261 find : (y : Ordinal) → ψ y
262 find ox = TransFinite1 {ψ} ind ox
263 253
264 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where 254 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
265 field 255 field
266 os→ : (x : Ordinal) → x o< maxordinal → Ordinal 256 os→ : (x : Ordinal) → x o< maxordinal → Ordinal
267 os← : Ordinal → Ordinal 257 os← : Ordinal → Ordinal