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

changeset 765:7fff07748fde

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 Mon, 25 Jul 2022 18:13:43 +0900
parents bbf12d61143f
children e1c6c32efe01
files src/zorn.agda
diffstat 1 files changed, 37 insertions(+), 40 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jul 25 17:53:18 2022 +0900
+++ b/src/zorn.agda	Mon Jul 25 18:13:43 2022 +0900
@@ -55,6 +55,9 @@
 _<<_ : (x y : Ordinal ) → Set n    -- Set n order
 x << y = * x < * y
 
+_<=_ : (x y : Ordinal ) → Set n    -- Set n order
+x <= y = (x ≡ y ) ∨ ( * x < * y )
+
 POO : IsStrictPartialOrder _≡_ _<<_ 
 POO = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans } 
    ; trans = IsStrictPartialOrder.trans PO 
@@ -260,8 +263,8 @@
    field
       csupz    : FClosure A f (supf u) z 
       supfu=u  : supf u ≡ u 
-      fcy<sup  : {z : Ordinal } → FClosure A f y z → z << supf u   -- not a initial chain
-      order    : {sup1 z1 : Ordinal} → (lt : sup1 o< u ) → FClosure A f (supf sup1 ) z1 → z1 << supf u
+      fcy<sup  : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u ) 
+      order    : {sup1 z1 : Ordinal} → (lt : sup1 o< u ) → FClosure A f (supf sup1 ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
 
 -- Union of supf z which o< x
 --
@@ -295,8 +298,8 @@
 
       csupf : {z : Ordinal } → odef chain (supf z) 
       sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
-      fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → w << supf u     -- different from order because y o< supf 
-      order : {b sup1 z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f (supf sup1) z1 → z1 << supf b
+      fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
+      order : {b sup1 z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
 
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
@@ -319,32 +322,40 @@
 chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
      ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
      ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb
-     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
+     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub supb fcb) with ChainP.fcy<sup supb fca
+     ... | case1 eq = ?
+     ... | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
           ct00 : * a < * (supf ub)
-          ct00 = ChainP.fcy<sup supb fca
+          ct00 = lt
           ct01 : * a < * b 
           ct01 with s≤fc (supf ub) f mf fcb
           ... | case1 eq =  subst (λ k → * a < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-init fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
+     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb
+     ... | case1 eq = ?
+     ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
           ct00 : * b < * (supf ua)
-          ct00 = ChainP.fcy<sup supa fcb
+          ct00 = lt
           ct01 : * b < * a 
           ct01 with s≤fc (supf ua) f mf fca
           ... | case1 eq =  subst (λ k → * b < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
      ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) with trio< ua ub
-     ... | tri< a₁ ¬b ¬c = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
+     ... | tri< a₁ ¬b ¬c with ChainP.order supb  a₁ (ChainP.csupz supa)
+     ... | case1 eq = ?
+     ... | case2 lt = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
           ct03 : * a < * (supf ub)
-          ct03 = ChainP.order supb  a₁ (ChainP.csupz supa)
+          ct03 = lt
           ct02 : * a < * b 
           ct02 with s≤fc (supf ub) f mf fcb
           ... | case1 eq =  subst (λ k → * a < k ) eq ct03
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
-     ... | tri≈ ¬a  refl ¬c = fcn-cmp (supf ua) f mf fca fcb
-     ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
+     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri≈ ¬a  refl ¬c = fcn-cmp (supf ua) f mf fca fcb
+     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri> ¬a ¬b c with ChainP.order supa c (ChainP.csupz supb)
+     ... | case1 eq = ?
+     ... | case2 lt = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
           ct05 : * b < * (supf ua)
-          ct05 = ChainP.order supa c (ChainP.csupz supb)
+          ct05 = lt
           ct04 : * b < * a 
           ct04 with s≤fc (supf ua) f mf fca
           ... | case1 eq =  subst (λ k → * b < k ) eq ct05
@@ -469,7 +480,7 @@
                     ... | ch-is-sup u is-sup-a fc with trio< u px
                     ... | tri< a ¬b ¬c    = ⟪ proj1 ua , ch-is-sup u  is-sup-a fc ⟫ -- u o< osuc x
                     ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u  is-sup-a fc ⟫
-                    ... | tri> ¬a ¬b c = ⊥-elim (<-irr u≤a (ptrans a<b b<u) ) where
+                    ... | tri> ¬a ¬b c = ⊥-elim (<-irr u≤a (ptrans a<b ? ) ) where
                          --  a and b is a sup of chain, order forces minimulity of sup
                          su=u : ZChain.supf zc u ≡ u
                          su=u = ChainP.supfu=u is-sup-a 
@@ -482,8 +493,8 @@
                          fcb : FClosure A f (ZChain.supf zc b) b
                          fcb = subst (λ k → FClosure A f k b ) (sym (ZChain.sup=u zc ab (z09 ab) 
                             (record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x m07 o≤-refl lt)  } ) )) ( init ab )
-                         b<u : b << u
-                         b<u = subst (λ k → b << k ) su=u ( ZChain.order zc u<A (ordtrans b<px c)  fcb )
+                         b<u : b <= u
+                         b<u = subst (λ k → b <= k ) su=u ( ZChain.order zc u<A (ordtrans b<px c)  fcb )
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
                          (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
@@ -493,9 +504,9 @@
                     m05 : b ≡ ZChain.supf zc b
                     m05 = sym ( ZChain.sup=u zc ab (z09 ab) 
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono2 x (osucc b<x) o≤-refl uz )  }  )
-                    m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z << ZChain.supf zc b
+                    m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
                     m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
