Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 804:2d84411a636e
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 11 Aug 2022 14:07:57 +0900 |
| parents | 7c6612b753b9 |
| children | 9d97134d0a93 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 67 insertions(+), 65 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Aug 09 12:52:57 2022 +0900 +++ b/src/zorn.agda Thu Aug 11 14:07:57 2022 +0900 @@ -238,7 +238,7 @@ record SUP ( A B : HOD ) : Set (Level.suc n) where field sup : HOD - A∋maximal : A ∋ sup + as : A ∋ sup x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup ) -- B is Total, use positive -- @@ -328,7 +328,7 @@ record Maximal ( A : HOD ) : Set (Level.suc n) where field maximal : HOD - A∋maximal : A ∋ maximal + as : A ∋ maximal ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x -- A is Partial, use negative -- data UChain is total @@ -432,7 +432,7 @@ Gtx : { x : HOD} → A ∋ x → HOD Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = z07 } z08 : ¬ Maximal A → HasMaximal =h= od∅ - z08 nmx = record { eq→ = λ {x} lt → ⊥-elim ( nmx record {maximal = * x ; A∋maximal = subst (λ k → odef A k) (sym &iso) (proj1 lt) + z08 nmx = record { eq→ = λ {x} lt → ⊥-elim ( nmx record {maximal = * x ; as = subst (λ k → odef A k) (sym &iso) (proj1 lt) ; ¬maximal<x = λ {y} ay → subst (λ k → ¬ (* x < k)) *iso (proj2 lt (& y) ay) } ) ; eq← = λ {y} lt → ⊥-elim ( ¬x<0 lt )} x-is-maximal : ¬ Maximal A → {x : Ordinal} → (ax : odef A x) → & (Gtx (subst (λ k → odef A k ) (sym &iso) ax)) ≡ o∅ → (m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m)) x-is-maximal nmx {x} ax nogt m am = ⟪ subst (λ k → odef A k) &iso (subst (λ k → odef A k ) (sym &iso) ax) , ¬x<m ⟫ where @@ -559,17 +559,17 @@ → * a < * b → odef chain b z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) z11 : & (SUP.sup sp1) o< & A - z11 = c<→o< ( SUP.A∋maximal sp1) + z11 = c<→o< ( SUP.as sp1) z12 : odef chain (& (SUP.sup sp1)) z12 with o≡? (& s) (& (SUP.sup sp1)) ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) - ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z11 (SUP.A∋maximal sp1) + ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z11 (SUP.as sp1) (case2 z19 ) z13 where z13 : * (& s) < * (& (SUP.sup sp1)) z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc ) ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt - z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.A∋maximal sp1) + z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1) z19 = record { x<sup = z20 } where z20 : {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1)) z20 {y} zy with SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) zy) @@ -580,7 +580,7 @@ z14 with total (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 ... | tri< a ¬b ¬c = ⊥-elim z16 where z16 : ⊥ - z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 )) + z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 )) ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) )) ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt )) ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b ) @@ -600,10 +600,10 @@ z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥ - z04 nmx 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) ) + z04 nmx zc total = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as sp1 )))) + (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) ) (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc total ))) -- x ≡ f x ̄ - (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1 ))) where -- x < f x + (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x sp1 : SUP A (ZChain.chain zc) sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total c = & (SUP.sup sp1) @@ -622,48 +622,8 @@ → SUP A (uchain f mf ay) ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt) (utotal f mf ay) - initChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅ - initChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; sup = {!!} ; supf-is-sup = {!!} - ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ? ; csupf = {!!} } where - spi = & (SUP.sup (ysup f mf ay)) - isupf : Ordinal → Ordinal - isupf z = spi - sp = ysup f mf ay - asi = SUP.A∋maximal sp - cy : odef (UnionCF A f mf ay isupf o∅) y - cy = ⟪ ay , ch-init (init ay refl) ⟫ - y<sup : * y ≤ SUP.sup (ysup f mf ay) - y<sup = SUP.x<sup (ysup f mf ay) (subst (λ k → FClosure A f y k ) (sym &iso) (init ay refl)) - sup : {x : Ordinal} → x o< o∅ → SUP A (UnionCF A f mf ay isupf x) - sup {x} lt = ⊥-elim ( ¬x<0 lt ) - isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z - isy {z} ⟪ az , uz ⟫ with uz - ... | ch-init fc = s≤fc y f mf fc - ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup) (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc ) - inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a) - inext {a} ua with (proj2 ua) - ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-init (fsuc _ fc ) ⟫ - ... | ch-is-sup u u≤x is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ - itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) - itotal {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 isupf (proj2 ca) (proj2 cb) - csupf : {z : Ordinal} → z o≤ o∅ → odef (UnionCF A f mf ay isupf z ) (isupf z) - csupf {z} z≤0 = ⟪ asi , ch-is-sup o∅ o∅≤z uz02 (init asi refl) ⟫ where - uz03 : {z : Ordinal } → FClosure A f y z → (z ≡ isupf spi) ∨ (z << isupf spi) - uz03 {z} fc with SUP.x<sup sp (subst (λ k → FClosure A f y k ) (sym &iso) fc ) - ... | case1 eq = case1 ( begin - z ≡⟨ sym &iso ⟩ - & (* z) ≡⟨ cong (&) eq ⟩ - spi ∎ ) where open ≡-Reasoning - ... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt ) - uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi) - uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi ) - uz02 : ChainP A f mf ay isupf o∅ - uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → {!!} ; supu=u = {!!} } - SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B - SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; A∋maximal = SUP.A∋maximal sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt) } + SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt) } -- -- create all ZChains under o< x @@ -732,15 +692,33 @@ -- if previous chain satisfies maximality, we caan reuse it -- -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x - no-extension : ¬ sp1 ≡ x → ZChain A f mf ay x + no-extension : ¬ sp1 ≡ supf1 x → ZChain A f mf ay x no-extension ¬sp=x = record { supf = supf1 ; sup = sup - ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = {!!} ; csupf = {!!} - ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = {!!} } where + ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = {!!} ; csupf = csupf + ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = ptotal1 } where UnionCF⊆ : {z : Ordinal } → z o≤ x → UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay supf0 x UnionCF⊆ {z} z≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ - UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫ - UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with - UnionCF⊆ {z} z≤x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ + UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤z record { fcy<sup = fc<s ; order = o1 ; supu=u = sp=u } (init au1 refl) ⟫ = zc30 where + zc30 : odef (UnionCF A f mf ay supf0 x) (supf1 u1 ) + zc30 with trio< u1 px + ... | tri< a ¬b ¬c = ⟪ au , ch-is-sup u1 (OrdTrans u1≤z z≤x) ? (init au1 refl) ⟫ + ... | tri≈ ¬a b ¬c = ⟪ au , ch-is-sup u1 (OrdTrans u1≤z z≤x) ? (init au1 refl) ⟫ + ... | tri> ¬a ¬b px<u1 = ? where + zc31 : u1 ≡ x + zc31 with trio< u1 x + ... | tri< a ¬b ¬c = ⊥-elim (¬p<x<op ⟪ px<u1 , subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) a ⟫ ) + ... | tri≈ ¬a b ¬c = b + ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , ordtrans≤-< u1≤z z≤x ⟫ ) + UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤z u1-is-sup (fsuc xp fcu1) ⟫ with + UnionCF⊆ {z} z≤x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤z u1-is-sup fcu1 ⟫ + ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ + ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ + UnionCF⊆R : {z : Ordinal } → z o≤ x → UnionCF A f mf ay supf0 z ⊆' UnionCF A f mf ay supf1 x + UnionCF⊆R {z} z≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ + UnionCF⊆R {z} z≤x ⟪ au , ch-is-sup u1 u1≤z u1-is-sup (init au1 refl) ⟫ + = ⟪ au , ch-is-sup u1 (OrdTrans u1≤z z≤x) ? (init ? ?) ⟫ + UnionCF⊆R {z} z≤x ⟪ au , ch-is-sup u1 u1≤z u1-is-sup (fsuc xp fcu1) ⟫ with + UnionCF⊆R {z} z≤x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤z u1-is-sup fcu1 ⟫ ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) @@ -755,7 +733,21 @@ zc11 = ZChain.sup=u zc ab ? ? ... | tri≈ ¬a b ¬c = ? ... | tri> ¬a ¬b c = ? - + ptotal1 : IsTotalOrderSet pchain1 + ptotal1 {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)) + csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b) + csupf {b} b≤x with trio< b px | inspect supf1 b + ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫ + ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫ + ... | tri> ¬a ¬b px<b | record { eq = eq1 } = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ supf1 k ) (sym zc30) (sym eq1) )) where + -- px< b ≤ x + -- b ≡ x, supf x ≡ sp1 , ¬ x ≡ sp1 + zc30 : x ≡ b + zc30 with osuc-≡< b≤x + ... | case1 eq = sym (eq) + ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) zc4 : ZChain A f mf ay x zc4 with ODC.∋-p O A (* x) ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip @@ -764,10 +756,10 @@ ... | case1 pr = no-extension {!!} -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax ) ... | case1 is-sup = -- x is a sup of zc - record { supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} + record { supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = csupf ; sup=u = {!!} ; initial = {!!} ; chain∋init = {!!} ; sup = {!!} ; supf-is-sup = {!!} } where supx : SUP A (UnionCF A f mf ay supf0 x) - supx = record { sup = * x ; A∋maximal = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} } + supx = record { sup = * x ; as = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} } spx = & (SUP.sup supx ) x=spx : x ≡ spx x=spx = {!!} @@ -776,6 +768,16 @@ ... | tri< a ¬b ¬c = ZChain.supf zc z ... | tri≈ ¬a b ¬c = x ... | tri> ¬a ¬b c = x + csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay psupf1 b) (psupf1 b) + csupf {b} b≤x with trio< b px | inspect psupf1 b + ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫ + ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫ + ... | tri> ¬a ¬b c | record { eq = eq1 } = ? where -- b ≡ x, supf x ≡ sp + zc30 : x ≡ b + zc30 with trio< x b + ... | tri< a ¬b ¬c = ? + ... | tri≈ ¬a b ¬c = b + ... | tri> ¬a ¬b c = ? ... | case2 ¬x=sup = no-extension {!!} -- px is not f y' nor sup of former ZChain from y -- no extention @@ -879,14 +881,14 @@ ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b c = {!!} csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z) - csupf {z} z<x with trio< z x + csupf {z} z≤x with trio< z x ... | tri< a ¬b ¬c = zc9 where zc9 : odef (UnionCF A f mf ay supf1 z) (ZChain.supf (pzc (osuc z) (ob<x lim a)) z) zc9 = {!!} zc8 : odef (UnionCF A f mf ay (supfu a) z) (ZChain.supf (pzc (osuc z) (ob<x lim a)) z) zc8 = ZChain.csupf (pzc (osuc z) (ob<x lim a)) (o<→≤ <-osuc ) - ... | tri≈ ¬a b ¬c = {!!} -- ⊥-elim (¬a z<x) - ... | tri> ¬a ¬b c = {!!} -- ⊥-elim (¬a z<x) + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x)) zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x) @@ -905,7 +907,7 @@ 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 + ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x = zorn02 } where -- yes we have the maximal zorn03 : odef HasMaximal ( & ( ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) ) zorn03 = ODC.x∋minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) -- Axiom of choice @@ -918,7 +920,7 @@ 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) ) ⟫ + zc5 = ⟪ Maximal.as mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫ zorn04 : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A) zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) total : IsTotalOrderSet (ZChain.chain zorn04)