Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 1069:99df080f4fdb

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Tue, 13 Dec 2022 09:31:11 +0900
parents	f24f4de4d459
children	33d601c9ee96

comparison

equal deleted inserted replaced

-:f24f4de4d459
+:99df080f4fdb
 mf00 : * x < * (f x)
 mf00 = proj1 ( mf< x ax )
 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? ; 0<supfz = ?
 ; zo≤sz = ?   ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs    }  where
--- mf : ≤-monotonic-f A f
--- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫  will result memory exhaust
 mf : ≤-monotonic-f A f
 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
 mf00 : * x < * (f x)
 mf00 = proj1 ( mf< x ax )
 ysp =  MinSUP.sup (ysup f mf ay)
 supfz : {z : Ordinal } → z o< x → Ordinal
 supfz {z} z<x = ZChain.supf (pzc  (ob<x lim z<x)) z
-pchainx : HOD
+pchainU : HOD
-pchainx = UnionIC A f ay supfz
+pchainU = UnionIC A f ay supfz
 zeq : {xa xb z : Ordinal }
 → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa
 → ZChain.supf (pzc  xa<x) z ≡  ZChain.supf (pzc  xb<x) z
 zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa =  supf-unique A f mf< ay xa≤xb
 pic<x : {z : Ordinal } → (ic : IChain ay supfz z ) → osuc (IChain-i ic) o< x
 pic<x {z} (ic-init fc) = ob<x lim 0<x   -- 0<x ∧ lim x → osuc o∅ o< x
 pic<x {z} (ic-isup ia ia<x sa<x fca) = ob<x lim ia<x
-pchainx⊆chain : {z : Ordinal } → (pz : odef pchainx z) → odef (ZChain.chain (pzc (pic<x (proj2 pz)))) z
+pchainU⊆chain : {z : Ordinal } → (pz : odef pchainU z) → odef (ZChain.chain (pzc (pic<x (proj2 pz)))) z
-pchainx⊆chain {z} ⟪ aw , ic-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+pchainU⊆chain {z} ⟪ aw , ic-init fc ⟫ = ⟪ aw , ch-init fc ⟫
-pchainx⊆chain {z} ⟪ aw , (ic-isup ia ia<x sa<x fca) ⟫ = ZChain.cfcs (pzc (ob<x lim ia<x) ) <-osuc o≤-refl uz03 fca where
+pchainU⊆chain {z} ⟪ aw , (ic-isup ia ia<x sa<x fca) ⟫ = ZChain.cfcs (pzc (ob<x lim ia<x) ) <-osuc o≤-refl uz03 fca where
 uz02 : FClosure A f (ZChain.supf (pzc (ob<x lim ia<x)) ia ) z
 uz02 = fca
 uz03 : ZChain.supf (pzc (ob<x lim ia<x)) ia o≤ ia
 uz03 = sa<x
-chain⊆pchainx : {z w : Ordinal } → (oz<x : osuc z o< x) → odef (ZChain.chain (pzc oz<x)) w → odef pchainx w
+chain⊆pchainU : {z w : Ordinal } → (oz<x : osuc z o< x) → odef (ZChain.chain (pzc oz<x)) w → odef pchainU w
-chain⊆pchainx {z} {w} oz<x ⟪ aw , ch-init fc ⟫ = ⟪ aw , ic-init fc ⟫
+chain⊆pchainU {z} {w} oz<x ⟪ aw , ch-init fc ⟫ = ⟪ aw , ic-init fc ⟫
-chain⊆pchainx {z} {w} oz<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫
+chain⊆pchainU {z} {w} oz<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫
 = ⟪ aw , ic-isup u u<x (o≤-refl0 su≡u) (subst (λ  k → FClosure A f k w ) su=su fc) ⟫ where
 u<x : u o< x
 u<x = ordtrans u<oz oz<x
 su=su : ZChain.supf (pzc oz<x) u ≡ supfz u<x
 su=su = sym ( zeq _ _  (osucc u<oz) (o<→≤ <-osuc) )
 ic01 = ordtrans<-≤ ic02 sa<x
 IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-isup j j<x sb<x fcb ) ia≤ib
 = ZChain.cfcs (pzc (ob<x lim j<x) ) ia≤ib o≤-refl (OrdTrans (ZChain.supf-mono (pzc (ob<x lim j<x)) ia≤ib) sb<x)
 (subst (λ k → FClosure A f k a) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc)) fc )
