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

changeset 889:450225f4d55d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
x≤supfx1 is no good
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Oct 2022 19:00:35 +0900
parents 49e0ab5e30e0
children 3eaf3b8b1009
files src/zorn.agda
diffstat 1 files changed, 31 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Oct 03 12:52:25 2022 +0900
+++ b/src/zorn.agda	Mon Oct 03 19:00:35 2022 +0900
@@ -395,7 +395,7 @@
       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 : {z : Ordinal } → z o≤ supf z
+      x≤supfx : {x : Ordinal } → x o≤ z → x o≤ supf x
 
       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) ))
@@ -830,7 +830,7 @@
           ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ ) 
 
           zc4 : ZChain A f mf ay x
-          zc4 with osuc-≡< (ZChain.x≤supfx zc )
+          zc4 with osuc-≡< (ZChain.x≤supfx zc o≤-refl )
           ... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1  
               ; x≤supfx = ? ; minsup = ? ; supf-is-sup = ? ; csupf = ?    }  where
 
@@ -1078,15 +1078,32 @@
                                   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 z
-                 x≤supfx1 {z} with trio< z ( supf1 z) --  supf1 x o< x → supf1 x o≤ supf1 px → x o< px ∨ supf1 x ≡ supf1 px
+                 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
-                 ... | tri> ¬a ¬b c with osuc-≡< (subst (λ k → supf1 x o< k ) (sym (Oprev.oprev=x op)) ? ) -- c : supf1 x < x     
-                 ... | case2 lt = ?
-                    -- ⊥-elim ( o<> (pxo<x op) (supf-inject0 supf-mono1 ( subst (λ k → supf1 x o< k ) 
-                    --  (trans sfpx=px (sym (sf1=sf0 o≤-refl))) lt )))  -- lt : supf1 x o< px ≡ supf0 px ≡ supf1 px
-                 ... | case1 eq = ? --   supf1 x ≡ px ≡ supf1 px
+                 ... | tri> ¬a ¬b c with trio< z px
+                 ... | tri< a ¬b ¬c = ZChain.x≤supfx zc (o<→≤ a)
+                 ... | tri≈ ¬a b ¬c = subst (λ k → k o< osuc px) (sym b) <-osuc
+                 ... | tri> ¬a ¬b lt = ⊥-elim ( o≤> sf04 c ) where --   c : sp1 o< z, lt : px o< z --  supf1 z ≡ sp1 -- supf1 z o< z
+                       z=x : z ≡ x 
+                       z=x with trio< z x
+                       ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ lt , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) a ⟫ )
+                       ... | tri≈ ¬a b ¬c = b
+                       ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤x c )
+                       sf01 : supf1 x ≡ sp1
+                       sf01 with trio< x px
+                       ... | tri< a ¬b ¬c = ⊥-elim ( ¬c (pxo<x op ))
+                       ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c (pxo<x op ))
+                       ... | tri> ¬a ¬b c = refl
+                       sf02 : supf1 px o≤ supf1 x
+                       sf02 = supf-mono1 (o<→≤ (pxo<x op ))
+                       sf00 : px o≤ sp1  --   supf1 px o≤ spuf1 x -- c : sp1 o< x
+                       sf00 = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl) (sym sfpx=px)) sf01 sf02
+                       sf04 : z o≤ sp1
+                       sf04 with osuc-≡< sf00
+                       ... | case1 eq = ? where --   sup of U px ≡ supf1 px ≡ supf1 x ≡ sp1 ≡ sup of U x
+                       ... | case2 lt = subst (λ k → k o≤ sp1 ) (trans (Oprev.oprev=x op) (sym z=x)) (osucc lt )
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
@@ -1110,19 +1127,19 @@
                         z1≤px : z1 o≤ px
                         z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) sfpx=px a ))
                  ... | tri≈ ¬a b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) zc20 (case2 (init apx sfpx=px )) where
-                      z1≤px : z1 o≤ px -- z1 o≤ supf1 z ≡ px 
-                      z1≤px = subst (λ k → z1 o< k) (cong osuc b ) ( ZChain.x≤supfx zc  )
+                      z1≤px : z1 o≤ px -- z1 o≤ supf1 z1 ≡ px 
+                      z1≤px = subst (λ k → z1 o< k) (sym (Oprev.oprev=x op)) (supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 o≤-refl ) ))
                       zc20 : supf0 px ≡ supf1 z1 
                       zc20 = begin
                         supf0 px  ≡⟨ sym sfpx=px ⟩
                         px  ≡⟨ sym b ⟩
                         supf0 z1  ≡⟨ sym (sf1=sf0 z1≤px)  ⟩
                         supf1 z1 ∎ where open ≡-Reasoning
-                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ zc20 , subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) where
+                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ zc21 , subst (λ k → z1 o< k ) (sym (Oprev.oprev=x op)) zc22 ⟫ ) where
                       zc21 : px o< z1
                       zc21 =  ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) sfpx=px c  )
-                      zc20 : px o< supf1 z1
-                      zc20 = ordtrans<-≤ zc21 x≤supfx1
+                      zc22 : z1 o< x -- c : px o< supf0 z1
+                      zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 o≤-refl ) )
                      -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x
 
           ... | case2 px<spfx = ? where