Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison Ordinals.agda @ 221:1709c80b7275

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix Ordinals
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 08 Aug 2019 17:32:21 +0900
parents 95a26d1698f4
children 59771eb07df0
comparison
equal deleted inserted replaced
220:95a26d1698f4 221:1709c80b7275
13 open import Relation.Binary 13 open import Relation.Binary
14 open import Relation.Binary.Core 14 open import Relation.Binary.Core
15 15
16 16
17 17
18 record IsOrdinal {n : Level} (Ord : Set n) (_O<_ : Ord → Ord → Set n) : Set n where 18 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) : Set n where
19 field 19 field
20 Otrans : {x y z : Ord } → x O< y → y O< z → x O< z 20 Otrans : {x y z : ord } → x o< y → y o< z → x o< z
21 OTri : Trichotomous {n} _≡_ _O<_ 21 OTri : Trichotomous {n} _≡_ _o<_
22 ¬x<0 : { x : ord } → ¬ ( x o< o∅ )
23 <-osuc : { x : ord } → x o< osuc x
24 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
22 25
23 record Ordinal {n : Level} : Set (suc n) where 26 record Ordinals {n : Level} : Set (suc n) where
24 field 27 field
25 ord : Set n 28 ord : Set n
26 O< : ord → ord → Set n 29 o∅ : ord
27 isOrdinal : IsOrdinal ord O< 30 osuc : ord → ord
31 _o<_ : ord → ord → Set n
32 isOrdinal : IsOrdinals ord o∅ osuc _o<_
28 33
29 open Ordinal 34 module inOrdinal {n : Level} (O : Ordinals {n} ) where
30 35
31 _o<_ : {n : Level} ( x y : Ordinal {n}) → Set n 36 Ordinal : Set n
32 _o<_ x y = O< x {!!} {!!} -- (ord x) (ord y) 37 Ordinal = Ordinals.ord O
33 38
34 o<-dom : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal 39 _o<_ : Ordinal → Ordinal → Set n
35 o<-dom {n} {x} _ = x 40 _o<_ = Ordinals._o<_ O
36 41
37 o<-cod : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal 42 osuc : Ordinal → Ordinal
38 o<-cod {n} {_} {y} _ = y 43 osuc = Ordinals.osuc O
39 44
40 o<-subst : {n : Level } {Z X z x : Ordinal {n}} → Z o< X → Z ≡ z → X ≡ x → z o< x 45 o∅ : Ordinal
41 o<-subst df refl refl = df 46 o∅ = Ordinals.o∅ O
42 47
43 o∅ : {n : Level} → Ordinal {n} 48 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
44 o∅ = {!!} 49 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O)
50 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O)
51
52 o<-dom : { x y : Ordinal } → x o< y → Ordinal
53 o<-dom {x} _ = x
45 54
46 osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n} 55 o<-cod : { x y : Ordinal } → x o< y → Ordinal
47 osuc = {!!} 56 o<-cod {_} {y} _ = y
48 57
49 <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x 58 o<-subst : {Z X z x : Ordinal } → Z o< X → Z ≡ z → X ≡ x → z o< x
50 <-osuc = {!!} 59 o<-subst df refl refl = df
51 60
52 osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox → osuc oy o< osuc ox 61 ordtrans : {x y z : Ordinal } → x o< y → y o< z → x o< z
53 osucc = {!!} 62 ordtrans = IsOrdinals.Otrans (Ordinals.isOrdinal O)
54 63
55 o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy → ox o< oy → ⊥ 64 trio< : Trichotomous _≡_ _o<_
56 o<¬≡ = {!!} 65 trio< = IsOrdinals.OTri (Ordinals.isOrdinal O)
57 66
58 ¬x<0 : {n : Level} → { x : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} ) 67 o<¬≡ : { ox oy : Ordinal } → ox ≡ oy → ox o< oy → ⊥
59 ¬x<0 = {!!} 68 o<¬≡ {ox} {oy} eq lt with trio< ox oy
69 o<¬≡ {ox} {oy} eq lt | tri< a ¬b ¬c = ¬b eq
70 o<¬≡ {ox} {oy} eq lt | tri≈ ¬a b ¬c = ¬a lt
71 o<¬≡ {ox} {oy} eq lt | tri> ¬a ¬b c = ¬b eq
60 72
61 o<> : {n : Level} → {x y : Ordinal {n} } → y o< x → x o< y → ⊥ 73 o<> : {x y : Ordinal } → y o< x → x o< y → ⊥
62 o<> = {!!} 74 o<> {ox} {oy} lt tl with trio< ox oy
75 o<> {ox} {oy} lt tl | tri< a ¬b ¬c = ¬c lt
76 o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl
77 o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl
63 78
64 osuc-≡< : {n : Level} { a x : Ordinal {n} } → x o< osuc a → (x ≡ a ) ∨ (x o< a) 79 osuc-< : { x y : Ordinal } → y o< osuc x → x o< y → ⊥
65 osuc-≡< = {!!} 80 osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox
81 osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y
82 osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x
66 83
67 osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x → x o< y → ⊥ 84 osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox
68 osuc-< = {!!} 85 ---- y < osuc y < x < osuc x
86 ---- y < osuc y = x < osuc x
87 ---- y < osuc y > x < osuc x -> y = x ∨ x < y → ⊥
88 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
89 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
90 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc
91 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with osuc-≡< c
92 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox)
93 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox)
69 94
70 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n) 95 open _∧_
71 a o≤ b = (a ≡ b) ∨ ( a o< b )
72 96
73 ordtrans : {n : Level} {x y z : Ordinal {n} } → x o< y → y o< z → x o< z 97 osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
74 ordtrans = {!!} 98 proj2 (osuc2 x y) lt = osucc lt
99 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy
100 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy
101 proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy
75 102
76 trio< : {n : Level } → Trichotomous {suc n} _≡_ _o<_ 103 _o≤_ : Ordinal → Ordinal → Set n
77 trio< = {!!} 104 a o≤ b = (a ≡ b) ∨ ( a o< b )
78 105
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 106
85 maxα : {n : Level} → Ordinal {suc n} → Ordinal → Ordinal 107 xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob
86 maxα x y with trio< x y 108 xo<ab {oa} {ob} a→b with trio< oa ob
87 maxα x y | tri< a ¬b ¬c = y 109 xo<ab {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc
88 maxα x y | tri> ¬a ¬b c = x 110 xo<ab {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc
89 maxα x y | tri≈ ¬a refl ¬c = x 111 xo<ab {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) )
90 112
91 minα : {n : Level} → Ordinal {n} → Ordinal → Ordinal 113 maxα : Ordinal → Ordinal → Ordinal
92 minα {n} x y with trio< {n} x y 114 maxα x y with trio< x y
93 minα x y | tri< a ¬b ¬c = x 115 maxα x y | tri< a ¬b ¬c = y
94 minα x y | tri> ¬a ¬b c = y 116 maxα x y | tri> ¬a ¬b c = x
95 minα x y | tri≈ ¬a refl ¬c = x 117 maxα x y | tri≈ ¬a refl ¬c = x
96 118
97 min1 : {n : Level} → {x y z : Ordinal {n} } → z o< x → z o< y → z o< minα x y 119 minα : Ordinal → Ordinal → Ordinal
98 min1 {n} {x} {y} {z} z<x z<y with trio< {n} x y 120 minα x y with trio< x y
99 min1 {n} {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x 121 minα x y | tri< a ¬b ¬c = x
100 min1 {n} {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x 122 minα x y | tri> ¬a ¬b c = y
101 min1 {n} {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y 123 minα x y | tri≈ ¬a refl ¬c = x
102 124
103 -- 125 min1 : {x y z : Ordinal } → z o< x → z o< y → z o< minα x y
104 -- max ( osuc x , osuc y ) 126 min1 {x} {y} {z} z<x z<y with trio< x y
105 -- 127 min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
128 min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
129 min1 {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
106 130
107 omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n} 131 --
108 omax {n} x y with trio< x y 132 -- max ( osuc x , osuc y )
109 omax {n} x y | tri< a ¬b ¬c = osuc y 133 --
110 omax {n} x y | tri> ¬a ¬b c = osuc x
111 omax {n} x y | tri≈ ¬a refl ¬c = osuc x
112 134
113 omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y 135 omax : ( x y : Ordinal ) → Ordinal
114 omax< {n} x y lt with trio< x y 136 omax x y with trio< x y
115 omax< {n} x y lt | tri< a ¬b ¬c = refl 137 omax x y | tri< a ¬b ¬c = osuc y
116 omax< {n} x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt ) 138 omax x y | tri> ¬a ¬b c = osuc x
117 omax< {n} x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt ) 139 omax x y | tri≈ ¬a refl ¬c = osuc x
118 140
119 omax≡ : {n : Level} ( x y : Ordinal {suc n} ) → x ≡ y → osuc y ≡ omax x y 141 omax< : ( x y : Ordinal ) → x o< y → osuc y ≡ omax x y
120 omax≡ {n} x y eq with trio< x y 142 omax< x y lt with trio< x y
121 omax≡ {n} x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq ) 143 omax< x y lt | tri< a ¬b ¬c = refl
122 omax≡ {n} x y eq | tri≈ ¬a refl ¬c = refl 144 omax< x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
123 omax≡ {n} x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq ) 145 omax< x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
124 146
125 omax-x : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y 147 omax≡ : ( x y : Ordinal ) → x ≡ y → osuc y ≡ omax x y
126 omax-x {n} x y with trio< x y 148 omax≡ x y eq with trio< x y
127 omax-x {n} x y | tri< a ¬b ¬c = ordtrans a <-osuc 149 omax≡ x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
128 omax-x {n} x y | tri> ¬a ¬b c = <-osuc 150 omax≡ x y eq | tri≈ ¬a refl ¬c = refl
129 omax-x {n} x y | tri≈ ¬a refl ¬c = <-osuc 151 omax≡ x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq )
130 152
131 omax-y : {n : Level} ( x y : Ordinal {suc n} ) → y o< omax x y 153 omax-x : ( x y : Ordinal ) → x o< omax x y
132 omax-y {n} x y with trio< x y 154 omax-x x y with trio< x y
133 omax-y {n} x y | tri< a ¬b ¬c = <-osuc 155 omax-x x y | tri< a ¬b ¬c = ordtrans a <-osuc
134 omax-y {n} x y | tri> ¬a ¬b c = ordtrans c <-osuc 156 omax-x x y | tri> ¬a ¬b c = <-osuc
135 omax-y {n} x y | tri≈ ¬a refl ¬c = <-osuc 157 omax-x x y | tri≈ ¬a refl ¬c = <-osuc
136 158
137 omxx : {n : Level} ( x : Ordinal {suc n} ) → omax x x ≡ osuc x 159 omax-y : ( x y : Ordinal ) → y o< omax x y
138 omxx {n} x with trio< x x 160 omax-y x y with trio< x y
139 omxx {n} x | tri< a ¬b ¬c = ⊥-elim (¬b refl ) 161 omax-y x y | tri< a ¬b ¬c = <-osuc
140 omxx {n} x | tri> ¬a ¬b c = ⊥-elim (¬b refl ) 162 omax-y x y | tri> ¬a ¬b c = ordtrans c <-osuc
141 omxx {n} x | tri≈ ¬a refl ¬c = refl 163 omax-y x y | tri≈ ¬a refl ¬c = <-osuc
142 164
143 omxxx : {n : Level} ( x : Ordinal {suc n} ) → omax x (omax x x ) ≡ osuc (osuc x) 165 omxx : ( x : Ordinal ) → omax x x ≡ osuc x
144 omxxx {n} x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc )) 166 omxx x with trio< x x
167 omxx x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
168 omxx x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
169 omxx x | tri≈ ¬a refl ¬c = refl
145 170
146 open _∧_ 171 omxxx : ( x : Ordinal ) → omax x (omax x x ) ≡ osuc (osuc x)
172 omxxx x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
147 173
148 osuc2 : {n : Level} ( x y : Ordinal {suc n} ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y) 174 open _∧_
149 osuc2 = {!!}
150 175
151 OrdTrans : {n : Level} → Transitive {suc n} _o≤_ 176 OrdTrans : Transitive _o≤_
152 OrdTrans (case1 refl) (case1 refl) = case1 refl 177 OrdTrans (case1 refl) (case1 refl) = case1 refl
153 OrdTrans (case1 refl) (case2 lt2) = case2 lt2 178 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
154 OrdTrans (case2 lt1) (case1 refl) = case2 lt1 179 OrdTrans (case2 lt1) (case1 refl) = case2 lt1
155 OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y) 180 OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
156 181
157 OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n) 182 OrdPreorder : Preorder n n n
158 OrdPreorder {n} = record { Carrier = Ordinal 183 OrdPreorder = record { Carrier = Ordinal
159 ; _≈_ = _≡_ 184 ; _≈_ = _≡_
160 ; _∼_ = _o≤_ 185 ; _∼_ = _o≤_
161 ; isPreorder = record { 186 ; isPreorder = record {
162 isEquivalence = record { refl = refl ; sym = sym ; trans = trans } 187 isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
163 ; reflexive = case1 188 ; reflexive = case1
164 ; trans = OrdTrans 189 ; trans = OrdTrans
165 } 190 }
166 } 191 }
167 192
168 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m } 193 TransFiniteExists : {m l : Level} → ( ψ : Ordinal → Set m )
169 → {!!} 194 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
170 → {!!} 195 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
171 → ∀ (x : Ordinal) → ψ x 196 → ¬ p
172 TransFinite {n} {m} {ψ} = {!!} 197 TransFiniteExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
173 198
174 -- we cannot prove this in intutionistic logic
175 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p
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 )
185 → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → ¬ p )
186 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
187 → ¬ p
188 TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
189