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

comparison src/zorn.agda @ 538:854908eb70f2

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 Sun, 24 Apr 2022 14:10:06 +0900
parents e12add1519ec
children adbac273d2a6
comparison
equal deleted inserted replaced
537:e12add1519ec 538:854908eb70f2
195 record ZChain ( A : HOD ) {x : Ordinal} (ax : A ∋ * x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) 195 record ZChain ( A : HOD ) {x : Ordinal} (ax : A ∋ * x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f )
196 (sup : (C : Ordinal ) → (* C ⊆ A) → IsTotalOrderSet (* C) → Ordinal) (z : Ordinal) : Set (Level.suc n) where 196 (sup : (C : Ordinal ) → (* C ⊆ A) → IsTotalOrderSet (* C) → Ordinal) (z : Ordinal) : Set (Level.suc n) where
197 field 197 field
198 chain : HOD 198 chain : HOD
199 chain⊆A : chain ⊆ A 199 chain⊆A : chain ⊆ A
200 chain∋x : odef chain x
200 f-total : IsTotalOrderSet chain 201 f-total : IsTotalOrderSet chain
201 f-next : {a : Ordinal } → odef chain a → odef chain (f a) 202 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
202 is-max : {a b : Ordinal } → (ca : odef chain a ) → odef A b → a o< z 203 is-max : {a b : Ordinal } → (ca : odef chain a ) → odef A b → a o< z
203 → ( Prev< A (incl chain⊆A (subst (λ k → odef chain k ) (sym &iso) ca)) f 204 → ( Prev< A (incl chain⊆A (subst (λ k → odef chain k ) (sym &iso) ca)) f
204 ∨ (sup (& chain) (subst (λ k → k ⊆ A) (sym *iso) chain⊆A) (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b )) 205 ∨ (sup (& chain) (subst (λ k → k ⊆ A) (sym *iso) chain⊆A) (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b ))
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) 238 ¬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)
238 cf : ¬ Maximal A → Ordinal → Ordinal 239 cf : ¬ Maximal A → Ordinal → Ordinal
239 cf nmx x with ODC.∋-p O A (* x) 240 cf nmx x with ODC.∋-p O A (* x)
240 ... | no _ = o∅ 241 ... | no _ = o∅
241 ... | yes ax with is-o∅ (& ( Gtx ax )) 242 ... | yes ax with is-o∅ (& ( Gtx ax ))
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 243 ... | yes nogt = -- no larger element, so it is maximal
244 ⊥-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 ⟫ )
243 ... | no not = & (ODC.minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))) 245 ... | 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) ) 246 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) 247 is-cf nmx {x} ax with ODC.∋-p O A (* x)
246 ... | no not = ⊥-elim ( not (subst (λ k → odef A k ) (sym &iso) ax )) 248 ... | no not = ⊥-elim ( not (subst (λ k → odef A k ) (sym &iso) ax ))
247 ... | yes ax with is-o∅ (& ( Gtx ax )) 249 ... | yes ax with is-o∅ (& ( Gtx ax ))
251 cf-is-<-monotonic nmx x ax = ⟪ proj2 (is-cf nmx ax ) , proj1 (is-cf nmx ax ) ⟫ 253 cf-is-<-monotonic nmx x ax = ⟪ proj2 (is-cf nmx ax ) , proj1 (is-cf nmx ax ) ⟫
252 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx ) 254 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx )
253 cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ 255 cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫
254 zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc : ZChain A sa f mf supO (& A)) → SUP A (ZChain.chain zc) 256 zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc : ZChain A sa f mf supO (& A)) → SUP A (ZChain.chain zc)
255 zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc ) 257 zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc )
256 -- zsup zc f mf = & ( SUP.sup (supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf ) ) )
257 A∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) 258 A∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A))
258 → A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )) 259 → A ∋ * ( & ( SUP.sup (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 ) ) 260 A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal (zsup (cf nmx) (cf-is-≤-monotonic nmx) 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 )) 261 sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf supO (& A)) → SUP A (* (& (ZChain.chain zc)))
261 z03 f mf zc = {!!} 262 sp0 f mf zc = supP (* (& (ZChain.chain zc))) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc))
263 (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc) )
264 z03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf supO (& A))
265 → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc ))
266 z03 f mf zc = z14 where
267 chain = ZChain.chain zc
268 sp1 = sp0 f mf zc
269 z10 : {a b : Ordinal } → (ca : odef chain a ) → odef A b → a o< (& A)
270 → ( Prev< A (incl (ZChain.chain⊆A zc) (subst (λ k → odef chain k ) (sym &iso) ca)) f
271 ∨ (supO (& chain) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc)) (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc)) ≡ b ))
272 → * a < * b → odef chain b
273 z10 = ZChain.is-max zc
274 z12 : odef chain (& (SUP.sup sp1))
275 z12 with o≡? (& s) (& (SUP.sup sp1))
276 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋x zc )
277 ... | no ne = z10 {& s} {& (SUP.sup sp1)} (ZChain.chain∋x zc) (SUP.A∋maximal sp1) (c<→o< (subst (λ k → odef A (& k) ) *iso sa) ) (case2 refl ) z13 where
278 z13 : * (& s) < * (& (SUP.sup sp1))
279 z13 with SUP.x<sup sp1 (subst (λ k → odef k (& s)) (sym *iso) ( ZChain.chain∋x zc ))
280 ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
281 ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
282 z14 : f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc))
283 z14 with IsStrictTotalOrder.compare (ZChain.f-total zc ) (me (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12))) (me z12 )
284 ... | tri< a ¬b ¬c = ⊥-elim z16 where
285 z16 : ⊥
286 z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
287 ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
288 ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
289 ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
290 ... | tri> ¬a ¬b c = ⊥-elim z17 where
291 c1 : SUP.sup sp1 < * (f ( & ( SUP.sup sp1 )))
292 c1 = c
293 z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1)
294 z15 = SUP.x<sup sp1 (subst₂ (λ j k → odef j k ) (sym *iso) (sym &iso) (ZChain.f-next zc z12) )
295 z17 : ⊥
296 z17 with z15
297 ... | case1 eq = ¬b eq
298 ... | case2 lt = ¬a lt
262 z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) → ⊥ 299 z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) → ⊥
263 z04 nmx zc = z01 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) 300 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 ))))) 301 (proj1 (is-cf nmx (SUP.A∋maximal sp1))))
265 (A∋zsup nmx zc ) (case1 ( cong (*)( z03 (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) 302 (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) ) (case1 ( cong (*)( z03 (cf nmx) (cf-is-≤-monotonic nmx ) zc )))
266 (proj1 (cf-is-<-monotonic nmx c ((subst λ k → odef A k ) &iso (A∋zsup nmx zc )))) where 303 (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where
267 c = & (SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc )) 304 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc
305 c = & (SUP.sup sp1)
268 -- ZChain is not compatible with the SUP condition 306 -- ZChain is not compatible with the SUP condition
269 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A sa f mf supO y ) 307 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A sa f mf supO y )
270 → ZChain A sa f mf supO x 308 → ZChain A sa f mf supO x
271 ind f mf x prev with Oprev-p x 309 ind f mf x prev with Oprev-p x
272 ... | yes op with ODC.∋-p O A (* x) 310 ... | yes op with ODC.∋-p O A (* x)