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