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

changeset 714:e1ef5e6961ce

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 Fri, 15 Jul 2022 12:35:59 +0900
parents 55e82405ec0d
children e4587714c376
files src/zorn.agda
diffstat 1 files changed, 62 insertions(+), 30 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Jul 15 10:33:55 2022 +0900
+++ b/src/zorn.agda	Fri Jul 15 12:35:59 2022 +0900
@@ -95,6 +95,10 @@
 A∋fc {A} s f mf (init as) = as
 A∋fc {A} s f mf (fsuc y fcy) = proj2 (mf y ( A∋fc {A} s  f mf fcy ) )
 
+A∋fcs : {A : HOD} (s : Ordinal) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → odef A s
+A∋fcs {A} s f mf (init as) = as
+A∋fcs {A} s f mf (fsuc y fcy) = A∋fcs {A} s f mf fcy 
+
 s≤fc : {A : HOD} (s : Ordinal ) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → * s ≤ * y
 s≤fc {A} s {.s} f mf (init x) = case1 refl
 s≤fc {A} s {.(f x)} f mf (fsuc x fcy) with proj1 (mf x (A∋fc s f mf fcy ) )
@@ -244,13 +248,14 @@
 --    minimum index is y not ϕ 
 --
 
-record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (sup z : Ordinal) : Set n where
+record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u z : Ordinal) : Set n where
    field
       y-init   : supf o∅  ≡ y
+      au       : odef A u
       asup     : (x : Ordinal) → odef A (supf x)
-      fcy<sup  : {z : Ordinal } → FClosure A f y z → z << supf sup
-      csupz    : FClosure A f (supf sup) z 
-      order    : {sup1 z1 : Ordinal} → (lt : sup1 o< sup ) → FClosure A f (supf sup1 ) z1 → z1 << supf sup
+      fcy<sup  : {z : Ordinal } → FClosure A f y z → z << supf u
+      csupz    : FClosure A f (supf u) z 
+      order    : {sup1 z1 : Ordinal} → (lt : sup1 o< u ) → FClosure A f (supf sup1 ) z1 → z1 << supf u
 
 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) : Ordinal →  Ordinal → Set n where
     ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay supf o∅ z 
@@ -340,7 +345,7 @@
 
 ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
    → {x z : Ordinal } →  ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z )
-ChainP-next A f mf {y} ay supf {x} {z} cp = record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp 
+ChainP-next A f mf {y} ay supf {x} {z} cp = record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp  ; au = ChainP.au cp
      ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
 
 Zorn-lemma : { A : HOD } 
@@ -489,12 +494,8 @@
             b o< o∅ → (ab : odef A b) →
             HasPrev A (UnionCF A f mf ay isupf o∅) ab f ∨ IsSup A (UnionCF A f mf ay isupf o∅) ab →
             * a < * b → odef (UnionCF A f mf ay isupf o∅) b
-          imax {a} {b} ua b<ox ab (case1 hasp) a<b = subst (λ k → odef  (UnionCF A f mf ay isupf o∅) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) )
-          imax {a} {b} ua b<ox ab (case2 sup)  a<b = ?
-          -- with IsSup.x<sup sup (inext 
-          -- ... | case1 a=b = ?
-          -- ... | case2 a<b = ?
-          -- ⊥-elim ( <-irr (case2 ? ) ( IsSup  ) )
+          imax {a} {b} ua b<x ab (case1 hasp) a<b = subst (λ k → odef  (UnionCF A f mf ay isupf o∅) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) )
+          imax {a} {b} ua b<x ab (case2 sup)  a<b = ⊥-elim ( ¬x<0 b<x )
 
      --
      -- create all ZChains under o< x
@@ -568,9 +569,21 @@
              → pchain ≡ UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) 
           chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
 
+          zc11 : ( {z : Ordinal} → (az : odef pchain z) → ¬ ( UChain.u (proj2 az) ≡ px  )) → pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) px
+          zc11 ne {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = 
+              ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ 
+          zc11 ne {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ with trio<  o∅ px
+          ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-init z fc } ⟫  
+          ... | tri≈ ¬a b ¬c = ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫  
+          ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+          zc11 ne {z} uz@record { proj1 = az ; proj2 =  record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } } with trio< u px
+          ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ 
+          ... | tri≈ ¬a b ¬c = ⊥-elim ( ne uz  b )
+          ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op))  u<x  ⟫ )
+
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* px)
-          ... | no nopax = no-extenion zc1 where -- ¬ A ∋ p, just skip
+          ... | no noapx = no-extenion zc1 where -- ¬ A ∋ p, just skip
                 zc1 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
                     HasPrev A pchain ab f ∨  IsSup A pchain ab →
                             * a < * b → odef pchain b
