Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate Ordinals.agda @ 420:53422a8ea836
bijection
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 31 Jul 2020 17:42:25 +0900 |
parents | aa306f5dab9b |
children | 9984cdd88da3 |
rev | line source |
---|---|
16 | 1 open import Level |
220
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
2 module Ordinals where |
3 | 3 |
14
e11e95d5ddee
separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
4 open import zf |
3 | 5 |
23 | 6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
75 | 7 open import Data.Empty |
14
e11e95d5ddee
separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
8 open import Relation.Binary.PropositionalEquality |
213
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
204
diff
changeset
|
9 open import logic |
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
204
diff
changeset
|
10 open import nat |
220
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
11 open import Data.Unit using ( ⊤ ) |
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
12 open import Relation.Nullary |
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
13 open import Relation.Binary |
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
14 open import Relation.Binary.Core |
3 | 15 |
414 | 16 record Oprev {n : Level} (ord : Set n) (osuc : ord → ord ) (x : ord ) : Set (suc n) where |
17 field | |
18 oprev : ord | |
19 oprev=x : osuc oprev ≡ x | |
20 | |
320 | 21 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where |
16 | 22 field |
221 | 23 Otrans : {x y z : ord } → x o< y → y o< z → x o< z |
24 OTri : Trichotomous {n} _≡_ _o<_ | |
25 ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) | |
26 <-osuc : { x : ord } → x o< osuc x | |
27 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) | |
414 | 28 Oprev-p : ( x : ord ) → Dec ( Oprev ord osuc x ) |
324 | 29 TransFinite : { ψ : ord → Set n } |
222
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
30 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) |
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
31 → ∀ (x : ord) → ψ x |
388 | 32 TransFinite1 : { ψ : ord → Set (suc n) } |
33 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) | |
34 → ∀ (x : ord) → ψ x | |
16 | 35 |
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
36 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 |
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
37 field |
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
38 x<nx : { y : ord } → (y o< next y ) |
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
39 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y |
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
40 ¬nx<nx : {x y : ord} → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z)) |
222
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
41 |
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
42 record Ordinals {n : Level} : Set (suc (suc n)) where |
220
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
43 field |
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
44 ord : Set n |
221 | 45 o∅ : ord |
46 osuc : ord → ord | |
47 _o<_ : ord → ord → Set n | |
320 | 48 next : ord → ord |
49 isOrdinal : IsOrdinals ord o∅ osuc _o<_ next | |
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
50 isNext : IsNext ord o∅ osuc _o<_ next |
17 | 51 |
221 | 52 module inOrdinal {n : Level} (O : Ordinals {n} ) where |
3 | 53 |
221 | 54 Ordinal : Set n |
55 Ordinal = Ordinals.ord O | |
56 | |
57 _o<_ : Ordinal → Ordinal → Set n | |
58 _o<_ = Ordinals._o<_ O | |
218 | 59 |
221 | 60 osuc : Ordinal → Ordinal |
61 osuc = Ordinals.osuc O | |
218 | 62 |
221 | 63 o∅ : Ordinal |
64 o∅ = Ordinals.o∅ O | |
43
0d9b9db14361
equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
65 |
320 | 66 next : Ordinal → Ordinal |
67 next = Ordinals.next O | |
68 | |
221 | 69 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O) |
70 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) | |
71 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) | |
235 | 72 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) |
388 | 73 TransFinite1 = IsOrdinals.TransFinite1 (Ordinals.isOrdinal O) |
414 | 74 Oprev-p = IsOrdinals.Oprev-p (Ordinals.isOrdinal O) |
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
75 |
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
76 x<nx = IsNext.x<nx (Ordinals.isNext O) |
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
77 osuc<nx = IsNext.osuc<nx (Ordinals.isNext O) |
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
78 ¬nx<nx = IsNext.¬nx<nx (Ordinals.isNext O) |
321 | 79 |
221 | 80 o<-dom : { x y : Ordinal } → x o< y → Ordinal |
81 o<-dom {x} _ = x | |
74
819da8c08f05
ordinal atomical successor?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
82 |
221 | 83 o<-cod : { x y : Ordinal } → x o< y → Ordinal |
84 o<-cod {_} {y} _ = y | |
147 | 85 |
221 | 86 o<-subst : {Z X z x : Ordinal } → Z o< X → Z ≡ z → X ≡ x → z o< x |
87 o<-subst df refl refl = df | |
94 | 88 |
221 | 89 ordtrans : {x y z : Ordinal } → x o< y → y o< z → x o< z |
90 ordtrans = IsOrdinals.Otrans (Ordinals.isOrdinal O) | |
94 | 91 |
221 | 92 trio< : Trichotomous _≡_ _o<_ |
93 trio< = IsOrdinals.OTri (Ordinals.isOrdinal O) | |
9
5ed16e2d8eb7
try to fix axiom of replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
94 |
221 | 95 o<¬≡ : { ox oy : Ordinal } → ox ≡ oy → ox o< oy → ⊥ |
96 o<¬≡ {ox} {oy} eq lt with trio< ox oy | |
97 o<¬≡ {ox} {oy} eq lt | tri< a ¬b ¬c = ¬b eq | |
98 o<¬≡ {ox} {oy} eq lt | tri≈ ¬a b ¬c = ¬a lt | |
99 o<¬≡ {ox} {oy} eq lt | tri> ¬a ¬b c = ¬b eq | |
23 | 100 |
221 | 101 o<> : {x y : Ordinal } → y o< x → x o< y → ⊥ |
102 o<> {ox} {oy} lt tl with trio< ox oy | |
103 o<> {ox} {oy} lt tl | tri< a ¬b ¬c = ¬c lt | |
104 o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl | |
105 o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl | |
23 | 106 |
221 | 107 osuc-< : { x y : Ordinal } → y o< osuc x → x o< y → ⊥ |
108 osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox | |
109 osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y | |
110 osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x | |
180 | 111 |
221 | 112 osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox |
113 ---- y < osuc y < x < osuc x | |
114 ---- y < osuc y = x < osuc x | |
115 ---- y < osuc y > x < osuc x -> y = x ∨ x < y → ⊥ | |
116 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox | |
117 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc | |
118 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc | |
119 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with osuc-≡< c | |
120 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox) | |
121 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox) | |
122 | |
338 | 123 osucprev : {ox oy : Ordinal } → osuc oy o< osuc ox → oy o< ox |
124 osucprev {ox} {oy} oy<ox with trio< oy ox | |
125 osucprev {ox} {oy} oy<ox | tri< a ¬b ¬c = a | |
126 osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox ) | |
127 osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox ) | |
128 | |
221 | 129 open _∧_ |
84 | 130 |
221 | 131 osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y) |
132 proj2 (osuc2 x y) lt = osucc lt | |
133 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy | |
134 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy | |
135 proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy | |
129 | 136 |
221 | 137 _o≤_ : Ordinal → Ordinal → Set n |
326 | 138 a o≤ b = a o< osuc b -- (a ≡ b) ∨ ( a o< b ) |
221 | 139 |
129 | 140 |
221 | 141 xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob |
142 xo<ab {oa} {ob} a→b with trio< oa ob | |
143 xo<ab {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc | |
144 xo<ab {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc | |
145 xo<ab {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) ) | |
88 | 146 |
221 | 147 maxα : Ordinal → Ordinal → Ordinal |
148 maxα x y with trio< x y | |
149 maxα x y | tri< a ¬b ¬c = y | |
150 maxα x y | tri> ¬a ¬b c = x | |
151 maxα x y | tri≈ ¬a refl ¬c = x | |
84 | 152 |
308 | 153 omin : Ordinal → Ordinal → Ordinal |
154 omin x y with trio< x y | |
155 omin x y | tri< a ¬b ¬c = x | |
156 omin x y | tri> ¬a ¬b c = y | |
157 omin x y | tri≈ ¬a refl ¬c = x | |
88 | 158 |
308 | 159 min1 : {x y z : Ordinal } → z o< x → z o< y → z o< omin x y |
221 | 160 min1 {x} {y} {z} z<x z<y with trio< x y |
161 min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x | |
162 min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x | |
163 min1 {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y | |
84 | 164 |
221 | 165 -- |
166 -- max ( osuc x , osuc y ) | |
167 -- | |
168 | |
169 omax : ( x y : Ordinal ) → Ordinal | |
170 omax x y with trio< x y | |
171 omax x y | tri< a ¬b ¬c = osuc y | |
172 omax x y | tri> ¬a ¬b c = osuc x | |
173 omax x y | tri≈ ¬a refl ¬c = osuc x | |
86 | 174 |
221 | 175 omax< : ( x y : Ordinal ) → x o< y → osuc y ≡ omax x y |
176 omax< x y lt with trio< x y | |
177 omax< x y lt | tri< a ¬b ¬c = refl | |
178 omax< x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt ) | |
179 omax< x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt ) | |
86 | 180 |
411 | 181 omax≤ : ( x y : Ordinal ) → x o≤ y → osuc y ≡ omax x y |
182 omax≤ x y le with trio< x y | |
183 omax≤ x y le | tri< a ¬b ¬c = refl | |
184 omax≤ x y le | tri≈ ¬a refl ¬c = refl | |
185 omax≤ x y le | tri> ¬a ¬b c with osuc-≡< le | |
186 omax≤ x y le | tri> ¬a ¬b c | case1 eq = ⊥-elim (¬b eq) | |
187 omax≤ x y le | tri> ¬a ¬b c | case2 x<y = ⊥-elim (¬a x<y) | |
188 | |
221 | 189 omax≡ : ( x y : Ordinal ) → x ≡ y → osuc y ≡ omax x y |
190 omax≡ x y eq with trio< x y | |
191 omax≡ x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq ) | |
192 omax≡ x y eq | tri≈ ¬a refl ¬c = refl | |
193 omax≡ x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq ) | |
91 | 194 |
221 | 195 omax-x : ( x y : Ordinal ) → x o< omax x y |
196 omax-x x y with trio< x y | |
197 omax-x x y | tri< a ¬b ¬c = ordtrans a <-osuc | |
198 omax-x x y | tri> ¬a ¬b c = <-osuc | |
199 omax-x x y | tri≈ ¬a refl ¬c = <-osuc | |
16 | 200 |
221 | 201 omax-y : ( x y : Ordinal ) → y o< omax x y |
202 omax-y x y with trio< x y | |
203 omax-y x y | tri< a ¬b ¬c = <-osuc | |
204 omax-y x y | tri> ¬a ¬b c = ordtrans c <-osuc | |
205 omax-y x y | tri≈ ¬a refl ¬c = <-osuc | |
206 | |
207 omxx : ( x : Ordinal ) → omax x x ≡ osuc x | |
208 omxx x with trio< x x | |
209 omxx x | tri< a ¬b ¬c = ⊥-elim (¬b refl ) | |
210 omxx x | tri> ¬a ¬b c = ⊥-elim (¬b refl ) | |
211 omxx x | tri≈ ¬a refl ¬c = refl | |
212 | |
213 omxxx : ( x : Ordinal ) → omax x (omax x x ) ≡ osuc (osuc x) | |
214 omxxx x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc )) | |
215 | |
216 open _∧_ | |
16 | 217 |
326 | 218 o≤-refl : { i j : Ordinal } → i ≡ j → i o≤ j |
219 o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc | |
221 | 220 OrdTrans : Transitive _o≤_ |
326 | 221 OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c |
222 OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc | |
223 OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc | |
224 OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc | |
225 OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b b<c) <-osuc | |
97
f2b579106770
power set using sup on Def
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
226 |
221 | 227 OrdPreorder : Preorder n n n |
228 OrdPreorder = record { Carrier = Ordinal | |
229 ; _≈_ = _≡_ | |
230 ; _∼_ = _o≤_ | |
231 ; isPreorder = record { | |
232 isEquivalence = record { refl = refl ; sym = sym ; trans = trans } | |
326 | 233 ; reflexive = o≤-refl |
221 | 234 ; trans = OrdTrans |
235 } | |
236 } | |
165 | 237 |
258 | 238 FExists : {m l : Level} → ( ψ : Ordinal → Set m ) |
221 | 239 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) |
240 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) | |
241 → ¬ p | |
258 | 242 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) |
221 | 243 |
393 | 244 nexto∅ : {x : Ordinal} → o∅ o< next x |
245 nexto∅ {x} with trio< o∅ x | |
246 nexto∅ {x} | tri< a ¬b ¬c = ordtrans a x<nx | |
247 nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx | |
248 nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) | |
249 | |
339 | 250 next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z |
251 next< {x} {y} {z} x<nz y<nx with trio< y (next z) | |
252 next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a | |
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
253 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) |
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
254 (λ 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) )))) |
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
255 next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx ) |
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
256 (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc )))) |
339 | 257 |
342 | 258 osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y |
259 osuc< {x} {y} refl = <-osuc | |
260 | |
340 | 261 nexto=n : {x y : Ordinal} → x o< next (osuc y) → x o< next y |
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
262 nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy |
340 | 263 |
341 | 264 nexto≡ : {x : Ordinal} → next x ≡ next (osuc x) |
265 nexto≡ {x} with trio< (next x) (next (osuc x) ) | |
342 | 266 -- 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 |
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
267 nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx x<nx ) a |
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
268 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq))))) |
341 | 269 nexto≡ {x} | tri≈ ¬a b ¬c = b |
342 | 270 -- 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) ... |
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
271 nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c |
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
272 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq))))) |
346 | 273 |
352 | 274 next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y) |
275 next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where | |
276 y<nx : y o< next x | |
277 y<nx = osuc< (sym eq) | |
278 | |
393 | 279 omax<next : {x y : Ordinal} → x o< y → omax x y o< next y |
280 omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx) | |
281 | |
410 | 282 x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y |
283 x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y) | |
284 x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c = -- x < y < next x < next y ∧ next x = osuc z | |
285 ⊥-elim ( ¬nx<nx y<nx a (λ z eq → o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) | |
286 x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b | |
287 x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c = -- x < y < next y < next x | |
288 ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq → o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) | |
289 | |
411 | 290 ≤next : {x y : Ordinal} → x o≤ y → next x o≤ next y |
291 ≤next {x} {y} x≤y with trio< (next x) y | |
292 ≤next {x} {y} x≤y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc ) | |
293 ≤next {x} {y} x≤y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc ) | |
294 ≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y | |
295 ≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl refl -- x = y < next x | |
296 ≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl (x<ny→≡next x<y c) -- x ≤ y < next x | |
410 | 297 |
298 x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y | |
299 x<ny→≤next {x} {y} x<ny with trio< x y | |
411 | 300 x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c = ≤next (ordtrans a <-osuc ) |
410 | 301 x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c = o≤-refl refl |
302 x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl (sym ( x<ny→≡next c x<ny )) | |
303 | |
304 omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y ) | |
305 omax<nomax {x} {y} with trio< x y | |
306 omax<nomax {x} {y} | tri< a ¬b ¬c = subst (λ k → osuc y o< k ) nexto≡ (osuc<nx x<nx ) | |
307 omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx ) | |
308 omax<nomax {x} {y} | tri> ¬a ¬b c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx ) | |
309 | |
310 omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z | |
311 omax<nx {x} {y} {z} x<nz y<nz with trio< x y | |
312 omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz | |
313 omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz | |
314 omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz | |
315 | |
420 | 316 nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny) |
317 nn<omax {x} {nx} {ny} xnx xny with trio< nx ny | |
318 nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny | |
319 nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny | |
320 nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx | |
321 | |
309 | 322 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where |
323 field | |
324 os→ : (x : Ordinal) → x o< maxordinal → Ordinal | |
325 os← : Ordinal → Ordinal | |
326 os←limit : (x : Ordinal) → os← x o< maxordinal | |
327 os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x | |
328 os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x | |
329 | |
361 | 330 module o≤-Reasoning {n : Level} (O : Ordinals {n} ) where |
331 | |
332 open inOrdinal O | |
333 | |
334 resp-o< : Ordinals._o<_ O Respects₂ _≡_ | |
335 resp-o< = resp₂ _o<_ | |
336 | |
337 trans1 : {i j k : Ordinal} → i o< j → j o< osuc k → i o< k | |
338 trans1 {i} {j} {k} i<j j<ok with osuc-≡< j<ok | |
339 trans1 {i} {j} {k} i<j j<ok | case1 refl = i<j | |
340 trans1 {i} {j} {k} i<j j<ok | case2 j<k = ordtrans i<j j<k | |
341 | |
342 trans2 : {i j k : Ordinal} → i o< osuc j → j o< k → i o< k | |
343 trans2 {i} {j} {k} i<oj j<k with osuc-≡< i<oj | |
344 trans2 {i} {j} {k} i<oj j<k | case1 refl = j<k | |
345 trans2 {i} {j} {k} i<oj j<k | case2 i<j = ordtrans i<j j<k | |
346 | |
347 open import Relation.Binary.Reasoning.Base.Triple {n} {_} {_} {_} {Ordinal } {_≡_} {_o≤_} {_o<_} | |
348 (Preorder.isPreorder OrdPreorder) | |
349 ordtrans --<-trans | |
350 (resp₂ _o<_) --(resp₂ _<_) | |
351 (λ x → ordtrans x <-osuc ) --<⇒≤ | |
352 trans1 --<-transˡ | |
353 trans2 --<-transʳ | |
354 public | |
355 hiding (_≈⟨_⟩_) | |
356 |