-ptotalx : IsTotalOrderSet pchainx
+ptotalU : IsTotalOrderSet pchainU
-ptotalx {a} {b} ia ib with trio< (IChain-i (proj2 ia)) (IChain-i (proj2 ib))
+ptotalU {a} {b} ia ib with trio< (IChain-i (proj2 ia)) (IChain-i (proj2 ib))
-... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o<→≤ ia<ib)) (pchainx⊆chain ib)
+... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o<→≤ ia<ib)) (pchainU⊆chain ib)
-... | tri≈ ¬a ia=ib ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o≤-refl0 ia=ib)) (pchainx⊆chain ib)
+... | tri≈ ¬a ia=ib ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o≤-refl0 ia=ib)) (pchainU⊆chain ib)
-... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) (o<→≤ ib<ia))
+... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainU⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) (o<→≤ ib<ia))
-usup : MinSUP A pchainx
+usup : MinSUP A pchainU
-usup = minsupP pchainx (λ ic → ? ) ptotalx
+usup = minsupP pchainU (λ ic → proj1 ic ) ptotalU
 spu = MinSUP.sup usup
+pchainS : HOD
+pchainS = record { od = record { def = λ z →  (odef A z  ∧ IChain  ay supfz z )
+∨ (FClosure A f spu z ∧ (spu o< x)) } ; odmax = & A ; <odmax = zc00 } where
+zc00 : {z : Ordinal } → (odef A z ∧ IChain ay supfz z ) ∨ (FClosure A f spu z ∧ (spu o< x) )→ z o< & A
+zc00 {z} (case1 lt) = z07 lt
+zc00 {z} (case2 fc) = z09 ( A∋fc spu f mf (proj1 fc) )
+zc02 : { a b : Ordinal } → odef A a ∧ IChain ay supfz a → FClosure A f spu b ∧ ( spu o< x) → a ≤ b
+zc02 {a} {b} ca fb = zc05 (proj1 fb) where
+zc05 : {b : Ordinal } → FClosure A f spu b → a ≤ b
+zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc spu f mf fb ))
+... | case1 eq = subst (λ k → a ≤ k ) eq (zc05 fb)
+... | case2 lt = ≤-ftrans (zc05 fb) (case2 lt)
+zc05 (init b1 refl) = MinSUP.x≤sup usup ca
+ptotalS : IsTotalOrderSet pchainS
+ptotalS (case1 a) (case1 b) =  ptotalU a b
+ptotalS {a0} {b0} (case1 a) (case2 b) with zc02 a b
+... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where
+eq1 : a0 ≡ b0
+eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where
+lt1 : a0 < b0
+lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
+ptotalS {b0} {a0} (case2 b) (case1 a) with zc02 a b
+... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where
+eq1 : a0 ≡ b0
+eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1  where
+lt1 : a0 < b0
+lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
+ptotalS (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp spu f mf (proj1 a) (proj1 b))
+S⊆A : pchainS ⊆' A
+S⊆A (case1 lt) = proj1 lt
+S⊆A (case2 fc) = A∋fc _ f mf (proj1 fc)
+ssup : MinSUP A pchainS
+ssup = minsupP pchainS S⊆A ptotalS
+sps = MinSUP.sup ssup
 supf1 : Ordinal → Ordinal
 supf1 z with trio< z x
-... | tri< a ¬b ¬c = ZChain.supf (pzc  (ob<x lim a)) z
+... | tri< a ¬b ¬c = ZChain.supf (pzc  (ob<x lim a)) z   -- each sup o< x
-... | tri≈ ¬a b ¬c = spu
+... | tri≈ ¬a b ¬c = spu                                 -- sup of all sup o< x
-... | tri> ¬a ¬b c = spu
+... | tri> ¬a ¬b c = sps                                 -- sup of spu which o< x
+--  if x o< spu, spu is not included in UnionCF x
+-- the chain
 pchain : HOD
 pchain = UnionCF A f ay supf1 x
--- pchain ⊆ pchainx
+-- pchain ⊆ pchainU ⊆ pchianS
-ptotal : IsTotalOrderSet pchain
-ptotal {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 supf1 ( (proj2 ca)) ( (proj2 cb))
 sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc  (ob<x lim a)) z
 sf1=sf {z} z<x with trio< z x
 ... | tri< a ¬b ¬c = cong ( λ k → ZChain.supf (pzc (ob<x lim k)) z) o<-irr
 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x)
 ... | tri> ¬a ¬b c = ⊥-elim (¬a z<x)
