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

changeset 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
files src/OrdUtil.agda src/zorn.agda
diffstat 2 files changed, 52 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/OrdUtil.agda	Sun Apr 24 08:04:42 2022 +0900
+++ b/src/OrdUtil.agda	Sun Apr 24 14:10:06 2022 +0900
@@ -65,6 +65,12 @@
 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy
 proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy 
 
+o≡? : (x y : Ordinal) → Dec ( x ≡ y )
+o≡? x y with trio< x y
+... | tri< a ¬b ¬c = no ¬b
+... | tri≈ ¬a b ¬c = yes b
+... | tri> ¬a ¬b c = no ¬b
+
 _o≤_ :  Ordinal → Ordinal → Set  n
 a o≤ b  = a o< osuc b -- (a ≡ b)  ∨ ( a o< b )
 
--- a/src/zorn.agda	Sun Apr 24 08:04:42 2022 +0900
+++ b/src/zorn.agda	Sun Apr 24 14:10:06 2022 +0900
@@ -197,6 +197,7 @@
    field
       chain : HOD
       chain⊆A : chain ⊆ A
+      chain∋x : odef chain x
       f-total : IsTotalOrderSet chain 
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       is-max :  {a b : Ordinal } → (ca : odef chain a ) → odef A b → a o< z
@@ -239,7 +240,8 @@
      cf  nmx x with ODC.∋-p O A (* x)
      ... | no _ = o∅
      ... | yes ax with is-o∅ (& ( Gtx ax ))
-     ... | 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
+     ... | yes nogt = -- no larger element, so it is maximal
+         ⊥-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 not =  & (ODC.minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq)))
      is-cf : (nmx : ¬ Maximal A ) → {x : Ordinal} → odef A x → odef A (cf nmx x) ∧ ( * x < * (cf nmx x) )
      is-cf nmx {x} ax with ODC.∋-p O A (* x)
@@ -253,18 +255,54 @@
      cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
      zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc : ZChain A sa f mf supO (& A)) → SUP A  (ZChain.chain zc) 
      zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc  )   
-     -- zsup zc f mf = & ( SUP.sup (supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf )  ) )
      A∋zsup :  (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) 
         →  A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) ))
      A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal  (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )
-     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 ))
-     z03 f mf zc = {!!}
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf supO (& A)) → SUP A (* (& (ZChain.chain zc)))
+     sp0 f mf zc = supP (* (& (ZChain.chain zc))) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc))
+               (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc) )
+     z03 :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf supO (& A))
+            → f (& (SUP.sup (sp0 f mf zc  ))) ≡ & (SUP.sup (sp0 f mf zc  ))
+     z03 f mf zc = z14 where
+           chain = ZChain.chain zc
+           sp1 = sp0 f mf zc
+           z10 :  {a b : Ordinal } → (ca : odef chain a ) → odef A b → a o< (& A)
+              → ( Prev< A (incl (ZChain.chain⊆A zc)  (subst (λ k → odef chain k ) (sym &iso) ca)) f
+                   ∨ (supO (& chain) (subst (λ k → k  ⊆ A) (sym *iso) (ZChain.chain⊆A zc))  (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc)) ≡ b ))
+              → * a < * b  → odef chain b
+           z10 = ZChain.is-max zc
+           z12 : odef chain (& (SUP.sup sp1))
+           z12 with o≡? (& s) (& (SUP.sup sp1))
+           ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋x zc )
+           ... | 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
+               z13 :  * (& s) < * (& (SUP.sup sp1))
+               z13 with SUP.x<sup sp1 (subst (λ k → odef k (& s)) (sym *iso) ( ZChain.chain∋x zc ))
+               ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
+               ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
+           z14 :  f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc))
+           z14 with IsStrictTotalOrder.compare (ZChain.f-total zc ) (me (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12))) (me z12 )
+           ... | tri< a ¬b ¬c = ⊥-elim z16 where
+               z16 : ⊥
+               z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
+               ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
+               ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
+           ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
+           ... | tri> ¬a ¬b c = ⊥-elim z17 where
+               c1 : SUP.sup sp1 < * (f ( & ( SUP.sup sp1 ))) 
+               c1 = c
+               z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) <  SUP.sup sp1)
+               z15  = SUP.x<sup sp1 (subst₂ (λ j k → odef j k ) (sym *iso) (sym &iso)  (ZChain.f-next zc z12) )
+               z17 : ⊥
+               z17 with z15
+               ... | case1 eq = ¬b eq
+               ... | case2 lt = ¬a lt
      z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) → ⊥
      z04 nmx zc = z01  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso)
-           (proj1 (is-cf nmx (SUP.A∋maximal  (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc )))))
-           (A∋zsup nmx zc ) (case1 ( cong (*)( z03 (cf nmx) (cf-is-≤-monotonic nmx ) zc )))
-           (proj1 (cf-is-<-monotonic nmx c ((subst λ k → odef A k ) &iso (A∋zsup nmx zc )))) where
-          c = & (SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ))
+           (proj1 (is-cf nmx (SUP.A∋maximal  sp1))))
+           (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) ) (case1 ( cong (*)( z03 (cf nmx) (cf-is-≤-monotonic nmx ) zc )))
+           (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where
+          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc 
+          c = & (SUP.sup sp1)
      -- ZChain is not compatible with the SUP condition
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A sa f mf supO y )
          →  ZChain A sa f mf supO x