@@ -579,22 +592,37 @@
                       zc10 : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)
                       zc10 {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = 
                                     ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ 
-                      zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ = 
-                                    ⟪ az , record { u = u ; u<x = case1 ? ; uchain = ch-init z fc } ⟫ 
-                      zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = 
-                                    ⟪ az , record { u = u ; u<x = case1 ? ; uchain = ch-is-sup is-sup fc } ⟫ 
-                -- ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
-                ... | tri≈ ¬a b=px ¬c = ?
+                      zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ with trio<  o∅ px
+                      ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-init z fc } ⟫  
+                      ... | tri≈ ¬a b ¬c = ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫  
+                      ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+                      zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ with trio< u px
+                      ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ 
+                      ... | tri≈ ¬a b ¬c = ⊥-elim ( noapx ( subst (λ k → odef A k ) (trans b (sym &iso) )  (ChainP.au is-sup ) ))
+                      ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op))  u<x  ⟫ )
+                ... | tri≈ ¬a b=px ¬c = ⊥-elim ( noapx (subst (λ k → odef A k ) (trans b=px (sym &iso))  ab ) )
                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
           ... | yes apx with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) apx f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
-          ... | case1 pr = no-extenion ? where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
+          ... | case1 pr = no-extenion zc7 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
                 zc7 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
                     HasPrev A pchain ab f ∨  IsSup A pchain ab →
                             * a < * b → odef pchain b
-                zc7 {a} {b} za b<x ab P a<b with osuc-≡< ?
-                ... | case2 lt = zcp za ? ? ab P a<b
-                ... | case1 b=x = ? 
+                zc7 {a} {b} za b<x ab P a<b with trio< b px
+                ... | tri< lt ¬b ¬c = zcp za (chain-≡ zc10) lt ab P a<b where
+                      zc10 : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)
+                      zc10 {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = 
+                                    ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ 
+                      zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ with trio<  o∅ px
+                      ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-init z fc } ⟫  
+                      ... | tri≈ ¬a b ¬c = ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫  
+                      ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+                      zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ with trio< u px
+                      ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ 
+                      ... | tri≈ ¬a b ¬c = ? -- ⊥-elim ( noapx ( subst (λ k → odef A k ) (trans b (sym &iso) )  (ChainP.au is-sup ) ))
+                      ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op))  u<x  ⟫ )
+                ... | tri≈ ¬a b=px ¬c = ? -- ⊥-elim ( noapx (subst (λ k → odef A k ) (trans b=px (sym &iso))  ab ) )
+                ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
                 -- subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx )
           ... | case1 is-sup = -- x is a sup of zc 
@@ -604,19 +632,23 @@
                     b o< x → (ab : odef A b) →
                     ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) →
                         * a < * b → odef pchain b
-                p-ismax {a} {b} ua b<x ab (case1 hasp) a<b = ?
-                p-ismax {a} {b} ua b<x ab (case2 sup)  a<b = ?
-
-          ... | case2 ¬x=sup =  no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
+                p-ismax {a} {b} za b<x ab P a<b with trio< b px
+                ... | tri< lt ¬b ¬c = zcp za (chain-≡ ? ) lt ab P a<b 
+                ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
+                ... | tri≈ ¬a b=px ¬c with P
+                ... | case1 hasp = ?
+                ... | case2 sup  = ?
+          ... | case2 ¬x=sup =  no-extenion z18 where -- px is not f y' nor sup of former ZChain from y -- no extention
                 z18 :  {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
                             HasPrev A pchain ab f ∨ IsSup A pchain   ab →
                             * a < * b → odef pchain b
-                z18 {a} {b} za b<x ab P a<b with osuc-≡< ?
-                ... | case2 lt = zcp za ? ? ab P a<b
-                ... | case1 b=x with P
+                z18 {a} {b} za b<x ab P a<b with trio< b px
+                ... | tri< lt ¬b ¬c = zcp za (chain-≡ ? ) lt ab P a<b 
+                ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
+                ... | tri≈ ¬a b=px ¬c with P
                 ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
-                      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) 
+                      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=px (sym &iso)) 
                           (IsSup.x<sup b=sup (chain-mono zy) )  } ) 
      ... | no op = zc5 where
           pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z