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

changeset 533:7325484fc491

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 Sat, 23 Apr 2022 17:46:12 +0900
parents 90f61d55cc54
children c9f80aea598e
files src/zorn.agda
diffstat 1 files changed, 62 insertions(+), 44 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Apr 22 13:56:31 2022 +0900
+++ b/src/zorn.agda	Sat Apr 23 17:46:12 2022 +0900
@@ -438,12 +438,20 @@
 ≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set (Level.suc n)
 ≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧  odef A (f x )
 
-record ZChain ( A : HOD ) {x : Ordinal} (ax : A ∋ * x) (z : Ordinal)  : Set (Level.suc n) where
+record Indirect< (A : HOD) {x y : Ordinal } (xa : odef A x) (ya : odef A y) (z : Ordinal)  : Set n where
    field
-      chain : HOD
-      chain⊆A : chain ⊆ A
-      f-total : ( f : Ordinal → Ordinal ) → ≤-monotonic-f A f → IsTotalOrderSet chain 
-      is-max :  ( f : Ordinal → Ordinal ) → ≤-monotonic-f A f → {a b : Ordinal } → odef chain a → a o< z → * a < * b  → odef chain b
+      az : odef A z
+      x<z : * x < * z 
+      z<y : * z < * y 
+
+IndirectSet< : (A : HOD) → {x y : Ordinal } (xa : odef A x) (ya : odef A y) → HOD
+IndirectSet< A {x} {y} xa ya = record { od = record { def = λ z → odef A z ∧ Indirect< A xa ya z } ; odmax = & A ; <odmax = {!!} }
+
+record Prev< (A : HOD) {x : Ordinal } (xa : odef A x) : Set n where
+   field
+      prev : Ordinal
+      aprev : odef A prev
+      direct : & (IndirectSet< A aprev xa ) ≡ o∅ 
 
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
@@ -451,6 +459,18 @@
       A∋maximal : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
+SupCond : ( A B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → Set (Level.suc n)
+SupCond A B _ _ = SUP A B  
+
+record ZChain ( A : HOD ) {x : Ordinal} (ax : A ∋ * x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f )
+         (sup : (C : Ordinal ) → IsTotalOrderSet (* C) → Ordinal) (z : Ordinal)  : Set (Level.suc n) where
+   field
+      chain : HOD
+      chain⊆A : chain ⊆ A
+      f-total : IsTotalOrderSet chain 
+      f-next : {a : Ordinal } → odef chain a → odef chain (f a)
+      is-max :  {a b : Ordinal } → odef chain a → odef A b → a o< z → ( ? ∨ (sup (& chain)  (subst ? ? f-total) ≡ b )) → * a < * b  → odef chain b
+
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
     → IsPartialOrderSet A 
@@ -470,14 +490,14 @@
          z07 :   {y : Ordinal} → odef A y ∧ ((m : Ordinal) → odef A m → ¬ (* y < * m)) → y o< & A
          z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
      no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → ((m : Ordinal) →  odef A m →  odef A x ∧ (¬ (* x < * m) )) →  ⊥
-     no-maximum nomx x P = ¬x<0 (eq→ nomx {x} ? ) 
+     no-maximum nomx x P = ¬x<0 (eq→ nomx {x} {!!} ) 
      Gtx : { x : HOD} → A ∋ x → HOD
      Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = {!!} } 
      cf : ¬ Maximal A → Ordinal → Ordinal
      cf  nmx x with ODC.∋-p O A (* x)
      ... | no _ = o∅
      ... | yes ax with is-o∅ (& ( Gtx ax ))
-     ... | yes nogt = ⊥-elim (no-maximum ? x x-is-maximal ) where -- no larger element, so it is maximal
+     ... | yes nogt = ⊥-elim (no-maximum (≡o∅→=od∅ {!!} ) x x-is-maximal ) where -- no larger element, so it is maximal
           x-is-maximal :  (m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m))
           x-is-maximal m am  = ⟪ subst (λ k → odef A k) &iso ax ,  ¬x<m  ⟫ where
               ¬x<m :  ¬ (* x < * m)
@@ -487,45 +507,45 @@
      cf-is-<-monotonic nmx x ax = ⟪ {!!} , {!!} ⟫
      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 : (zc : ZChain A sa (& A)) → ( f : Ordinal → Ordinal ) → ≤-monotonic-f A f  → SUP A  (ZChain.chain zc) 
-     zsup zc f mf = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf )   
+     zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc : ZChain A sa f mf ? (& A)) → SUP A  (ZChain.chain zc) 
+     zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc  )   
      -- zsup zc f mf = & ( SUP.sup (supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf )  ) )
