Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ordinal.agda @ 85:7494ae6b83c6
omax-induction does not work
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 05 Jun 2019 02:58:17 +0900 |
| parents | 4b2aff372b7c |
| children | 08be6351927e |
comparison
equal
deleted
inserted
replaced
| 84:4b2aff372b7c | 85:7494ae6b83c6 |
|---|---|
| 197 maxα x y with <-cmp (lv x) (lv y) | 197 maxα x y with <-cmp (lv x) (lv y) |
| 198 maxα x y | tri< a ¬b ¬c = x | 198 maxα x y | tri< a ¬b ¬c = x |
| 199 maxα x y | tri> ¬a ¬b c = y | 199 maxα x y | tri> ¬a ¬b c = y |
| 200 maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) } | 200 maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) } |
| 201 | 201 |
| 202 -- | |
| 203 -- max ( osuc x , osuc y ) | |
| 204 -- | |
| 202 omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n} | 205 omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n} |
| 203 omax {n} x y with <-cmp (lv x) (lv y) | 206 omax {n} x y with <-cmp (lv x) (lv y) |
| 204 omax {n} x y | tri< a ¬b ¬c = osuc y | 207 omax {n} x y | tri< a ¬b ¬c = osuc y |
| 205 omax {n} x y | tri> ¬a ¬b c = osuc x | 208 omax {n} x y | tri> ¬a ¬b c = osuc x |
| 206 omax {n} x y | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y) | 209 omax {n} x y | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y) |
| 207 omax {n} x y | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = osuc y | 210 omax {n} x y | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = osuc y |
| 208 omax {n} x y | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = osuc x | 211 omax {n} x y | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = osuc x |
| 209 omax {n} x y | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = osuc x | 212 omax {n} x y | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = osuc x |
| 213 | |
| 214 omax-induction : {n : Level} ( x y : Ordinal {suc n} ) → { ψ : ( m : Ordinal {suc n} ) → m ≡ omax x y → Set (suc n) } | |
| 215 → ( lv x < lv y → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq ) | |
| 216 → ( lv y < lv x → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq ) | |
| 217 → ( lv y ≡ lv x → ord x ≅ ord y → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq ) | |
| 218 → ( lv y ≡ lv x → ord x d< ord y → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq ) | |
| 219 → ( lv y ≡ lv x → ord y d< ord x → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq ) | |
| 220 → ψ ( omax x y ) refl | |
| 221 omax-induction {n} x y c1 c2 c3 c4 c5 with <-cmp (lv x) (lv y) | |
| 222 omax-induction {n} x y c1 c2 c3 c4 c5 | tri< a ¬b ¬c = c1 a (osuc y) refl | |
| 223 omax-induction {n} x y c1 c2 c3 c4 c5 | tri> ¬a ¬b c = c2 c (osuc x) refl | |
| 224 omax-induction {n} x y c1 c2 c3 c4 c5 | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y) | |
| 225 omax-induction {n} x y c1 c2 c3 c4 c5 | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = c4 refl a (osuc y) refl | |
| 226 omax-induction {n} x y c1 c2 c3 c4 c5 | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = c3 refl refl (osuc x) refl | |
| 227 omax-induction {n} x y c1 c2 c3 c4 c5 | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = c5 refl c (osuc x) refl | |
| 210 | 228 |
| 211 omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y | 229 omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y |
| 212 omax< {n} x y lt with <-cmp (lv x) (lv y) | 230 omax< {n} x y lt with <-cmp (lv x) (lv y) |
| 213 omax< {n} x y lt | tri< a ¬b ¬c = refl | 231 omax< {n} x y lt | tri< a ¬b ¬c = refl |
| 214 omax< {n} x y (case1 lt) | tri> ¬a ¬b c = ⊥-elim (¬a lt) | 232 omax< {n} x y (case1 lt) | tri> ¬a ¬b c = ⊥-elim (¬a lt) |
| 218 omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = refl | 236 omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = refl |
| 219 omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( trio<≡ b lt ) | 237 omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( trio<≡ b lt ) |
| 220 omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim ( o<> (case2 lt) (case2 c) ) | 238 omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim ( o<> (case2 lt) (case2 c) ) |
| 221 | 239 |
| 222 omaxx : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y | 240 omaxx : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y |
| 223 omaxx {n} x y with trio< x y | 241 omaxx {n} x y = omax-induction {n} x y {λ om refl → x o< om } |
| 224 omaxx {n} x y | tri< a ¬b ¬c = {!!} | 242 ( λ lx<ly omax refl → ordtrans (case1 lx<ly) <-osuc ) |
| 225 omaxx {n} x y | tri> ¬a ¬b c = {!!} | 243 ( λ lx>ly omax → {!!} ) -- ordtrans (case1 lx>ly) <-osuc ) |
| 226 omaxx {n} x y | tri≈ ¬a b ¬c = {!!} | 244 ( λ refl refl omax refl → {!!} ) -- <-osuc ) |
| 245 ( λ refl ox<oy omax → {!!} ) -- ordtrans (case2 ox<oy) <-osuc ) | |
| 246 ( λ refl ox>oy omax → {!!} ) -- ordtrans (case2 ox>oy) <-osuc ) | |
| 227 | 247 |
| 228 OrdTrans : {n : Level} → Transitive {suc n} _o≤_ | 248 OrdTrans : {n : Level} → Transitive {suc n} _o≤_ |
| 229 OrdTrans (case1 refl) (case1 refl) = case1 refl | 249 OrdTrans (case1 refl) (case1 refl) = case1 refl |
| 230 OrdTrans (case1 refl) (case2 lt2) = case2 lt2 | 250 OrdTrans (case1 refl) (case2 lt2) = case2 lt2 |
| 231 OrdTrans (case2 lt1) (case1 refl) = case2 lt1 | 251 OrdTrans (case2 lt1) (case1 refl) = case2 lt1 |