Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ordinal.agda @ 73:dd430a95610f
fix ordinal
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 01 Jun 2019 18:17:24 +0900 |
parents | f39f1a90d154 |
children | 819da8c08f05 |
comparison
equal
deleted
inserted
replaced
72:f39f1a90d154 | 73:dd430a95610f |
---|---|
40 | 40 |
41 o<-subst : {n : Level } {Z X z x : Ordinal {n}} → Z o< X → Z ≡ z → X ≡ x → z o< x | 41 o<-subst : {n : Level } {Z X z x : Ordinal {n}} → Z o< X → Z ≡ z → X ≡ x → z o< x |
42 o<-subst df refl refl = df | 42 o<-subst df refl refl = df |
43 | 43 |
44 osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n} | 44 osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n} |
45 osuc record { lv = lx ; ord = (Φ lv) } = record { lv = lx ; ord = OSuc lx (Φ lv) } | 45 osuc record { lv = 0 ; ord = (Φ lv) } = record { lv = 0 ; ord = OSuc 0 (Φ lv) } |
46 osuc record { lv = Suc lx ; ord = (Φ (Suc lv)) } = record { lv = Suc lx ; ord = ℵ lv } | |
46 osuc record { lv = lx ; ord = (OSuc lx ox ) } = record { lv = lx ; ord = OSuc lx (OSuc lx ox) } | 47 osuc record { lv = lx ; ord = (OSuc lx ox ) } = record { lv = lx ; ord = OSuc lx (OSuc lx ox) } |
47 osuc record { lv = Suc lx ; ord = ℵ lx } = record { lv = Suc lx ; ord = OSuc (Suc lx) (ℵ lx) } | 48 osuc record { lv = Suc lx ; ord = ℵ lx } = record { lv = Suc lx ; ord = OSuc (Suc lx) (ℵ lx) } |
48 | 49 |
49 open import Data.Nat.Properties | 50 open import Data.Nat.Properties |
50 open import Data.Empty | 51 open import Data.Empty |
61 s<refl {n} {lv} {Φ lv} = Φ< | 62 s<refl {n} {lv} {Φ lv} = Φ< |
62 s<refl {n} {lv} {OSuc lv x} = s< s<refl | 63 s<refl {n} {lv} {OSuc lv x} = s< s<refl |
63 s<refl {n} {Suc lv} {ℵ lv} = ℵs< | 64 s<refl {n} {Suc lv} {ℵ lv} = ℵs< |
64 | 65 |
65 <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x | 66 <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x |
66 <-osuc {n} { record { lv = lv ; ord = (Φ .(lv)) } } = case2 Φ< | 67 <-osuc {n} { record { lv = 0 ; ord = Φ 0 } } = case2 Φ< |
67 <-osuc {n} { record { lv = lv ; ord = (OSuc lv ox ) } } = case2 ( s< s<refl ) | 68 <-osuc {n} { record { lv = (Suc lv) ; ord = Φ (Suc lv) } } = case2 ℵΦ< |
69 <-osuc {n} {record { lv = Zero ; ord = OSuc .0 ox }} = case2 ( s< s<refl ) | |
70 <-osuc {n} {record { lv = Suc lv₁ ; ord = OSuc .(Suc lv₁) ox }} = case2 ( s< s<refl ) | |
68 <-osuc {n} { record { lv = .(Suc lv₁) ; ord = (ℵ lv₁) } } = case2 ℵs< | 71 <-osuc {n} { record { lv = .(Suc lv₁) ; ord = (ℵ lv₁) } } = case2 ℵs< |
72 | |
73 osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x ) | |
74 osuc-lveq {n} {record { lv = 0 ; ord = Φ 0 }} = refl | |
75 osuc-lveq {n} {record { lv = Suc lv ; ord = Φ (Suc lv) }} = refl | |
76 osuc-lveq {n} {record { lv = Zero ; ord = OSuc .0 ord₁ }} = refl | |
77 osuc-lveq {n} {record { lv = Suc lv₁ ; ord = OSuc .(Suc lv₁) ord₁ }} = refl | |
78 osuc-lveq {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} = refl | |
79 | |
80 nat-<> : { x y : Nat } → x < y → y < x → ⊥ | |
81 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x | |
82 | |
83 osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x → x o< y → ⊥ | |
84 osuc-< {n} {record { lv = .0 ; ord = Φ .0 }} {record { lv = .(Suc _) ; ord = ord }} (case1 ()) (case1 (s≤s z≤n)) | |
85 osuc-< {n} {record { lv = .0 ; ord = OSuc .0 ord₁ }} {record { lv = .(Suc _) ; ord = ord }} (case1 ()) (case1 (s≤s z≤n)) | |
86 osuc-< {n} {record { lv = lx ; ord = xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) with osuc-lveq {n} {record { lv = lx ; ord = xo }} | |
87 osuc-< {n} {record { lv = Zero ; ord = Φ .0 }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2 | |
88 osuc-< {n} {record { lv = Suc lx ; ord = Φ .(Suc lx) }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2 | |
89 osuc-< {n} {record { lv = Zero ; ord = OSuc .0 xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2 | |
90 osuc-< {n} {record { lv = Suc lx ; ord = OSuc .(Suc lx) xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2 | |
91 osuc-< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | refl = nat-<> lt1 lt2 | |
92 osuc-< {n} {x} {y} (case1 x₁) (case2 x₂) = {!!} | |
93 osuc-< {n} {x} {y} (case2 x₁) (case1 x₂) = {!!} | |
94 osuc-< {n} {x} {y} (case2 x₁) (case2 x₂) = {!!} | |
69 | 95 |
70 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl) | 96 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl) |
71 | 97 |
72 ordinal-cong : {n : Level} {x y : Ordinal {n}} → | 98 ordinal-cong : {n : Level} {x y : Ordinal {n}} → |
73 lv x ≡ lv y → ord x ≅ ord y → x ≡ y | 99 lv x ≡ lv y → ord x ≅ ord y → x ≡ y |