-     A∋zsup : (zc : ZChain A sa (& A)) →  (nmx : ¬ Maximal A )  →  A ∋ * ( & ( SUP.sup (zsup zc (cf nmx) (cf-is-≤-monotonic nmx)) ))
-     A∋zsup zc nmx = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal  (zsup zc (cf nmx) (cf-is-≤-monotonic nmx)) )
-     z03 : (zc : ZChain A sa (& A)) → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → f (& ( SUP.sup (zsup zc f mf ))) ≡ & (SUP.sup (zsup zc f mf ))
+     A∋zsup :  (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic 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 ) )
+     z03 :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf ? (& A)) → f (& ( SUP.sup (zsup f mf zc ))) ≡ & (SUP.sup (zsup f mf zc ))
      z03 = {!!}
-     z04 : (zc : ZChain A sa (& A)) → ¬ Maximal A  → ⊥
-     z04 zc nmx = z01  {* (cf nmx c)} {* c} {!!} (A∋zsup zc nmx ) (case1 ( cong (*)( z03 zc (cf nmx) (cf-is-≤-monotonic nmx ))))
-           (proj1 (cf-is-<-monotonic nmx c ((subst λ k → odef A k ) &iso (A∋zsup zc nmx )))) where
-          c = & (SUP.sup (zsup zc (cf nmx) (cf-is-≤-monotonic nmx)))
+     z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) ?  (& A)) → ⊥
+     z04 nmx zc = z01  {* (cf nmx c)} {* c} {!!} (A∋zsup nmx zc ) (case1 ( cong (*)( z03 (cf nmx) (cf-is-≤-monotonic nmx ) zc )))
+           (proj1 (cf-is-<-monotonic nmx c ((subst λ k → odef A k ) &iso (A∋zsup nmx zc )))) where
+          c = & (SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ))
      -- ZChain is not compatible with the SUP condition
-     ind : (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A sa y ∨ Maximal A )
-         →  ZChain A sa x ∨ Maximal A 
-     ind x prev with Oprev-p x
+     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A sa f mf ? y )
+         →  ZChain A sa f mf ? x 
+     ind f mf x prev with Oprev-p x
      ... | yes op with ODC.∋-p O A (* x)
      ... | no ¬Ax = zc1 where
           -- we have previous ordinal and ¬ A ∋ x, use previous Zchain
           px = Oprev.oprev op
-          zc1 : ZChain A sa x ∨ Maximal A
-          zc1 with prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
-          ... | case2 x = case2 x  -- we have the Maximal
-          ... | case1 zc = case1 {!!}
+          zc0 : ZChain A sa f mf ? (Oprev.oprev op) 
+          zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
+          zc1 : ZChain A sa f mf ? x 
+          zc1 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; is-max = {!!} }
      ... | yes ax = zc4 where -- we have previous ordinal and A ∋ x
           px = Oprev.oprev op
-          zc1 : OSup> A (subst (OD.def (od A)) (sym &iso) (subst (OD.def (od A)) &iso ax)) → ZChain A sa x ∨ Maximal A
-          zc1 os with  prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
-          ... | case2 mx = case2 mx
-          ... | case1 zc = case1 {!!}
-          zc4 : ZChain A sa x ∨ Maximal A
-          zc4 with Zorn-lemma-3case 0<A PO x (subst (λ k → odef A k) &iso ax )
-          ... | case1 y>x = zc1 y>x
-          ... | case2 (case1 mx) = case2 mx
-          ... | case2 (case2 ic) with  prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
-          ... | case2 mx = case2 mx
-          ... | case1 zc = {!!}
-     ind x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
-     ... | t = {!!}
-
+          zc0 : ZChain A sa f mf ? (Oprev.oprev op) 
+          zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
+          --   x is in the previous chain, use the same
+          --   x has some y which y < x ∧ f y ≡ x
+          --   x has no y which y < x 
+          zc4 : ZChain A sa f mf ? x
+          zc4 = record { chain = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; is-max = {!!} }
+     ind f mf x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
+     ... | tri< a ¬b ¬c = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
+              ; is-max = {!!} } where
+          zc0 = prev (& A) a
+     ... | tri≈ ¬a b ¬c = {!!}
+     ... | tri> ¬a ¬b c = {!!}
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
      ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where
@@ -536,16 +556,14 @@
          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 zorn03  zorn04 ) where
+     ... | yes ¬Maximal = ⊥-elim ( z04 nmx  (zorn03 (cf nmx) (cf-is-≤-monotonic nmx))) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
-         zorn04 : ¬ Maximal A 
-         zorn04 mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
+         nmx : ¬ Maximal A 
+         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 : ZChain A sa (& A)
-         zorn03 with TransFinite ind  (& A)
-         ... | case1 zc = zc
-         ... | case2 mx = ⊥-elim ( zorn04 mx )
+         zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → ZChain A sa f mf ? (& A)
+         zorn03 f mf = TransFinite (ind f mf)  (& A) 
 
 -- usage (see filter.agda )
 --