changeset 582:48e9d2e61bbe

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 07 Jun 2022 02:18:25 +0900
parents 95ec4d121e12
children f545b97ce7a8
files src/zorn.agda
diffstat 1 files changed, 26 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jun 06 17:18:05 2022 +0900
+++ b/src/zorn.agda	Tue Jun 07 02:18:25 2022 +0900
@@ -235,8 +235,8 @@
    field
       x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
-record ZChain ( A : HOD )  {x : Ordinal} (ax : odef A x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f )
-                 (sup : (C : HOD ) → ( C ⊆' A) → IsTotalOrderSet C → Ordinal) ( z : Ordinal ) : Set (Level.suc n) where
+record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) 
+                  ( z : Ordinal ) : Set (Level.suc n) where
    field
       chain : HOD
       chain⊆A : chain ⊆' A
@@ -250,6 +250,15 @@
           → * a < * b  → odef chain b
       fc∨sup :  {a : Ordinal } → a o< osuc z →  ( ca : odef chain a ) → HasPrev A chain ( chain⊆A ca) f  ∨ IsSup A chain  ( chain⊆A ca)
 
+Uz-mono : ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) 
+     → ( a b : Ordinal ) → a o< b → (za : ZChain A x f a) (zb : ZChain A x f b) 
+     → ZChain.chain za  ⊆' ZChain.chain zb
+Uz-mono A x f a b a<b za zb {i} zai = TransFinite0 (ind i) a where
+    open ZChain
+    ind : (i a : Ordinal) → ((y : Ordinal) → y o< a → odef (ZChain.chain zb) i) → odef (ZChain.chain zb) i 
+    ind = ?
+
+
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
       maximal : HOD
@@ -319,12 +328,12 @@
      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  ) ⟫
 
-     zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc : ZChain A as f mf supO (& A) ) → SUP A  (ZChain.chain zc) 
+     zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc : ZChain A (& s) f (& A) ) → SUP A  (ZChain.chain zc) 
      zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc  )   
-     A∋zsup :  (nmx : ¬ Maximal A ) (zc : ZChain A as (cf nmx) (cf-is-≤-monotonic nmx) supO (& A) ) 
+     A∋zsup :  (nmx : ¬ Maximal A ) (zc : ZChain A (& s) (cf nmx)  (& A) ) 
         →  A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) ))
      A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal  (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )
-     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (subst (λ k → odef A k ) &iso as ) f mf supO (& A) ) → SUP A (ZChain.chain zc)
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (& A) ) → SUP A (ZChain.chain zc)
      sp0 f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain.f-total zc) 
      zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P
      zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y)
@@ -332,7 +341,7 @@
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
-     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (subst (λ k → odef A k ) &iso as ) f mf supO (& A) )
+     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (& A) )
             → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc ))
      fixpoint f mf zc = z14 where
            chain = ZChain.chain zc
@@ -380,7 +389,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 ) → (zc : ZChain A (subst (λ k → odef A k ) &iso as ) (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) → ⊥
+     z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (& s) (cf nmx)  (& A)) → ⊥
      z04 nmx zc = <-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 ) zc ))) -- x ≡ f x ̄
@@ -392,19 +401,19 @@
      -- create all ZChains under o< x
      --
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) →
-            ((z : Ordinal) → z o< x → {y : Ordinal} → (ya : odef A y) → ZChain A ya f mf supO z ) → { y : Ordinal } → (ya : odef A y) → ZChain A ya f mf supO x
+            ((z : Ordinal) → z o< x → {y : Ordinal} → (ya : odef A y) → ZChain A y f z ) → { y : Ordinal } → (ya : odef A y) → ZChain A y f x
      ind f mf x prev {y} ay with Oprev-p x
      ... | yes op = zc4 where
           --
           -- we have previous ordinal to use induction
           --
           px = Oprev.oprev op
-          zc0 : ZChain A ay f mf supO (Oprev.oprev op)
+          zc0 : ZChain A y f (Oprev.oprev op)
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay
           zc0-b<x : (b : Ordinal ) → b o< x → b o< osuc px
           zc0-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
 
-          zc4 : ZChain A ay f mf supO x 
+          zc4 : ZChain A y f x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax =  -- ¬ A ∋ p, just skip
                  record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 
@@ -416,7 +425,7 @@
                 zc11 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
                 ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt)  ab P a<b
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax f )   -- we have to check adding x preserve is-max ZChain A ay f mf supO x
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax f )   -- we have to check adding x preserve is-max ZChain A y f mf supO x
           ... | case1 pr = zc9 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
                 chain = ZChain.chain zc0
                 zc17 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
@@ -425,7 +434,7 @@
                 zc17 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b
                 ... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
-                zc9 :  ZChain A ay f mf supO x
+                zc9 :  ZChain A y f x
                 zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 -- no extention
                      ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = {!!}}  
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
@@ -548,7 +557,7 @@
                      ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }
      ... | tri≈ ¬a b ¬c = {!!}
      ... | tri> ¬a ¬b y<x = {!!} where
-       UnionZ : ZChain A ay f mf supO x
+       UnionZ : ZChain A y f x
        UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next
                      ; initial = u-initial ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
@@ -558,7 +567,7 @@
                chain∋z : odef (ZChain.chain (prev u u<x {y} ay )) z
          Uz⊆A : {z : Ordinal} → UZFChain z → odef A z
          Uz⊆A {z} u = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) {y} ay ) (UZFChain.chain∋z u)
-         uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A ay f mf supO  (UZFChain.u u)
+         uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f (UZFChain.u u)
          uzc {z} u =  prev (UZFChain.u u) (UZFChain.u<x u) {y} ay
          Uz : HOD
          Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A
@@ -569,11 +578,6 @@
          u-initial {z} u = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
          u-chain∋x :  odef Uz y
          u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) }
-         Uz-mono : { a b : Ordinal } → (ua : odef Uz a) (ub : odef Uz b )  → a o< b → b o< x → ZChain.chain (uzc ua) ⊆' ZChain.chain (uzc ub)
-         Uz-mono {a} {b} ua ub a<b b<x {i} = z40 where
-             z40 : odef (ZChain.chain (uzc ua)) i → odef (ZChain.chain (uzc ub)) i
-             z40 uai = ZChain.is-max (uzc ub) (ZChain.chain∋x (uzc ub)) {!!} {!!}
-                (ZChain.fc∨sup (uzc ub) {!!} {!!} ) ?
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy = {!!}
          --- ux ⊆ uy ∨ uy ⊆ ux
@@ -594,9 +598,9 @@
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
               zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) 
               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) ) ⟫
-         zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain A ya f mf supO (& A)
-         zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A ya f mf supO z } (ind f mf) (& A)
-         zorn04 : ZChain A (subst (λ k → odef A k ) &iso as ) (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)
+         zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain A (& s) f (& A)
+         zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A y f z } (ind f mf) (& A)
+         zorn04 : ZChain A (& s) (cf nmx)  (& A)
          zorn04 = zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
 
 -- usage (see filter.agda )