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

changeset 976:8fe873f0c88e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
is-max condition have to be b o< x
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 08 Nov 2022 18:29:35 +0900
parents 1e88cce74699
children f0d2666fe3b2
files src/zorn.agda
diffstat 1 files changed, 12 insertions(+), 66 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Nov 08 11:26:59 2022 +0900
+++ b/src/zorn.agda	Tue Nov 08 18:29:35 2022 +0900
@@ -524,7 +524,7 @@
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    supf = ZChain.supf zc
    field
-      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → supf b o< supf z  → (ab : odef A b)
+      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< z  → (ab : odef A b)
           → HasPrev A (UnionCF A f mf ay supf z) f b ∨  IsSUP A (UnionCF A f mf ay supf b) ab
           → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
       order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
@@ -699,17 +699,17 @@
            zc-b<x : {b : Ordinal } → ZChain.supf zc b o< ZChain.supf zc x → b o< osuc px
            zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt  )
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
-              ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
+              b o< x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
               * a < * b → odef (UnionCF A f mf ay supf x) b
            is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
            is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
-           is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup
+           is-max {a} {b} ua b<x ab P a<b | case2 is-sup
              = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
               b<A : b o< & A
               b<A = z09 ab
-              b<x : b o< x
-              b<x  = ZChain.supf-inject zc sb<sx
+              sb<sx : supf b o< supf x
+              sb<sx = ?
               m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
               m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                     chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
@@ -724,18 +724,18 @@
               m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
         ... | no lim = record { is-max = is-max ; order = order }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
-              ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
+              b o< x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
               * a < * b → odef (UnionCF A f mf ay supf x) b
            is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P
            is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
            is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
            ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
-           ... | case2 y<b = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+           ... | case2 y<b = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
               m09 : b o< & A
               m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
               b<x : b o< x
-              b<x  = ZChain.supf-inject zc sb<sx
+              b<x  = ZChain.supf-inject zc ?
               m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
               m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
               m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
@@ -1477,16 +1477,15 @@
 
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
             → (sp1 : MinSUP A (ZChain.chain zc))
-            → (ssp<as :  ZChain.supf zc (MinSUP.sup sp1) o< ZChain.supf zc (& A))
             → f (MinSUP.sup sp1)  ≡ MinSUP.sup sp1
-     fixpoint f mf zc sp1 ssp<as = z14 where
+     fixpoint f mf zc sp1 = z14 where
            chain = ZChain.chain zc
            supf = ZChain.supf zc
            sp : Ordinal
            sp = MinSUP.sup sp1
            asp : odef A sp
            asp = MinSUP.asm sp1
-           z10 :  {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b )
+           z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b )
               →  HasPrev A chain f b  ∨  IsSUP A (UnionCF A f mf as0 (ZChain.supf zc) b) ab
               → * a < * b  → odef chain b
            z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
@@ -1495,7 +1494,7 @@
            z12 : odef chain sp
            z12 with o≡? (& s) sp
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-           ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp (case2 z19 ) z13 where
+           ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) z22 asp (case2 z19 ) z13 where
                z13 :  * (& s) < * sp
                z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne eq )
@@ -1544,7 +1543,7 @@
      z04 nmx zc = <-irr0  {* (cf nmx a)} {* a}
            (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.asm  asup ))))
            (subst (λ k → odef A k) (sym &iso) (MinSUP.asm asup) )
-           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc asup sa<sa ))) -- x ≡ f x ̄
+           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc asup ))) -- x ≡ f x ̄
                 (proj1 (cf-is-<-monotonic nmx a (MinSUP.asm asup ))) where                 -- x < f x
 
           supf = ZChain.supf zc
@@ -1554,59 +1553,6 @@
           a = MinSUP.sup asup
           a<A : a o< & A
           a<A =  ∈∧P→o< ⟪ MinSUP.asm asup , lift true ⟫
-          
-          csup : MinSUP  A (UnionCF A (cf nmx)  (cf-is-≤-monotonic nmx) as0 supf a)
-          csup = ZChain.minsup zc (o<→≤ a<A)
-          c : Ordinal
-          c = MinSUP.sup csup
-          ac : odef A c
-          ac = ?
-          sfc=c : supf a ≡ c
-          sfc=c = ZChain.supf-is-minsup zc (o<→≤ a<A)
-          c<A : c o< & A
-          c<A =  ∈∧P→o< ⟪ MinSUP.asm csup , lift true ⟫
-
-          dsup : MinSUP  A (UnionCF A (cf nmx)  (cf-is-≤-monotonic nmx) as0 supf c)
-          dsup = ZChain.minsup zc (o<→≤ c<A)
-          d : Ordinal
-          d = MinSUP.sup dsup
-          ad : odef A d
-          ad = ?
-          sfc=d : supf c ≡ d
-          sfc=d = ZChain.supf-is-minsup zc (o<→≤ c<A)
-          d<A : d o< & A
-          d<A =  ∈∧P→o< ⟪ MinSUP.asm dsup , lift true ⟫
-
-          zc40 : uchain (cf nmx)  (cf-is-≤-monotonic nmx) ac  ⊆' UnionCF A (cf nmx)  (cf-is-≤-monotonic nmx) as0 supf d
-          zc40 = ?
-
-          sc<<d : {mc : Ordinal } → (asc : odef A (supf mc)) → (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc ))
-             → supf mc << MinSUP.sup spd
-          sc<<d {mc} asc spd = z25 where
-                d1 :  Ordinal
-                d1 = MinSUP.sup spd -- supf d1 ≡ d
-                z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 )
-                z24 = MinSUP.x≤sup spd (init asc refl)
-                --
-                --   f ( f .. ( supf mc ) <= d1
-                --   f d1 <= d1
-                --
-                z25 : supf mc << d1
-                z25 with z24
-                ... | case2 lt = lt
-                ... | case1 eq = ⊥-elim ( <-irr z29 (proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) ) )  where
-                    --  supf mc ≡ d1
-                    z32 : ((cf nmx (supf mc)) ≡ d1) ∨ ( (cf nmx (supf mc)) << d1 )
-                    z32 = MinSUP.x≤sup spd (fsuc _ (init asc refl))
-                    z29 :  (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
-                    z29  with z32
-                    ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1)  )
-                    ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt)
-
-          --   supf a ≡  c o< d ≡ supf c o≤ supf (& A)
-
-          sa<sa : supf a o< supf (& A)
-          sa<sa = ?
 
      zorn00 : Maximal A
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM