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

changeset 662:a45ec34b9fa7

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 Sun, 03 Jul 2022 14:20:22 +0900
parents 9142e834c4c6
children 5f85e71b2490
files src/zorn.agda
diffstat 1 files changed, 31 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Jul 03 06:10:51 2022 +0900
+++ b/src/zorn.agda	Sun Jul 03 14:20:22 2022 +0900
@@ -239,8 +239,9 @@
       A∋maximal : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
+-- Union of supf z which o< x
+--
 record UChain (x : Ordinal) (chain : (z : Ordinal ) → z o< x → HOD)  (z : Ordinal) : Set n where 
-   -- Union of supf z which o< x
    field
       u : Ordinal
       u<x : u o< x
@@ -255,7 +256,7 @@
         ( c : Chain A f ay (Oprev.oprev op) chain) ( h :  HasPrev A chain ax f ) → Chain A f ay x chain
     ch-is-sup : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x ) 
         ( c : Chain A f ay (Oprev.oprev op) chain) ( nh :  ¬ HasPrev A chain  ax f ) ( sup : IsSup A chain   ax ) → Chain A f ay x 
-            record { od = record { def = λ x → odef A x ∧ (odef chain x ∨ (FClosure A f y x)) } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
+            record { od = record { def = λ z → odef A z ∧ (odef chain z ∨ (FClosure A f x z)) } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
     ch-skip : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x ) 
         ( c : Chain A f ay (Oprev.oprev op) chain) ( nh : ¬  HasPrev A chain ax f ) ( nsup : ¬ IsSup A chain ax ) → Chain A f ay x chain
     ch-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x ) 
@@ -264,14 +265,17 @@
              record { od = record { def = λ z → odef A z ∧ (UChain x chainf z ∨ FClosure A f y z ) } 
                 ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
+ChainF : (A : HOD) →  ( f : Ordinal → Ordinal ) {y : Ordinal} (ay : odef A y) → (chain : HOD ) → Chain A f ay (& A) chain → (x : Ordinal) → x o< & A →  HOD
+ChainF A f {y} ay chain Ch x x<a = ?
+
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
    field
       chain : HOD
       chain-uniq : Chain A f ay z chain 
 
-record ZChain ( A : HOD )    ( f : Ordinal → Ordinal ) {init : Ordinal} (ay : odef A init)  (zc0 : (x : Ordinal) → ZChain1 A f ay x ) ( z : Ordinal ) : Set (Level.suc n) where
+record ZChain ( A : HOD )    ( f : Ordinal → Ordinal ) {init : Ordinal} (ay : odef A init)  (zc0 :  ZChain1 A f ay (& A) ) ( z : Ordinal ) : Set (Level.suc n) where
    chain : HOD
-   chain = ZChain1.chain (zc0 z)
+   chain = ?
    field
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
@@ -345,7 +349,7 @@
      cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
      cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
 
-     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : (x : Ordinal) → ZChain1 A f as0 x ) (zc : ZChain A f as0 zc0 (& A) ) 
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f as0 (& A) ) (zc : ZChain A f as0 zc0 (& A) ) 
         (total : IsTotalOrderSet (ZChain.chain zc) )  → SUP A (ZChain.chain zc)
      sp0 f mf zc0 zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total 
      zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P
@@ -354,7 +358,7 @@
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
-     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : (x : Ordinal) → ZChain1 A f as0 x) (zc : ZChain A f as0 zc0 (& A) )
+     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f as0 (& A)) (zc : ZChain A f as0 zc0 (& A) )
             → (total : IsTotalOrderSet (ZChain.chain zc) )
             → f (& (SUP.sup (sp0 f mf zc0 zc total ))) ≡ & (SUP.sup (sp0 f mf zc0 zc  total))
      fixpoint f mf zc0 zc total = z14 where
@@ -403,7 +407,7 @@
      -- ZChain forces fix point on any ≤-monotonic function (fixpoint)
      -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain
      --
-     z04 :  (nmx : ¬ Maximal A ) → (zc0 : (x : Ordinal) → ZChain1 A (cf nmx) as0 x) (zc : ZChain A (cf nmx) as0 zc0 (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥
+     z04 :  (nmx : ¬ Maximal A ) → (zc0 : ZChain1 A (cf nmx) as0 (& A)) (zc : ZChain A (cf nmx) as0 zc0 (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥
      z04 nmx zc0 zc total = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal  sp1 ))))
                                                (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) )
            (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc0 zc total ))) -- x ≡ f x ̄
@@ -428,11 +432,14 @@
           sc = prev px px<x
           sc4 : ZChain1 A f ay x
           sc4 with ODC.∋-p O A (* x)
