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

changeset 695:7c0bb8ed7193

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, 11 Jul 2022 16:46:18 +0900
parents 196eff771492
children 0e28091e9271
files src/zorn.agda
diffstat 1 files changed, 47 insertions(+), 77 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jul 11 14:15:17 2022 +0900
+++ b/src/zorn.agda	Mon Jul 11 16:46:18 2022 +0900
@@ -248,11 +248,11 @@
 
 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
    field
-      y-init    : supf o∅  ≡ y
-      asup    : (x : Ordinal) → odef A (supf x)
+      y-init   : supf o∅  ≡ y
+      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
+      csupz    : FClosure A f (supf sup) z 
+      order    : {sup1 z1 : Ordinal} → (lt : sup1 o< sup ) → FClosure A f (supf sup1 ) z1 → z1 << supf sup
 
 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 y z 
@@ -281,8 +281,8 @@
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
    field
       supf :  Ordinal → Ordinal 
-      supf-mono : (x y : Ordinal ) → x o≤ y  → supf x o≤ supf y
-      is-chain : {w : Ordinal } → Chain A f mf ay supf z w 
+      -- is-chain : {w : Ordinal } → Chain A f mf ay supf z w 
+      -- supf-mono : (x y : Ordinal ) → x o≤ y  → supf x o≤ supf y
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)  
           (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where
@@ -304,9 +304,6 @@
       A∋maximal : A ∋ maximal
       ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
-SupCond : ( A B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → Set (Level.suc n)
-SupCond A B _ _ = SUP A B  
-
 -- data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) : Ordinal →  Ordinal → Set n where
 --
 -- data Chain is total
@@ -317,33 +314,33 @@
      ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay supf xa a → Chain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
-          ct00 : * a < * xb
-          ct00 = {!!} -- ChainP.fcy<sup supb fca
+          ct00 : * a < * (supf xb)
+          ct00 = ChainP.fcy<sup supb fca
           ct01 : * a < * b 
-          ct01 with s≤fc xb f mf {!!}
+          ct01 with s≤fc (supf xb) 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 supa fca) (ch-init b fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
-          ct00 : * b < * xa
-          ct00 = {!!} -- ChainP.fcy<sup supa fcb
+          ct00 : * b < * (supf xa)
+          ct00 = ChainP.fcy<sup supa fcb
           ct01 : * b < * a 
-          ct01 with s≤fc xa f mf  {!!}
+          ct01 with s≤fc (supf xa) 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 supa fca) (ch-is-sup supb fcb) with trio< xa xb
      ... | tri< a₁ ¬b ¬c = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
-          ct03 : * a < * xb
-          ct03 = {!!} -- ChainP.order supb a₁ (ChainP.csupz supa)
+          ct03 : * a < * (supf xb)
+          ct03 = ChainP.order supb a₁ (ChainP.csupz supa)
           ct02 : * a < * b 
-          ct02 with s≤fc xb f mf {!!} 
+          ct02 with s≤fc (supf xb) f mf fcb
           ... | case1 eq =  subst (λ k → * a < k ) eq ct03
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
-     ... | tri≈ ¬a  refl ¬c = fcn-cmp xa f mf {!!} {!!} 
+     ... | tri≈ ¬a  refl ¬c = fcn-cmp (supf xa) f mf fca fcb
      ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
-          ct05 : * b < * xa
-          ct05 = {!!} -- ChainP.order supa c (ChainP.csupz supb)
+          ct05 : * b < * (supf xa)
+          ct05 = ChainP.order supa c (ChainP.csupz supb)
           ct04 : * b < * a 
-          ct04 with s≤fc xa f mf {!!} 
+          ct04 with s≤fc (supf xa) f mf fca
           ... | case1 eq =  subst (λ k → * b < k ) eq ct05
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct05 lt
 
@@ -475,7 +472,10 @@
 
      sind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
          → ((z : Ordinal) → z o< x → ZChain1 A f mf ay z ) → ZChain1 A f mf ay x
-     sind f mf {y} ay x prev  with Oprev-p x
+     sind f mf {y} ay x prev  with trio< o∅ x
+     ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c )
+     ... | tri≈ ¬a b ¬c = record { supf = λ _ → y }
+     ... | tri< 0<x ¬b ¬c with Oprev-p x
      ... | yes op = sc4 where
           open ZChain1
           px = Oprev.oprev op
@@ -484,85 +484,55 @@
           sc : ZChain1 A f mf ay px
           sc = prev px px<x
           pchain : HOD
-          pchain  = {!!}
+          pchain  = UnionCF A f mf ay (ZChain1.supf sc) x
 
           no-ext :  ZChain1 A f mf ay x
-          no-ext = {!!} where -- record { supf = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = ? }  where
-            psup1 : Ordinal → Ordinal
-            psup1 z with o≤? z x
-            ... | yes _ = ZChain1.supf sc z
-            ... | no _ = ZChain1.supf sc x
-            chainf1 : (z : Ordinal ) → HOD
-            chainf1 z with o≤? z x
-            ... | yes _  = {!!}
-            ... | no _ = {!!}
-            is-chain1 : {!!}
-            is-chain1 = {!!}
+          no-ext = record { supf = ZChain1.supf sc }  
           sc4 : ZChain1 A f mf ay x
           sc4 with ODC.∋-p O A (* x)
           ... | no noax = no-ext
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
           ... | case1 pr = no-ext
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { supf = {!!} ; p≤z = {!!} ; chainf = {!!} ; is-chain = {!!} } where
-                schain : HOD
-                schain = {!!} -- record { od = record { def = λ z → odef A z ∧ ( odef (ZChain1.chain sc ) z ∨ (FClosure A f x z)) } 
-                    -- ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
+          ... | case1 is-sup = record { supf = psup1 } where
+            psup1 : Ordinal → Ordinal
+            psup1 z with trio< z x 
+            ... | tri< a ¬b ¬c = ZChain1.supf sc z
+            ... | tri≈ ¬a b ¬c = x
+            ... | tri> ¬a ¬b c = x
           ... | case2 ¬x=sup = no-ext
      ... | no ¬ox = sc4 where
-          pchainf : (z : Ordinal) → z o< x → HOD
-          pchainf z z<x = {!!} -- Chain1.chainf (prev z z<x) z  
           pzc : (z : Ordinal) → z o< x → ZChain1 A f mf ay z
           pzc z z<x = prev z z<x
+          psupf : (z : Ordinal) → Ordinal
+          psupf z with trio< z x
+          ... | tri< a ¬b ¬c = ZChain1.supf (pzc z a) z
+          ... | tri≈ ¬a b ¬c = o∅
+          ... | tri> ¬a ¬b c = o∅
           UZ : HOD
-          UZ = {!!} -- UnionCF A x pchainf
-          chainf0 : (z : Ordinal ) → HOD
-          chainf0 z with trio< z x
-          ... | tri< a ¬b ¬c = {!!} -- ZChain1.chainf (pzc z a) z
-          ... | tri≈ ¬a b ¬c = UZ
-          ... | tri> ¬a ¬b c = UZ
-          Chain-ext : {!!}
-          Chain-ext = {!!}
+          UZ = UnionCF A f mf ay psupf x
           total-UZ : IsTotalOrderSet UZ
           total-UZ {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay {!!}
-                   (Chain-ext ca (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) (UChain.chain∋z (proj2 ca)))) 
-                   (Chain-ext cb (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) (UChain.chain∋z (proj2 cb)))) 
+               uz01 = chain-total A f mf ay psupf (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 
           usup : SUP A UZ
           usup = supP UZ (λ lt → proj1 lt) total-UZ 
           spu = & (SUP.sup usup)
           sc4 :  ZChain1 A f mf ay x
-          sc4 = record { supf = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = {!!} }  where
+          sc4 = record { supf = psup1 }  where
             psup1 : Ordinal → Ordinal
-            psup1 z with o≤? x z
-            ... | yes _ = spu
-            ... | no z<x = ZChain1.supf (pzc z (o¬≤→< z<x)) z
-            p≤z1 : (z : Ordinal ) → odef A (psup1 z)
-            p≤z1 z with o≤? x z
-            ... | yes _  = SUP.A∋maximal usup
-            ... | no z<x  = {!!} -- ZChain1.p≤z (pzc z (o¬≤→< z<x)) z
-            chainf1 : (z : Ordinal ) → HOD
-            chainf1 z with o≤? x z
-            ... | yes _  = record { od = record { def = λ w → odef A w ∧ FClosure A f spu w  } ; odmax = & A ; <odmax = {!!} }
-            ... | no z<x = {!!} -- ZChain1.chainf (pzc z (o¬≤→< z<x)) z
-            is-chain1 : (z w : Ordinal) → odef (chainf1 z) w → Chain A f mf ay {!!} (psup1 z ) w
-            is-chain1 z w lt with o≤? x z
-            ... | no z<x = {!!} -- ZChain1.is-chain (pzc z (o¬≤→< z<x)) z w ? ?
-            is-chain1 z w ⟪ ax , ux ⟫ | yes _ = ch-is-sup {!!} ux where
-                y<spu : y << spu
-                y<spu = {!!}
-                lty : y o< spu
-                lty = {!!}
-                aspu : odef A spu
-                aspu = SUP.A∋maximal usup
-                is-sup : (x1 w₁ : Ordinal) → x1 o< & (SUP.sup usup) → Chain A f mf ay {!!} x1 w₁ → w₁ << & (SUP.sup usup)
-                is-sup = {!!}
+            psup1 z with trio< z x 
+            ... | tri< a ¬b ¬c = ZChain1.supf (pzc z a) z
+            ... | tri≈ ¬a b ¬c = spu
+            ... | tri> ¬a ¬b c = spu
 
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
          → (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x) 
          → ((z : Ordinal) → z o< x → ZChain A f mf ay zc0 z) → ZChain A f mf ay zc0 x
-     ind f mf {y} ay x zc0 prev with Oprev-p x
+     ind f mf {y} ay x zc0 prev with trio< o∅ x
+     ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c )
+     ... | tri≈ ¬a x=0 ¬c = ?
+     ... | tri< 0<x ¬b ¬c with Oprev-p x
      ... | yes op = {!!} where
           --
           -- we have previous ordinal to use induction