-                    m09 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
+                    m09 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
                     m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
                     m06 : ChainP A f mf ay (ZChain.supf zc) b b
                     m06 = record { csupz = subst (λ k → FClosure A f k b) m05 (init ab) ; supfu=u = sym m05 
@@ -512,9 +523,9 @@
            ... | case2 y<b = chain-mono2 x (o<→≤ (ob<x lim b<x) ) o≤-refl m04 where
                  m09 : b o< & A
                  m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
-                 m07 : {z : Ordinal} → FClosure A f y z → z << ZChain.supf zc b
+                 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
                  m07 {z} fc = ZChain.fcy<sup zc m09 fc
-                 m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
+                 m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
                  m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
                  m05 : b ≡ ZChain.supf zc b
                  m05 = sym (ZChain.sup=u zc ab m09
@@ -607,10 +618,7 @@
       ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
           spi =  & (SUP.sup (ysup f mf ay))
           isupf : Ordinal → Ordinal
-          isupf z with trio< z spi
-          ... | tri< a ¬b ¬c = y
-          ... | tri≈ ¬a b ¬c = spi
-          ... | tri> ¬a ¬b c = spi
+          isupf z = spi
           sp = ysup f mf ay
           cy : odef (UnionCF A f mf ay isupf o∅) y
           cy = ⟪ ay , ch-init (init ay)  ⟫
@@ -630,18 +638,7 @@
                uz01 = chain-total A f mf ay isupf (proj2 ca) (proj2 cb)  
 
           csupf : {z : Ordinal} → odef (UnionCF A f mf ay isupf o∅) (isupf z)
-          csupf {z} with trio< z spi
-          ... | tri< a ¬b ¬c = ⟪ ay , ch-init (init ay ) ⟫ 
-          ... | tri≈ ¬a b ¬c = ?
-          ... | tri> ¬a ¬b c = ⟪ SUP.A∋maximal sp   , ch-is-sup spi ? ? ⟫ where
-               uz03 : {z : Ordinal} → FClosure A f y z → z << isupf spi
-               uz03 {z} fcz with SUP.x<sup sp (subst (λ k → FClosure A f y k) (sym &iso) fcz) 
-               ... | case2 lt = ? -- subst (λ k → * z < k ) (sym *iso) lt
-               ... | case1 eq = ? -- ⊥-elim (<-irr (case1 e)
-               uz04 : {sup1 z1 : Ordinal} → sup1 o< spi → FClosure A f (isupf sup1) z1 → z1 << isupf spi
-               uz04 {_} {z} _ fcz = ?
-               uz02 : ChainP A f mf ay isupf spi spi
-               uz02 = ? -- record { csupz = init (SUP.A∋maximal sp) ; supfu=u = refl ; fcy<sup = uz03 ; order = uz04 }
+          csupf {z} = ?
 
      --
      -- create all ZChains under o< x
@@ -676,8 +673,8 @@
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
-          ... | ch-is-sup u is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
-               zc7 : y << (ZChain.supf zc) u 
+          ... | ch-is-sup u is-sup fc = ≤-ftrans ? (s≤fc _ f mf fc)  where
+               zc7 : y <= (ZChain.supf zc) u 
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
           pcy = ⟪ ay , ch-init (init ay)    ⟫
@@ -793,8 +790,8 @@
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
-          ... | ch-is-sup u is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
-               zc7 : y << psupf _
+          ... | ch-is-sup u is-sup fc = ≤-ftrans ? (s≤fc _ f mf fc)  where
+               zc7 : y <= psupf _
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
           pcy = ⟪ ay , ch-init (init ay)    ⟫