-sf1=spu : {z : Ordinal } → (a : x o≤ z ) → supf1 z ≡ spu
+sf1=spu : {z : Ordinal } → (a : x o≤ z ) → spu o< x → supf1 z ≡ spu
-sf1=spu {z} x≤z with trio< z x
+sf1=spu {z} x≤z s<x with trio< z x
 ... | tri< a ¬b ¬c = ⊥-elim (o≤> x≤z a)
 ... | tri≈ ¬a b ¬c = refl
-... | tri> ¬a ¬b c = refl
+... | tri> ¬a ¬b c = ?
-zc11 : {z : Ordinal } → odef pchain z → odef pchainx z
+sf1=sps : {z : Ordinal } → (a : x o≤ z ) → x o≤ spu → supf1 z ≡ sps
+sf1=sps {z} x≤z x≤s with trio< z x
+... | tri< a ¬b ¬c = ⊥-elim (o≤> x≤z a)
+... | tri≈ ¬a b ¬c = ?
+... | tri> ¬a ¬b c = ?
+zc11 : {z : Ordinal } → odef pchain z → odef pchainS z
 zc11 {z} lt = ?
-sfpx≤spu : {z : Ordinal } → supf1 z ≤ spu
+sfpx≤spu : {z : Ordinal } → supf1 z ≤ sps
 sfpx≤spu {z} with trio< z x
-... | tri< a ¬b ¬c = MinSUP.x≤sup usup ? -- (init (ZChain.asupf (pzc  (ob<x lim a)) ) refl )
+... | tri< a ¬b ¬c = ? -- MinSUP.x≤sup usup ? -- (init (ZChain.asupf (pzc  (ob<x lim a)) ) refl )
-... | tri≈ ¬a b ¬c = case1 refl
+... | tri≈ ¬a b ¬c = case1 ?
-... | tri> ¬a ¬b c = case1 refl
+... | tri> ¬a ¬b c = case1 ?
-sfpxo≤spu : {z : Ordinal } → supf1 z o≤ spu
+sfpxo≤spu : {z : Ordinal } → supf1 z o≤ sps
 sfpxo≤spu {z} with trio< z x
 ... | tri< a ¬b ¬c = ? -- MinSUP.x≤sup usup ? -- (init (ZChain.asupf (pzc  (ob<x lim a)) ) refl )
 ... | tri≈ ¬a b ¬c = o≤-refl0 ?
 ... | tri> ¬a ¬b c = o≤-refl0 ?
 asupf : {z : Ordinal } → odef A (supf1 z)
 asupf {z} with trio< z x
 ... | tri< a ¬b ¬c = ZChain.asupf (pzc  (ob<x lim a))
 ... | tri≈ ¬a b ¬c = MinSUP.as usup
-... | tri> ¬a ¬b c = MinSUP.as usup
+... | tri> ¬a ¬b c = MinSUP.as ssup
 supfmax : {z : Ordinal } → x o< z → supf1 z ≡ supf1 x
 supfmax {z} x<z with trio< z x
 ... | tri< a ¬b ¬c = ⊥-elim (o<> a x<z)
 ... | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (sym b) x<z)
-... | tri> ¬a ¬b c = sym (sf1=spu o≤-refl)
+... | tri> ¬a ¬b c = sym ? -- (sf1=sps o≤-refl)
 supf-mono : {z y : Ordinal } → z o≤ y → supf1 z o≤ supf1 y
 supf-mono {z} {y} z≤y with trio< y x
 ... | tri< y<x ¬b ¬c = ? where
 open o≤-Reasoning O
 z13 :  * (& s) < * sp
 z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
 ... | case1 eq = ⊥-elim ( ne eq )
 ... | case2 lt = lt
 z19 : IsSUP A (UnionCF A f ay (ZChain.supf zc) sp) sp
-z19 = record { ax = ? ;   x≤sup = z20 }  where
+z19 = record { ax = asp ;   x≤sup = z20 }  where
 z20 : {y : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)
 z20 {y} zy with MinSUP.x≤sup sp1
 (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22)  zy ))
 ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p )
 ... | case2 y<p = case2 (subst (λ k → * k < _ ) &iso y<p )

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

comparison src/zorn.agda @ 1069:99df080f4fdb