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

changeset 891:9fb948dac666

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
u < supf z
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 05 Oct 2022 13:13:35 +0900
parents 3eaf3b8b1009
children f331c8be2425
files src/zorn.agda
diffstat 1 files changed, 43 insertions(+), 37 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Oct 04 10:46:22 2022 +0900
+++ b/src/zorn.agda	Wed Oct 05 13:13:35 2022 +0900
@@ -395,10 +395,11 @@
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
-      x≤supfx : {x : Ordinal } → x o≤ supf z → x o≤ supf x
+      x≤supfx : {x : Ordinal } → x o≤ z → x o≤ supf x
+      supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
 
       minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x) 
-      supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (M→S supf (minsup x≤z) ))
+      supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
       csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
 
    chain : HOD
@@ -407,8 +408,7 @@
    chain⊆A = λ lt → proj1 lt
    sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x) 
    sup {x} x≤z = M→S supf (minsup x≤z) 
-   supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
-   supf-is-minsup {x} x≤z = trans (supf-is-sup x≤z) &iso
+   -- supf-sup<minsup : {x : Ordinal } → (x≤z : x o≤ z) → & (SUP.sup (M→S supf (minsup x≤z) )) o≤ supf x ... supf-mono
 
    chain∋init : odef chain y
    chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
@@ -442,16 +442,16 @@
    ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
    supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b)
-   supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) )
+   supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-minsup b≤z)) ( MinSUP.asm ( minsup b≤z ) )
 
    -- supf-idem : {x : Ordinal } → supf x o≤ z  → supf (supf x) ≡ supf x
    -- supf-idem {x} sx≤z = sup=u (supf∈A ?) sx≤z ?
 
    fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
-   fcy<sup  {u} {w} u≤z fc with SUP.x<sup (sup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
+   fcy<sup  {u} {w} u≤z fc with MinSUP.x<sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
-   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) ))
-   ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
+   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans ? (sym (supf-is-minsup u≤z ) ) ))
+   ... | case2 lt = case2 ? -- (subst (λ k → * w < k ) ? )-- (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-minsup u≤z ))) ) lt )
 
    -- ordering is not proved here but in ZChain1 
 
@@ -459,7 +459,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 ) →  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) b f ∨  IsSup A (UnionCF A f mf ay supf z) ab  
           → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
 
@@ -599,7 +599,7 @@
             → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
         chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) a≤b
         is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
-            b o< ZChain.supf zc x → (ab : odef A b) →
+            b o< x → (ab : odef A b) →
             HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f → 
             * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
         is-max-hp x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
@@ -641,13 +641,13 @@
                 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ 
         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)
         order {b} {s} {z1} b<z ss<sb fc = zc04 where
-          zc00 : ( * z1  ≡  SUP.sup (ZChain.sup zc (o<→≤ b<z) )) ∨ ( * z1  < SUP.sup ( ZChain.sup zc (o<→≤ b<z) ) )
-          zc00 = SUP.x<sup (ZChain.sup zc (o<→≤  b<z) ) (csupf-fc (o<→≤ b<z) ss<sb fc )
+          zc00 : ( z1  ≡  MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1  << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) )
+          zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤  b<z) ) ? -- (csupf-fc (o<→≤ b<z) ss<sb fc )
           -- supf (supf b) ≡ supf b
           zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
           zc04 with zc00
-          ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (ZChain.supf-is-sup zc (o<→≤ b<z))  ) (cong (&) eq) )
-          ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (ZChain.supf-is-sup zc (o<→≤ b<z) ) )))  lt )
+          ... | case1 eq = ? -- case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (ZChain.supf-is-minsup zc (o<→≤ b<z))  ) (cong (&) eq) )
+          ... | case2 lt = ? -- case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) ) )))  lt )
 
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x
@@ -656,13 +656,13 @@
            zc-b<x : {b : Ordinal } → b o< x → b o< osuc px
            zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
-              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) b f ∨ IsSup A (UnionCF A f mf ay supf x) 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 b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab P a<b | case2 is-sup 
-             = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
+             = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
               b<A : b o< & A
               b<A = z09 ab
               m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
@@ -680,17 +680,18 @@
               m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
-              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) b f ∨ IsSup A (UnionCF A f mf ay supf x) 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 b<x ab has-prev a<b 
            is-max {a} {b} ua b<x 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 = chain-mono1 ?
-             ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+           ... | case2 y<b = ⟪ ab , ch-is-sup b m10 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))
+              m10 : b o< ZChain.supf zc x
+              m10 = ordtrans<-≤ b<x ( ZChain.x≤supfx 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 
@@ -713,16 +714,19 @@
      fixpoint f mf zc = z14 where
            chain = ZChain.chain zc
            sp1 = sp0 f mf as0 zc 
-           z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< ZChain.supf zc (& A) → (ab : odef A b ) 
+           z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) 
               →  HasPrev A chain b f ∨  IsSup A chain {b} ab -- (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
               → * a < * b  → odef chain b
            z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
+           z21 : & (SUP.sup sp1) o< & A
+           z21 = c<→o< ( SUP.as sp1)
+           --  ZChain.supf zc (& A) o≤ & (SUP.sup sp1)  ( minimality )
            z11 : & (SUP.sup sp1) o< ZChain.supf zc (& A)
            z11 = ? -- c<→o< ( SUP.as sp1)
            z12 : odef chain (& (SUP.sup sp1))
            z12 with o≡? (& s) (& (SUP.sup sp1))
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z11 (SUP.as sp1)
+           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1)
                 (case2 z19 ) z13 where
                z13 :  * (& s) < * (& (SUP.sup sp1))
                z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc )
