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