-          ... | no noax = record { chain = ? ; chain-uniq = ? } 
+          ... | no noax = record { chain = chain sc ; chain-uniq = ch-noax op (subst (λ k → ¬ odef A k) &iso noax) ( chain-uniq sc )  } 
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain1.chain sc ) ax f )   
-          ... | case1 pr = {!!}
+          ... | case1 pr = record { chain = chain sc ; chain-uniq = ch-hasprev op (subst (λ k → odef A k) &iso ax) ( chain-uniq sc ) 
+                                       record { y = HasPrev.y pr  ; ay = HasPrev.ay pr  ; x=fy = sc6 } } where
+                sc6 : x ≡ f (HasPrev.y pr)
+                sc6 = subst (λ k → k ≡ f (HasPrev.y pr) ) &iso  ( HasPrev.x=fy pr  )
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.chain sc ) ax )
-          ... | case1 is-sup = {!!} where
+          ... | case1 is-sup = record { chain = schain ; chain-uniq = sc9 } where
                 -- A∋sc -- x is a sup of zc 
                 sup0 : SUP A (ZChain1.chain sc  )
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
@@ -445,6 +452,10 @@
                 schain : HOD
                 schain = record { od = record { def = λ x → odef A x ∧ ( odef (ZChain1.chain sc ) x ∨ (FClosure A f (& sp) x)) } 
                     ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
+                sc8 : Chain A f ay ? ?
+                sc8 = ch-is-sup op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) ? ?  
+                sc9 : Chain A f ay x schain
+                sc9 = ?
           ... | case2 ¬x=sup = {!!}
      ... | no ¬ox = ? where
           supf : (z : Ordinal) → z o< x → HOD
@@ -452,7 +463,7 @@
           sc5 : HOD
           sc5 = record { od = record { def = λ z → odef A z ∧ (UChain x supf z ∨ FClosure A f y z)} ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
-     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → (zc0 : (x : Ordinal) → ZChain1 A f ay x) 
+     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → (zc0 :  ZChain1 A f ay (& A)) 
          → ((z : Ordinal) → z o< x → ZChain A f ay zc0 z) → ZChain A f ay zc0 x
      ind f mf {y} ay x zc0 prev with Oprev-p x
      ... | yes op = zc4 where
@@ -461,7 +472,7 @@
           --
           px = Oprev.oprev op
           supf : Ordinal → HOD
-          supf x = ZChain1.chain (zc0 x)
+          supf x = ZChain1.chain zc0 
           zc : ZChain A f ay zc0 (Oprev.oprev op)
           zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
           zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
@@ -629,7 +640,7 @@
      ... | no ¬ox = record { chain⊆A = {!!} ; f-next = {!!} ; f-total = ?
                      ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!} }   where --- limit ordinal case
          supf : Ordinal → HOD
-         supf x = ZChain1.chain (zc0 x)
+         supf x = ZChain1.chain zc0 
          uzc : {z : Ordinal} → (u : UChain x ? z) → ZChain A f ay zc0 (UChain.u u)
          uzc {z} u =  prev (UChain.u u) (UChain.u<x u) 
          Uz : HOD
@@ -646,7 +657,7 @@
          u-chain∋init = ? -- case2 ( init ay )
          supf0 : Ordinal → HOD
          supf0 z with trio< z x
-         ... | tri< a ¬b ¬c = ZChain1.chain (zc0 z)
+         ... | tri< a ¬b ¬c = ZChain1.chain zc0 
          ... | tri≈ ¬a b ¬c = Uz 
          ... | tri> ¬a ¬b c = Uz
          u-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w
@@ -658,9 +669,9 @@
          ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
          ... | tri≈ ¬a b ¬c = refl
          ... | tri> ¬a ¬b c = refl
-         seq<x : {b : Ordinal } → (b<x : b o< x ) →  ZChain1.chain (zc0 b)  ≡ supf0 b
+         seq<x : {b : Ordinal } → (b<x : b o< x ) →  ZChain1.chain zc0  ≡ supf0 b
          seq<x {b} b<x with trio< b x
-         ... | tri< a ¬b ¬c = cong (λ k → ZChain1.chain (zc0 b)) o<-irr --  b<x ≡ a
+         ... | tri< a ¬b ¬c = ? -- cong (λ k → (ZChain1.chain zc0) o<-irr --  b<x ≡ a
          ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
          ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
          ord≤< : {x y z : Ordinal} → x o< z → z o≤ y → x o< y
@@ -671,8 +682,8 @@
      SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f ay x
      SZ0 f mf ay x = TransFinite {λ z → ZChain1 A f ay z} (sind f mf ay ) x
 
-     SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f ay (SZ0 f mf ay)  (& A)
-     SZ f mf {y} ay = TransFinite {λ z → ZChain A f ay (SZ0 f mf ay)  z  } (λ x → ind f mf ay x (SZ0 f mf ay)  ) (& A)
+     SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f ay (SZ0 f mf ay (& A))  (& A)
+     SZ f mf {y} ay = TransFinite {λ z → ZChain A f ay (SZ0 f mf ay (& A))  z  } (λ x → ind f mf ay x (SZ0 f mf ay (& A))  ) (& A)
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
@@ -684,7 +695,7 @@
          zorn01  = proj1  zorn03  
          zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
          zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
-     ... | yes ¬Maximal = ⊥-elim ( z04 nmx zc0 zorn04 total ) where
+     ... | yes ¬Maximal = ⊥-elim ( z04 nmx (zc0 (& A)) zorn04 total ) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A 
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
@@ -692,7 +703,7 @@
               zc5 = ⟪  Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫
          zc0 : (x : Ordinal) → ZChain1 A  (cf nmx) as0 x
          zc0 x = TransFinite {λ z → ZChain1 A (cf nmx) as0 z} (sind (cf nmx) (cf-is-≤-monotonic nmx)  as0) x
-         zorn04 : ZChain A (cf nmx) as0 zc0 (& A)
+         zorn04 : ZChain A (cf nmx) as0 (zc0 (& A)) (& A)
          zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) 
          total : IsTotalOrderSet (ZChain.chain zorn04)
          total {a} {b} = zorn06  where