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

comparison src/ODC.agda @ 469:69f90d8d0607

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 23 Mar 2022 21:42:12 +0900
parents c70cf01b29f9
children f57f92c7c874
comparison
equal deleted inserted replaced
468:c70cf01b29f9 469:69f90d8d0607
104 OrdP x y with trio< x (& y) 104 OrdP x y with trio< x (& y)
105 OrdP x y | tri< a ¬b ¬c = no ¬c 105 OrdP x y | tri< a ¬b ¬c = no ¬c
106 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) 106 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
107 OrdP x y | tri> ¬a ¬b c = yes c 107 OrdP x y | tri> ¬a ¬b c = yes c
108 108
109 open import Relation.Binary.HeterogeneousEquality as HE -- using (_≅_;refl)
110
111 record Element (A : HOD) : Set (suc n) where
112 field
113 elm : HOD
114 is-elm : A ∋ elm
115
116 open Element
117
109 TotalOrderSet : ( A : HOD ) → (_<_ : (x y : HOD) → Set n ) → Set (suc n) 118 TotalOrderSet : ( A : HOD ) → (_<_ : (x y : HOD) → Set n ) → Set (suc n)
110 TotalOrderSet A _<_ = {a b : HOD} → A ∋ a → A ∋ b → (a < b) ∨ (a ≡ b) ∨ (b < a ) 119 TotalOrderSet A _<_ = Trichotomous (λ (x : Element A) y → elm x ≡ elm y ) (λ x y → elm x < elm y )
120
121 me : { A a : HOD } → A ∋ a → Element A
122 me {A} {a} lt = record { elm = a ; is-elm = lt }
123
124 -- elm-cmp : {A a b : HOD} → {_<_ : (x y : HOD) → Set n } → A ∋ a → A ∋ b → TotalOrderSet A _<_ → Tri _ _ _
125 -- elm-cmp {A} {a} {b} ax bx cmp = cmp (me ax) (me bx)
111 126
112 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where 127 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
113 field 128 field
114 sup : HOD 129 sup : HOD
115 A∋maximal : A ∋ sup 130 A∋maximal : A ∋ sup
116 x≤sup : (x : HOD) → B ∋ x → (x ≡ sup ) ∨ (x < sup ) 131 x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )
117 132
118 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where 133 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
119 field 134 field
120 maximal : HOD 135 maximal : HOD
121 A∋maximal : HOD 136 A∋maximal : HOD
122 ¬maximal<x : (x : HOD) → (b : A ∋ x ) → ¬ maximal < x 137 ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x
123 138
124 record ZChain ( A : HOD ) (y : Ordinal) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where 139 record ZChain ( A : HOD ) (y : Ordinal) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
125 field 140 field
126 B : HOD 141 B : HOD
127 B⊆A : B ⊆ A 142 B⊆A : B ⊆ A
135 → ( ( B : HOD) → (B⊆A : B ⊆ A) → TotalOrderSet B _<_ → SUP A B _<_ ) 150 → ( ( B : HOD) → (B⊆A : B ⊆ A) → TotalOrderSet B _<_ → SUP A B _<_ )
136 → Maximal A _<_ 151 → Maximal A _<_
137 Zorn-lemma {A} {_<_} 0<A supP = zorn00 where 152 Zorn-lemma {A} {_<_} 0<A supP = zorn00 where
138 HasMaximal : HOD 153 HasMaximal : HOD
139 HasMaximal = record { od = record { def = λ x → (m : Ordinal) → odef A x ∧ odef A m ∧ (¬ (* x < * m))} ; odmax = & A ; <odmax = {!!} } 154 HasMaximal = record { od = record { def = λ x → (m : Ordinal) → odef A x ∧ odef A m ∧ (¬ (* x < * m))} ; odmax = & A ; <odmax = {!!} }
155 z01 : {B a b : HOD} → TotalOrderSet B _<_ → B ∋ a → B ∋ b → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
156 z01 {B} {a} {b} Tri B∋a B∋b (case1 a=b) b<a with Tri (me B∋a) (me B∋b)
157 ... | tri< a₁ ¬b ¬c = ¬b a=b
158 ... | tri≈ ¬a b₁ ¬c = ¬c b<a
159 ... | tri> ¬a ¬b c = ¬b a=b
160 z01 {B} {a} {b} Tri B∋a B∋b (case2 a<b) b<a with Tri (me B∋a) (me B∋b)
161 ... | tri< a₁ ¬b ¬c = ¬c b<a
162 ... | tri≈ ¬a b₁ ¬c = ¬c b<a
163 ... | tri> ¬a ¬b c = ¬a a<b
140 ZChain→¬SUP : (z : ZChain A (& A) _<_ ) → ¬ (SUP A (ZChain.B z) _<_ ) 164 ZChain→¬SUP : (z : ZChain A (& A) _<_ ) → ¬ (SUP A (ZChain.B z) _<_ )
141 ZChain→¬SUP z sp = ⊥-elim {!!} 165 ZChain→¬SUP z sp = ⊥-elim {!!} where
142 zeron01 : {B a b : HOD} → TotalOrderSet B _<_ → B ∋ a → B ∋ b → (a ≡ b ) ∨ (a < b ) → b < a → ⊥ 166 z02 : (x : HOD) → ZChain.B z ∋ x → ⊥
143 zeron01 {B} {a} {b} Tri s t (case1 a=b) v = {!!} 167 z02 x xe = ( z01 (ZChain.total z) xe {!!} (SUP.x≤sup sp xe) {!!} )
144 -- with Tri s t | inspect (Tri s) t
145 -- ... | case1 x | [ eq ] = {!!}
146 -- ... | case2 (case1 x) | [ eq ] = {!!}
147 -- ... | case2 (case2 x) | [ eq ] = {!!}
148 zeron01 {B} {a} {b} Tri s t (case2 a<b) v = {!!}
149 -- with Tri s t | inspect (Tri s) t
150 ind : (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A y _<_ ) 168 ind : (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A y _<_ )
151 → ZChain A x _<_ 169 → ZChain A x _<_
152 ind x prev with Oprev-p x 170 ind x prev with Oprev-p x
153 ... | yes _ = {!!} 171 ... | yes _ = {!!}
154 ind x prev | no ¬ox with trio< (& A) x 172 ind x prev | no ¬ox with trio< (& A) x