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

comparison Ordinals.agda @ 220:95a26d1698f4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
219:43021d2b8756 220:95a26d1698f4
1 open import Level
2 module Ordinals where
3
4 open import zf
5
6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
7 open import Data.Empty
8 open import Relation.Binary.PropositionalEquality
9 open import logic
10 open import nat
11 open import Data.Unit using ( ⊤ )
12 open import Relation.Nullary
13 open import Relation.Binary
14 open import Relation.Binary.Core
15
16
17
18 record IsOrdinal {n : Level} (Ord : Set n) (_O<_ : Ord → Ord → Set n) : Set n where
19 field
20 Otrans : {x y z : Ord } → x O< y → y O< z → x O< z
21 OTri : Trichotomous {n} _≡_ _O<_
22
23 record Ordinal {n : Level} : Set (suc n) where
24 field
25 ord : Set n
26 O< : ord → ord → Set n
27 isOrdinal : IsOrdinal ord O<
28
29 open Ordinal
30
31 _o<_ : {n : Level} ( x y : Ordinal {n}) → Set n
32 _o<_ x y = O< x {!!} {!!} -- (ord x) (ord y)
33
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
40 o<-subst : {n : Level } {Z X z x : Ordinal {n}} → Z o< X → Z ≡ z → X ≡ x → z o< x
41 o<-subst df refl refl = df
42
43 o∅ : {n : Level} → Ordinal {n}
44 o∅ = {!!}
45
46 osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n}
47 osuc = {!!}
48
49 <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x
50 <-osuc = {!!}
51
52 osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox → osuc oy o< osuc ox
53 osucc = {!!}
54
55 o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy → ox o< oy → ⊥
56 o<¬≡ = {!!}
57
58 ¬x<0 : {n : Level} → { x : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
59 ¬x<0 = {!!}
60
61 o<> : {n : Level} → {x y : Ordinal {n} } → y o< x → x o< y → ⊥
62 o<> = {!!}
63
64 osuc-≡< : {n : Level} { a x : Ordinal {n} } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
65 osuc-≡< = {!!}
66
67 osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x → x o< y → ⊥
68 osuc-< = {!!}
69
70 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
71 a o≤ b = (a ≡ b) ∨ ( a o< b )
72
73 ordtrans : {n : Level} {x y z : Ordinal {n} } → x o< y → y o< z → x o< z
74 ordtrans = {!!}
75
76 trio< : {n : Level } → Trichotomous {suc n} _≡_ _o<_
77 trio< = {!!}
78
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
85 maxα : {n : Level} → Ordinal {suc n} → Ordinal → Ordinal
86 maxα x y with trio< x y
87 maxα x y | tri< a ¬b ¬c = y
88 maxα x y | tri> ¬a ¬b c = x
89 maxα x y | tri≈ ¬a refl ¬c = x
90
91 minα : {n : Level} → Ordinal {n} → Ordinal → Ordinal
92 minα {n} x y with trio< {n} x y
93 minα x y | tri< a ¬b ¬c = x
94 minα x y | tri> ¬a ¬b c = y
95 minα x y | tri≈ ¬a refl ¬c = x
96
97 min1 : {n : Level} → {x y z : Ordinal {n} } → z o< x → z o< y → z o< minα x y
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
103 --
104 -- max ( osuc x , osuc y )
105 --
106
107 omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n}
108 omax {n} x y with trio< x y
109 omax {n} x y | tri< a ¬b ¬c = osuc y
110 omax {n} x y | tri> ¬a ¬b c = osuc x
111 omax {n} x y | tri≈ ¬a refl ¬c = osuc x
112
113 omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y
114 omax< {n} x y lt with trio< x y
115 omax< {n} x y lt | tri< a ¬b ¬c = refl
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 )
124
125 omax-x : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y
126 omax-x {n} x y with trio< x y
127 omax-x {n} x y | tri< a ¬b ¬c = ordtrans a <-osuc
128 omax-x {n} x y | tri> ¬a ¬b c = <-osuc
129 omax-x {n} x y | tri≈ ¬a refl ¬c = <-osuc
130
131 omax-y : {n : Level} ( x y : Ordinal {suc n} ) → y o< omax x y
132 omax-y {n} x y with trio< x y
133 omax-y {n} x y | tri< a ¬b ¬c = <-osuc
134 omax-y {n} x y | tri> ¬a ¬b c = ordtrans c <-osuc
135 omax-y {n} x y | tri≈ ¬a refl ¬c = <-osuc
136
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
142
143 omxxx : {n : Level} ( x : Ordinal {suc n} ) → omax x (omax x x ) ≡ osuc (osuc x)
144 omxxx {n} x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
145
146 open _∧_
147
148 osuc2 : {n : Level} ( x y : Ordinal {suc n} ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
149 osuc2 = {!!}
150
151 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
152 OrdTrans (case1 refl) (case1 refl) = case1 refl
153 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
154 OrdTrans (case2 lt1) (case1 refl) = case2 lt1
155 OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
156
157 OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n)
158 OrdPreorder {n} = record { Carrier = Ordinal
159 ; _≈_ = _≡_
160 ; _∼_ = _o≤_
161 ; isPreorder = record {
162 isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
163 ; reflexive = case1
164 ; trans = OrdTrans
165 }
166 }
167
168 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
169 → {!!}
170 → {!!}
171 → ∀ (x : Ordinal) → ψ x
172 TransFinite {n} {m} {ψ} = {!!}
173
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