Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 537:e12add1519ec
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 24 Apr 2022 08:04:42 +0900 |
parents | c43375ade2c5 |
children | 854908eb70f2 |
comparison
equal
deleted
inserted
replaced
536:c43375ade2c5 | 537:e12add1519ec |
---|---|
92 A∋x-irr A {x} {y} refl = refl | 92 A∋x-irr A {x} {y} refl = refl |
93 | 93 |
94 me-elm-refl : (A : HOD) → (x : Element A) → elm (me {A} (d→∋ A (is-elm x))) ≡ elm x | 94 me-elm-refl : (A : HOD) → (x : Element A) → elm (me {A} (d→∋ A (is-elm x))) ≡ elm x |
95 me-elm-refl A record { elm = ex ; is-elm = ax } = *iso | 95 me-elm-refl A record { elm = ex ; is-elm = ax } = *iso |
96 | 96 |
97 -- <-induction : (A : HOD) { ψ : (x : HOD) → A ∋ x → Set (Level.suc n)} | |
98 -- → IsPartialOrderSet A | |
99 -- → ( {x : HOD } → A ∋ x → ({ y : HOD } → A ∋ y → y < x → ψ y ) → ψ x ) | |
100 -- → {x0 x : HOD } → A ∋ x0 → A ∋ x → x0 < x → ψ x | |
101 -- <-induction A {ψ} PO ind ax0 ax x0<a = subst (λ k → ψ k ) *iso (<-induction-ord (osuc (& x)) <-osuc ) where | |
102 -- -- y < * ox → & y o< ox | |
103 -- induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox) | |
104 -- induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) {!!})) | |
105 -- <-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy) | |
106 -- <-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy | |
107 | |
108 | |
97 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) | 109 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
98 | 110 |
99 -- Don't use Element other than Order, you'll be in a trouble | 111 -- Don't use Element other than Order, you'll be in a trouble |
100 -- postulate -- may be proved by transfinite induction and functional extentionality | 112 -- postulate -- may be proved by transfinite induction and functional extentionality |
101 -- ∋x-irr : (A : HOD) {x y : HOD} → x ≡ y → (ax : A ∋ x) (ay : A ∋ y ) → ax ≅ ay | 113 -- ∋x-irr : (A : HOD) {x y : HOD} → x ≡ y → (ax : A ∋ x) (ay : A ∋ y ) → ax ≅ ay |
202 supO C C⊆A TC = & ( SUP.sup ( supP (* C) C⊆A TC )) | 214 supO C C⊆A TC = & ( SUP.sup ( supP (* C) C⊆A TC )) |
203 z01 : {a b : HOD} → A ∋ a → A ∋ b → (a ≡ b ) ∨ (a < b ) → b < a → ⊥ | 215 z01 : {a b : HOD} → A ∋ a → A ∋ b → (a ≡ b ) ∨ (a < b ) → b < a → ⊥ |
204 z01 {a} {b} A∋a A∋b (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋a} (sym a=b) b<a | 216 z01 {a} {b} A∋a A∋b (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋a} (sym a=b) b<a |
205 z01 {a} {b} A∋a A∋b (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋b} refl | 217 z01 {a} {b} A∋a A∋b (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋b} refl |
206 (IsStrictPartialOrder.trans PO {me A∋b} {me A∋a} {me A∋b} b<a a<b) | 218 (IsStrictPartialOrder.trans PO {me A∋b} {me A∋a} {me A∋b} b<a a<b) |
219 z07 : {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A | |
220 z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p ))) | |
207 s : HOD | 221 s : HOD |
208 s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) | 222 s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) |
209 sa : A ∋ * ( & s ) | 223 sa : A ∋ * ( & s ) |
210 sa = subst (λ k → odef A (& k) ) (sym *iso) ( ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) ) | 224 sa = subst (λ k → odef A (& k) ) (sym *iso) ( ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) ) |
211 HasMaximal : HOD | 225 HasMaximal : HOD |
212 HasMaximal = record { od = record { def = λ x → odef A x ∧ ( (m : Ordinal) → odef A m → ¬ (* x < * m)) } ; odmax = & A ; <odmax = z07 } where | 226 HasMaximal = record { od = record { def = λ x → odef A x ∧ ( (m : Ordinal) → odef A m → ¬ (* x < * m)) } ; odmax = & A ; <odmax = z07 } |
213 z07 : {y : Ordinal} → odef A y ∧ ((m : Ordinal) → odef A m → ¬ (* y < * m)) → y o< & A | 227 no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → odef A x ∧ ((m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m) )) → ⊥ |
214 z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p ))) | 228 no-maximum nomx x P = ¬x<0 (eq→ nomx {x} ⟪ proj1 P , (λ m ma p → proj2 ( proj2 P m ma ) p ) ⟫ ) |
215 no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → ((m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m) )) → ⊥ | |
216 no-maximum nomx x P = ¬x<0 (eq→ nomx {x} {!!} ) | |
217 Gtx : { x : HOD} → A ∋ x → HOD | 229 Gtx : { x : HOD} → A ∋ x → HOD |
218 Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = {!!} } | 230 Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = z07 } |
231 z08 : ¬ Maximal A → HasMaximal =h= od∅ | |
232 z08 nmx = record { eq→ = λ {x} lt → ⊥-elim ( nmx record {maximal = * x ; A∋maximal = subst (λ k → odef A k) (sym &iso) (proj1 lt) | |
233 ; ¬maximal<x = λ {y} ay → subst (λ k → ¬ (* x < k)) *iso (proj2 lt (& y) ay) } ) ; eq← = λ {y} lt → ⊥-elim ( ¬x<0 lt )} | |
234 x-is-maximal : ¬ Maximal A → {x : Ordinal} → (ax : odef A x) → & (Gtx (subst (λ k → odef A k ) (sym &iso) ax)) ≡ o∅ → (m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m)) | |
235 x-is-maximal nmx {x} ax nogt m am = ⟪ subst (λ k → odef A k) &iso (subst (λ k → odef A k ) (sym &iso) ax) , ¬x<m ⟫ where | |
236 ¬x<m : ¬ (* x < * m) | |
237 ¬x<m x<m = ∅< {Gtx (subst (λ k → odef A k ) (sym &iso) ax)} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫ (≡o∅→=od∅ nogt) | |
219 cf : ¬ Maximal A → Ordinal → Ordinal | 238 cf : ¬ Maximal A → Ordinal → Ordinal |
220 cf nmx x with ODC.∋-p O A (* x) | 239 cf nmx x with ODC.∋-p O A (* x) |
221 ... | no _ = o∅ | 240 ... | no _ = o∅ |
222 ... | yes ax with is-o∅ (& ( Gtx ax )) | 241 ... | yes ax with is-o∅ (& ( Gtx ax )) |
223 ... | yes nogt = ⊥-elim (no-maximum (≡o∅→=od∅ {!!} ) x x-is-maximal ) where -- no larger element, so it is maximal | 242 ... | yes nogt = ⊥-elim (no-maximum (z08 nmx) x ⟪ subst (λ k → odef A k) &iso ax , x-is-maximal nmx (subst (λ k → odef A k ) &iso ax) nogt ⟫ ) -- no larger element, so it is maximal |
224 x-is-maximal : (m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m)) | |
225 x-is-maximal m am = ⟪ subst (λ k → odef A k) &iso ax , ¬x<m ⟫ where | |
226 ¬x<m : ¬ (* x < * m) | |
227 ¬x<m x<m = ∅< {Gtx ax} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫ (≡o∅→=od∅ nogt) | |
228 ... | no not = & (ODC.minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))) | 243 ... | no not = & (ODC.minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))) |
244 is-cf : (nmx : ¬ Maximal A ) → {x : Ordinal} → odef A x → odef A (cf nmx x) ∧ ( * x < * (cf nmx x) ) | |
245 is-cf nmx {x} ax with ODC.∋-p O A (* x) | |
246 ... | no not = ⊥-elim ( not (subst (λ k → odef A k ) (sym &iso) ax )) | |
247 ... | yes ax with is-o∅ (& ( Gtx ax )) | |
248 ... | yes nogt = ⊥-elim (no-maximum (z08 nmx) x ⟪ subst (λ k → odef A k) &iso ax , x-is-maximal nmx (subst (λ k → odef A k ) &iso ax) nogt ⟫ ) | |
249 ... | no not = ODC.x∋minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq)) | |
229 cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) → odef A x → ( * x < * (cf nmx x) ) ∧ odef A (cf nmx x ) | 250 cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) → odef A x → ( * x < * (cf nmx x) ) ∧ odef A (cf nmx x ) |
230 cf-is-<-monotonic nmx x ax = ⟪ {!!} , {!!} ⟫ | 251 cf-is-<-monotonic nmx x ax = ⟪ proj2 (is-cf nmx ax ) , proj1 (is-cf nmx ax ) ⟫ |
231 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx ) | 252 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx ) |
232 cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ | 253 cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ |
233 zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc : ZChain A sa f mf supO (& A)) → SUP A (ZChain.chain zc) | 254 zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc : ZChain A sa f mf supO (& A)) → SUP A (ZChain.chain zc) |
234 zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc ) | 255 zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc ) |
235 -- zsup zc f mf = & ( SUP.sup (supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf ) ) ) | 256 -- zsup zc f mf = & ( SUP.sup (supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf ) ) ) |
236 A∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) | 257 A∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) |
237 → A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )) | 258 → A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )) |
238 A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) ) | 259 A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) ) |
239 z03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf supO (& A)) → f (& ( SUP.sup (zsup f mf zc ))) ≡ & (SUP.sup (zsup f mf zc )) | 260 z03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf supO (& A)) → f (& ( SUP.sup (zsup f mf zc ))) ≡ & (SUP.sup (zsup f mf zc )) |
240 z03 = {!!} | 261 z03 f mf zc = {!!} |
241 z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) → ⊥ | 262 z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) → ⊥ |
242 z04 nmx zc = z01 {* (cf nmx c)} {* c} {!!} (A∋zsup nmx zc ) (case1 ( cong (*)( z03 (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) | 263 z04 nmx zc = z01 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) |
264 (proj1 (is-cf nmx (SUP.A∋maximal (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ))))) | |
265 (A∋zsup nmx zc ) (case1 ( cong (*)( z03 (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) | |
243 (proj1 (cf-is-<-monotonic nmx c ((subst λ k → odef A k ) &iso (A∋zsup nmx zc )))) where | 266 (proj1 (cf-is-<-monotonic nmx c ((subst λ k → odef A k ) &iso (A∋zsup nmx zc )))) where |
244 c = & (SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc )) | 267 c = & (SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc )) |
245 -- ZChain is not compatible with the SUP condition | 268 -- ZChain is not compatible with the SUP condition |
246 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A sa f mf supO y ) | 269 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A sa f mf supO y ) |
247 → ZChain A sa f mf supO x | 270 → ZChain A sa f mf supO x |