Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate Ordinals.agda @ 235:846e0926bb89
fix cardinal
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 15 Aug 2019 04:51:24 +0900 |
| parents | 59771eb07df0 |
| children | 63df67b6281c |
| 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 |
|
222
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
16 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where |
| 16 | 17 field |
| 221 | 18 Otrans : {x y z : ord } → x o< y → y o< z → x o< z |
| 19 OTri : Trichotomous {n} _≡_ _o<_ | |
| 20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) | |
| 21 <-osuc : { x : ord } → x o< osuc x | |
| 22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) | |
|
222
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
23 TransFinite : { ψ : ord → Set (suc n) } |
|
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
24 → ( (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
|
25 → ∀ (x : ord) → ψ x |
| 16 | 26 |
|
222
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
27 |
|
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
28 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
|
29 field |
|
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
30 ord : Set n |
| 221 | 31 o∅ : ord |
| 32 osuc : ord → ord | |
| 33 _o<_ : ord → ord → Set n | |
| 34 isOrdinal : IsOrdinals ord o∅ osuc _o<_ | |
| 17 | 35 |
| 221 | 36 module inOrdinal {n : Level} (O : Ordinals {n} ) where |
| 3 | 37 |
| 221 | 38 Ordinal : Set n |
| 39 Ordinal = Ordinals.ord O | |
| 40 | |
| 41 _o<_ : Ordinal → Ordinal → Set n | |
| 42 _o<_ = Ordinals._o<_ O | |
| 218 | 43 |
| 221 | 44 osuc : Ordinal → Ordinal |
| 45 osuc = Ordinals.osuc O | |
| 218 | 46 |
| 221 | 47 o∅ : Ordinal |
| 48 o∅ = Ordinals.o∅ O | |
|
43
0d9b9db14361
equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
49 |
| 221 | 50 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O) |
| 51 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) | |
| 52 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) | |
| 235 | 53 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) |
| 221 | 54 |
| 55 o<-dom : { x y : Ordinal } → x o< y → Ordinal | |
| 56 o<-dom {x} _ = x | |
|
74
819da8c08f05
ordinal atomical successor?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
57 |
| 221 | 58 o<-cod : { x y : Ordinal } → x o< y → Ordinal |
| 59 o<-cod {_} {y} _ = y | |
| 147 | 60 |
| 221 | 61 o<-subst : {Z X z x : Ordinal } → Z o< X → Z ≡ z → X ≡ x → z o< x |
| 62 o<-subst df refl refl = df | |
| 94 | 63 |
| 221 | 64 ordtrans : {x y z : Ordinal } → x o< y → y o< z → x o< z |
| 65 ordtrans = IsOrdinals.Otrans (Ordinals.isOrdinal O) | |
| 94 | 66 |
| 221 | 67 trio< : Trichotomous _≡_ _o<_ |
| 68 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
|
69 |
| 221 | 70 o<¬≡ : { ox oy : Ordinal } → ox ≡ oy → ox o< oy → ⊥ |
| 71 o<¬≡ {ox} {oy} eq lt with trio< ox oy | |
| 72 o<¬≡ {ox} {oy} eq lt | tri< a ¬b ¬c = ¬b eq | |
| 73 o<¬≡ {ox} {oy} eq lt | tri≈ ¬a b ¬c = ¬a lt | |
| 74 o<¬≡ {ox} {oy} eq lt | tri> ¬a ¬b c = ¬b eq | |
| 23 | 75 |
| 221 | 76 o<> : {x y : Ordinal } → y o< x → x o< y → ⊥ |
| 77 o<> {ox} {oy} lt tl with trio< ox oy | |
| 78 o<> {ox} {oy} lt tl | tri< a ¬b ¬c = ¬c lt | |
| 79 o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl | |
| 80 o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl | |
| 23 | 81 |
| 221 | 82 osuc-< : { x y : Ordinal } → y o< osuc x → x o< y → ⊥ |
| 83 osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox | |
| 84 osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y | |
| 85 osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x | |
| 180 | 86 |
| 221 | 87 osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox |
| 88 ---- y < osuc y < x < osuc x | |
| 89 ---- y < osuc y = x < osuc x | |
| 90 ---- y < osuc y > x < osuc x -> y = x ∨ x < y → ⊥ | |
| 91 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox | |
| 92 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc | |
| 93 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc | |
| 94 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with osuc-≡< c | |
| 95 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox) | |
| 96 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox) | |
| 97 | |
| 98 open _∧_ | |
| 84 | 99 |
| 221 | 100 osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y) |
| 101 proj2 (osuc2 x y) lt = osucc lt | |
| 102 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy | |
| 103 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy | |
| 104 proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy | |
| 129 | 105 |
| 221 | 106 _o≤_ : Ordinal → Ordinal → Set n |
| 107 a o≤ b = (a ≡ b) ∨ ( a o< b ) | |
| 108 | |
| 129 | 109 |
| 221 | 110 xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob |
| 111 xo<ab {oa} {ob} a→b with trio< oa ob | |
| 112 xo<ab {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc | |
| 113 xo<ab {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc | |
| 114 xo<ab {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) ) | |
| 88 | 115 |
| 221 | 116 maxα : Ordinal → Ordinal → Ordinal |
| 117 maxα x y with trio< x y | |
| 118 maxα x y | tri< a ¬b ¬c = y | |
| 119 maxα x y | tri> ¬a ¬b c = x | |
| 120 maxα x y | tri≈ ¬a refl ¬c = x | |
| 84 | 121 |
| 221 | 122 minα : Ordinal → Ordinal → Ordinal |
| 123 minα x y with trio< x y | |
| 124 minα x y | tri< a ¬b ¬c = x | |
| 125 minα x y | tri> ¬a ¬b c = y | |
| 126 minα x y | tri≈ ¬a refl ¬c = x | |
| 88 | 127 |
| 221 | 128 min1 : {x y z : Ordinal } → z o< x → z o< y → z o< minα x y |
| 129 min1 {x} {y} {z} z<x z<y with trio< x y | |
| 130 min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x | |
| 131 min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x | |
| 132 min1 {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y | |
| 84 | 133 |
| 221 | 134 -- |
| 135 -- max ( osuc x , osuc y ) | |
| 136 -- | |
| 137 | |
| 138 omax : ( x y : Ordinal ) → Ordinal | |
| 139 omax x y with trio< x y | |
| 140 omax x y | tri< a ¬b ¬c = osuc y | |
| 141 omax x y | tri> ¬a ¬b c = osuc x | |
| 142 omax x y | tri≈ ¬a refl ¬c = osuc x | |
| 86 | 143 |
| 221 | 144 omax< : ( x y : Ordinal ) → x o< y → osuc y ≡ omax x y |
| 145 omax< x y lt with trio< x y | |
| 146 omax< x y lt | tri< a ¬b ¬c = refl | |
| 147 omax< x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt ) | |
| 148 omax< x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt ) | |
| 86 | 149 |
| 221 | 150 omax≡ : ( x y : Ordinal ) → x ≡ y → osuc y ≡ omax x y |
| 151 omax≡ x y eq with trio< x y | |
| 152 omax≡ x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq ) | |
| 153 omax≡ x y eq | tri≈ ¬a refl ¬c = refl | |
| 154 omax≡ x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq ) | |
| 91 | 155 |
| 221 | 156 omax-x : ( x y : Ordinal ) → x o< omax x y |
| 157 omax-x x y with trio< x y | |
| 158 omax-x x y | tri< a ¬b ¬c = ordtrans a <-osuc | |
| 159 omax-x x y | tri> ¬a ¬b c = <-osuc | |
| 160 omax-x x y | tri≈ ¬a refl ¬c = <-osuc | |
| 16 | 161 |
| 221 | 162 omax-y : ( x y : Ordinal ) → y o< omax x y |
| 163 omax-y x y with trio< x y | |
| 164 omax-y x y | tri< a ¬b ¬c = <-osuc | |
| 165 omax-y x y | tri> ¬a ¬b c = ordtrans c <-osuc | |
| 166 omax-y x y | tri≈ ¬a refl ¬c = <-osuc | |
| 167 | |
| 168 omxx : ( x : Ordinal ) → omax x x ≡ osuc x | |
| 169 omxx x with trio< x x | |
| 170 omxx x | tri< a ¬b ¬c = ⊥-elim (¬b refl ) | |
| 171 omxx x | tri> ¬a ¬b c = ⊥-elim (¬b refl ) | |
| 172 omxx x | tri≈ ¬a refl ¬c = refl | |
| 173 | |
| 174 omxxx : ( x : Ordinal ) → omax x (omax x x ) ≡ osuc (osuc x) | |
| 175 omxxx x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc )) | |
| 176 | |
| 177 open _∧_ | |
| 16 | 178 |
| 221 | 179 OrdTrans : Transitive _o≤_ |
| 180 OrdTrans (case1 refl) (case1 refl) = case1 refl | |
| 181 OrdTrans (case1 refl) (case2 lt2) = case2 lt2 | |
| 182 OrdTrans (case2 lt1) (case1 refl) = case2 lt1 | |
| 183 OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y) | |
|
97
f2b579106770
power set using sup on Def
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
184 |
| 221 | 185 OrdPreorder : Preorder n n n |
| 186 OrdPreorder = record { Carrier = Ordinal | |
| 187 ; _≈_ = _≡_ | |
| 188 ; _∼_ = _o≤_ | |
| 189 ; isPreorder = record { | |
| 190 isEquivalence = record { refl = refl ; sym = sym ; trans = trans } | |
| 191 ; reflexive = case1 | |
| 192 ; trans = OrdTrans | |
| 193 } | |
| 194 } | |
| 165 | 195 |
| 221 | 196 TransFiniteExists : {m l : Level} → ( ψ : Ordinal → Set m ) |
| 197 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) | |
| 198 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) | |
| 199 → ¬ p | |
| 200 TransFiniteExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) | |
| 201 |