@@ -854,16 +858,16 @@
 
                  zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 (supf0 px) a → FClosure A f px b → a <= b
                  zc02 {a} {b} ca fb = zc05 fb where
-                    zc06 : & (SUP.sup (ZChain.sup zc o≤-refl)) ≡ px
-                    zc06 = trans (sym ( ZChain.supf-is-sup zc o≤-refl )) (sym sfpx=px)
+                    zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ px
+                    zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) (sym sfpx=px)
                     zc05 : {b : Ordinal } → FClosure A f px b → a <= b
                     zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc px f mf fb ))
                     ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb)
                     ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) 
-                    zc05 (init b1 refl) with SUP.x<sup (ZChain.sup zc o≤-refl) 
+                    zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) 
                              ? -- (subst (λ k → odef A k ∧ UChain A f mf ay supf0 ? k) (sym &iso) ca )
-                    ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 (cong (&) eq))
-                    ... | case2 lt = case2 (subst (λ k → (* a) < k ) (trans (sym *iso) (cong (*) zc06)) lt)
+                    ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 ? )-- (cong (&) eq))
+                    ... | case2 lt = case2 (subst (λ k → (* a) < k ) ? ? ) -- (trans (sym *iso) (cong (*) zc06)) lt)
 
                  ptotal : IsTotalOrderSet pchainpx
                  ptotal (case1 a) (case1 b) =  subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso 
@@ -1083,7 +1087,7 @@
                                   csupf17 (init as refl ) = ZChain.csupf zc sf<px 
                                   csupf17 (fsuc x fc) = ? -- ZChain.f-next zc ? -- (csupf17 fc)
 
-                 x≤supfx1 : {z : Ordinal} → z o≤ supf1 x → z o≤ supf1 z
+                 x≤supfx1 : {z : Ordinal} → z o≤ x → z o≤ supf1 z
                  x≤supfx1 {z} z≤x with trio< z (supf1 z) --  supf1 x o< x → supf1 x o≤ supf1 px → x o< px ∨ supf1 x ≡ supf1 px
                  ... | tri< a ¬b ¬c = o<→≤ a
                  ... | tri≈ ¬a b ¬c = o≤-refl0 b
@@ -1249,14 +1253,16 @@
                           zc13 : odef pchain z
                           zc13 = subst (λ k → odef pchain k) (trans (sym (HasPrev.x=fy hp)) zc14) ( ZChain.f-next zc (HasPrev.ay hp) )
                         zc20 {.(f w)} (fsuc w fc) = ZChain.f-next zc (zc20 fc)
+
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
-                         tsup : SUP A (UnionCF A f mf ay supf0 z)
-                         tsup=sup : supf0 z ≡ & (SUP.sup tsup ) 
+                         tsup : MinSUP A (UnionCF A f mf ay supf1 z)
+                         tsup=sup : supf1 z ≡ MinSUP.sup tsup 
+
                  sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
                  sup {z} z≤x with trio< z px 
-                 ... | tri< a ¬b ¬c = record { tsup = ZChain.sup zc (o<→≤ a)  ; tsup=sup = ZChain.supf-is-sup zc (o<→≤ a) }
-                 ... | tri≈ ¬a b ¬c = record { tsup = ZChain.sup zc (o≤-refl0 b)  ; tsup=sup = ZChain.supf-is-sup zc (o≤-refl0 b) }
+                 ... | tri< a ¬b ¬c = ? -- jrecord { tsup = ZChain.minsup zc (o<→≤ a)  ; tsup=sup = ZChain.supf-is-minsup zc (o<→≤ a) }
+                 ... | tri≈ ¬a b ¬c = ? -- record { tsup = ZChain.minsup zc (o≤-refl0 b)  ; tsup=sup = ZChain.supf-is-minsup zc (o≤-refl0 b) }
                  ... | tri> ¬a ¬b px<z = zc35 where
                      zc30 : z ≡ x
                      zc30 with osuc-≡< z≤x
@@ -1268,16 +1274,16 @@
                      ... | case1 lt = SUP.x<sup zc32 lt 
                      ... | case2 ⟪ spx=px  , fc ⟫ = ⊥-elim ( ne spx=px )
                      zc33 : supf0 z ≡ & (SUP.sup zc32)
-                     zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl  )
+                     zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-minsup zc o≤-refl  )
                      zc36 : ¬ (supf0 px ≡ px) → STMP z≤x
-                     zc36 ne = record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 ne } ; tsup=sup = zc33  } 
+                     zc36 ne = ? -- record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 ne } ; tsup=sup = zc33  } 
                      zc35 : STMP z≤x
                      zc35 with trio< (supf0 px) px
                      ... | tri< a ¬b ¬c = zc36 ¬b
                      ... | tri> ¬a ¬b c = zc36 ¬b
-                     ... | tri≈ ¬a b ¬c = record { tsup = zc37 ; tsup=sup = ?  } where
-                          zc37 : SUP A (UnionCF A f mf ay supf0 z)
-                          zc37 = record { sup = ? ; as = ? ; x<sup = ? }
+                     ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ?  } where
+                          zc37 : MinSUP A (UnionCF A f mf ay supf0 z)
+                          zc37 = record { sup = ? ; asm = ? ; x<sup = ? }
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
@@ -1380,7 +1386,7 @@
                  sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup {!!}))
                  sis {z} z≤x with trio< z x
                  ... | tri< a ¬b ¬c = {!!} where
-                     zc8 = ZChain.supf-is-sup (pzc z a) {!!}
+                     zc8 = ZChain.supf-is-minsup (pzc z a) {!!}
                  ... | tri≈ ¬a b ¬c = {!!}
                  ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) 
                  sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) b f ) → supf1 b ≡ b