Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ordinal.agda @ 74:819da8c08f05
ordinal atomical successor?
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 01 Jun 2019 19:19:40 +0900 |
parents | dd430a95610f |
children | 714470702a8b |
comparison
equal
deleted
inserted
replaced
73:dd430a95610f | 74:819da8c08f05 |
---|---|
39 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) | 39 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) |
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} | |
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 } | |
47 osuc record { lv = lx ; ord = (OSuc lx ox ) } = record { lv = lx ; ord = OSuc lx (OSuc lx ox) } | |
48 osuc record { lv = Suc lx ; ord = ℵ lx } = record { lv = Suc lx ; ord = OSuc (Suc lx) (ℵ lx) } | |
49 | |
50 open import Data.Nat.Properties | 44 open import Data.Nat.Properties |
51 open import Data.Empty | 45 open import Data.Empty |
52 open import Data.Unit using ( ⊤ ) | 46 open import Data.Unit using ( ⊤ ) |
53 open import Relation.Nullary | 47 open import Relation.Nullary |
54 | 48 |
60 | 54 |
61 s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x | 55 s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x |
62 s<refl {n} {lv} {Φ lv} = Φ< | 56 s<refl {n} {lv} {Φ lv} = Φ< |
63 s<refl {n} {lv} {OSuc lv x} = s< s<refl | 57 s<refl {n} {lv} {OSuc lv x} = s< s<refl |
64 s<refl {n} {Suc lv} {ℵ lv} = ℵs< | 58 s<refl {n} {Suc lv} {ℵ lv} = ℵs< |
65 | |
66 <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x | |
67 <-osuc {n} { record { lv = 0 ; ord = Φ 0 } } = case2 Φ< | |
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 ) | |
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₂) = {!!} | |
95 | 59 |
96 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl) | 60 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl) |
97 | 61 |
98 ordinal-cong : {n : Level} {x y : Ordinal {n}} → | 62 ordinal-cong : {n : Level} {x y : Ordinal {n}} → |
99 lv x ≡ lv y → ord x ≅ ord y → x ≡ y | 63 lv x ≡ lv y → ord x ≅ ord y → x ≡ y |
157 d<→lv (s< lt) = refl | 121 d<→lv (s< lt) = refl |
158 d<→lv ℵΦ< = refl | 122 d<→lv ℵΦ< = refl |
159 d<→lv (ℵ< _) = refl | 123 d<→lv (ℵ< _) = refl |
160 d<→lv ℵs< = refl | 124 d<→lv ℵs< = refl |
161 d<→lv (ℵss< _) = refl | 125 d<→lv (ℵss< _) = refl |
126 | |
127 osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n} | |
128 osuc record { lv = 0 ; ord = (Φ lv) } = record { lv = 0 ; ord = OSuc 0 (Φ lv) } | |
129 osuc record { lv = Suc lx ; ord = (Φ (Suc lv)) } = record { lv = Suc lx ; ord = ℵ lv } | |
130 osuc record { lv = 0 ; ord = (OSuc 0 ox ) } = record { lv = 0 ; ord = OSuc 0 (OSuc 0 ox) } | |
131 osuc record { lv = Suc lx ; ord = (OSuc (Suc lx) ox ) } = record { lv = Suc lx ; ord = OSuc (Suc lx) (OSuc (Suc lx) ox) } | |
132 osuc record { lv = Suc lx ; ord = ℵ lx } = record { lv = Suc lx ; ord = OSuc (Suc lx) (ℵ lx) } | |
133 | |
134 <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x | |
135 <-osuc {n} { record { lv = 0 ; ord = Φ 0 } } = case2 Φ< | |
136 <-osuc {n} { record { lv = (Suc lv) ; ord = Φ (Suc lv) } } = case2 ℵΦ< | |
137 <-osuc {n} {record { lv = Zero ; ord = OSuc .0 ox }} = case2 ( s< s<refl ) | |
138 <-osuc {n} {record { lv = Suc lv₁ ; ord = OSuc .(Suc lv₁) ox }} = case2 ( s< s<refl ) | |
139 <-osuc {n} { record { lv = .(Suc lv₁) ; ord = (ℵ lv₁) } } = case2 ℵs< | |
140 | |
141 osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x ) | |
142 osuc-lveq {n} {record { lv = 0 ; ord = Φ 0 }} = refl | |
143 osuc-lveq {n} {record { lv = Suc lv ; ord = Φ (Suc lv) }} = refl | |
144 osuc-lveq {n} {record { lv = Zero ; ord = OSuc .0 ord₁ }} = refl | |
145 osuc-lveq {n} {record { lv = Suc lv₁ ; ord = OSuc .(Suc lv₁) ord₁ }} = refl | |
146 osuc-lveq {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} = refl | |
147 | |
148 nat-<> : { x y : Nat } → x < y → y < x → ⊥ | |
149 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x | |
150 | |
151 nat-<≡ : { x : Nat } → x < x → ⊥ | |
152 nat-<≡ (s≤s lt) = nat-<≡ lt | |
153 | |
154 osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x → x o< y → ⊥ | |
155 osuc-< {n} {record { lv = .0 ; ord = Φ .0 }} {record { lv = .(Suc _) ; ord = ord }} (case1 ()) (case1 (s≤s z≤n)) | |
156 osuc-< {n} {record { lv = .0 ; ord = OSuc .0 ord₁ }} {record { lv = .(Suc _) ; ord = ord }} (case1 ()) (case1 (s≤s z≤n)) | |
157 osuc-< {n} {record { lv = Suc lx ; ord = Φ .(Suc lx) }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) = nat-<> lt1 lt2 | |
158 osuc-< {n} {record { lv = Suc lx ; ord = OSuc .(Suc lx) xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) = nat-<> lt1 lt2 | |
159 osuc-< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) = nat-<> lt1 lt2 | |
160 osuc-< {n} {x} {y} (case1 x₁) (case2 x₂) with d<→lv x₂ | osuc-lveq {n} {x} | |
161 ... | refl | eq = {!!} | |
162 osuc-< {n} {x} {y} (case2 x₁) (case1 x₂) with d<→lv x₁ | osuc-lveq {n} {x} | |
163 ... | refl | eq = {!!} | |
164 osuc-< {n} {record { lv = Zero ; ord = Φ .0 }} {record { lv = Zero ; ord = Φ .0 }} (case2 Φ<) (case2 ()) | |
165 osuc-< {n} {record { lv = Suc lv₁ ; ord = Φ .(Suc lv₁) }} {record { lv = Zero ; ord = Φ .0 }} (case2 ()) (case2 x₂) | |
166 osuc-< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = Suc lv₂ ; ord = Φ .(Suc lv₂) }} (case2 x₁) (case2 ()) | |
167 osuc-< {n} {record { lv = .0 ; ord = Φ .0 }} {record { lv = Zero ; ord = OSuc .0 ord₁ }} (case2 (s< ())) (case2 Φ<) | |
168 osuc-< {n} {record { lv = .1 ; ord = ℵ Zero }} {record { lv = .1 ; ord = ℵ Zero }} (case2 ℵs<) (case2 ()) | |
169 osuc-< {n} {record { lv = .1 ; ord = ℵ Zero }} {record { lv = .1 ; ord = ℵ Zero }} (case2 (ℵss< x₁)) (case2 ()) | |
170 osuc-< {n} {record { lv = .1 ; ord = ℵ Zero }} {record { lv = .(Suc (Suc lv₂)) ; ord = ℵ Suc lv₂ }} (case2 ()) (case2 x₂) | |
171 osuc-< {n} {record { lv = .(Suc (Suc lv₁)) ; ord = ℵ Suc lv₁ }} {record { lv = .(Suc (Suc lv₁)) ; ord = ℵ .(Suc lv₁) }} (case2 ℵs<) (case2 ()) | |
172 osuc-< {n} {record { lv = .(Suc (Suc lv₁)) ; ord = ℵ Suc lv₁ }} {record { lv = .(Suc (Suc lv₁)) ; ord = ℵ .(Suc lv₁) }} (case2 (ℵss< x₁)) (case2 ()) | |
173 osuc-< {n} {record { lv = Suc lv₁ ; ord = .(Φ (Suc lv₁)) }} {record { lv = .(Suc lv₁) ; ord = (OSuc (Suc lv₁) y) }} (case2 (ℵ< x)) (case2 Φ<) = {!!} | |
174 osuc-< {n} {record { lv = Zero ; ord = (OSuc 0 ox) }} {record { lv = .0 ; ord = (OSuc 0 oy) }} (case2 (s< c1)) (case2 (s< c2)) = | |
175 osuc-< {n} {record { lv = Zero ; ord = ox }} {record { lv = 0 ; ord = oy }} (case2 {!!}) (case2 c2) | |
176 osuc-< {n} {record { lv = Suc lv₁ ; ord = .(OSuc (Suc lv₁) _) }} {record { lv = .(Suc lv₁) ; ord = .(OSuc (Suc lv₁) _) }} (case2 (s< c1)) (case2 (s< c2)) = {!!} | |
177 osuc-< {n} {record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 (ℵss< c1)) (case2 (ℵ< x)) = {!!} | |
178 osuc-< {n} {record { lv = .(Suc _) ; ord = .(ℵ _) }} {record { lv = .(Suc _) ; ord = .(OSuc (Suc _) (ℵ _)) }} (case2 (s< c1)) (case2 ℵs<) = {!!} | |
179 osuc-< {n} {record { lv = .(Suc _) ; ord = .(ℵ _) }} {record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) }} (case2 (s< c1)) (case2 (ℵss< c2)) = {!!} | |
180 | |
162 | 181 |
163 xsyℵ : {n : Level} {lx : Nat} {x y : OrdinalD {n} lx } → x d< y → ¬ℵ y → ¬ℵ x | 182 xsyℵ : {n : Level} {lx : Nat} {x y : OrdinalD {n} lx } → x d< y → ¬ℵ y → ¬ℵ x |
164 xsyℵ {_} {_} {Φ lv₁} {y} x<y t = ¬ℵΦ | 183 xsyℵ {_} {_} {Φ lv₁} {y} x<y t = ¬ℵΦ |
165 xsyℵ {_} {_} {OSuc lv₁ x} {OSuc lv₁ y} (s< x<y) (¬ℵs t) = ¬ℵs ( xsyℵ x<y t) | 184 xsyℵ {_} {_} {OSuc lv₁ x} {OSuc lv₁ y} (s< x<y) (¬ℵs t) = ¬ℵs ( xsyℵ x<y t) |
166 xsyℵ {_} {_} {OSuc .(Suc _) x} {.(ℵ _)} (ℵ< x₁) () | 185 xsyℵ {_} {_} {OSuc .(Suc _) x} {.(ℵ _)} (ℵ< x₁) () |