Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 727:322dd6569072
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 18 Jul 2022 16:26:01 +0900 |
| parents | b2e2cd12e38f |
| children | e864471a818f |
| files | src/zorn.agda |
| diffstat | 1 files changed, 23 insertions(+), 128 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Jul 18 15:30:35 2022 +0900 +++ b/src/zorn.agda Mon Jul 18 16:26:01 2022 +0900 @@ -300,9 +300,6 @@ initial : {y : Ordinal } → odef chain y → * init ≤ * y f-next : {a : Ordinal } → odef chain a → odef chain (f a) f-total : IsTotalOrderSet chain - is-max : {a b : Ordinal } → (ca : odef chain a ) → b o< z → (ab : odef A b) - → HasPrev A chain ab f ∨ IsSup A chain ab - → * a < * b → odef chain b record Maximal ( A : HOD ) : Set (Level.suc n) where field @@ -310,14 +307,6 @@ A∋maximal : A ∋ maximal ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x -- A is Partial, use negative --- IsSup→Maximal : {A B : HOD} → {s : Ordinal } → ( B⊆A : B ⊆' A ) → ( bs : odef B s )→ IsSup A B (B⊆A bs) → Maximal A --- IsSup→Maximal {A} {B} {s} B⊆A bs is-sup --- = record { maximal = * s ; A∋maximal = subst (λ k → odef A k ) (sym &iso) (B⊆A bs) ; ¬maximal<x = is00 } where --- is00 : {z : HOD} → A ∋ z → ¬ (* s < z) --- is00 = ? - --- 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 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) @@ -421,6 +410,15 @@ 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) + ZChain-is-max :( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) + {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) → + {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) a ) → b o< & A → (ab : odef A b) + → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) (& A)) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) (& A)) ab + → * a < * b → odef ((UnionCF A f mf ay (ZChain.supf zc) (& A))) b + ZChain-is-max A f mf {y} ay zc {a} {b} ca b<a ab (case1 has-prev) a<b = + subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) k ) (sym (HasPrev.x=fy has-prev)) ( ZChain.f-next zc (HasPrev.ay has-prev) ) + ZChain-is-max A f mf {y} ay zc {a} {b} ca b<a ab (case2 is-sup) a<b = ? + --- --- the maximum chain has fix point of any ≤-monotonic function --- @@ -433,7 +431,7 @@ z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) → HasPrev A chain ab f ∨ IsSup A chain {b} ab -- (supO chain (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b ) → * a < * b → odef chain b - z10 = ZChain.is-max zc + z10 = ZChain-is-max A f mf as0 zc z11 : & (SUP.sup sp1) o< & A z11 = c<→o< ( SUP.A∋maximal sp1) z12 : odef chain (& (SUP.sup sp1)) @@ -561,20 +559,9 @@ -- if previous chain satisfies maximality, we caan reuse it -- - no-extension : ( {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → - HasPrev A pchain ab f ∨ IsSup A pchain ab → - * a < * b → odef pchain b ) → ZChain A f mf ay x - no-extension is-max = record { initial = pinit ; chain∋init = pcy - ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; is-max = is-max } - - zcp : {a b : Ordinal} → odef pchain a - → pchain ≡ UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) - → b o< px → (ab : odef A b) - → HasPrev A pchain ab f ∨ IsSup A pchain ab - → * a < * b → odef pchain b - zcp {a} {b} za cheq b<x ab P a<b = subst (λ k → odef k b ) (sym cheq) ( - ZChain.is-max zc (subst (λ k → odef k a) cheq za) b<x ab - (subst (λ k → HasPrev A k ab f ∨ IsSup A k ab ) cheq P) a<b ) + no-extension : ZChain A f mf ay x + no-extension = record { initial = pinit ; chain∋init = pcy + ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } chain-mono : UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) ⊆' pchain chain-mono {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za) ; u<x = zc11 ; uchain = UChain.uchain (proj2 za) } ⟫ where @@ -601,83 +588,15 @@ zc4 : ZChain A f mf ay x zc4 with ODC.∋-p O A (* px) - ... | no noapx = no-extension zc1 where -- ¬ A ∋ p, just skip - zc1 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → - HasPrev A pchain ab f ∨ IsSup A pchain ab → - * a < * b → odef pchain b - zc1 {a} {b} za b<x ab P a<b with trio< b px - ... | tri< lt ¬b ¬c = zcp za (chain-≡ (chain-x zc14)) lt ab P a<b where - zc14 : {z : Ordinal} (az : odef pchain z) → ¬ UChain.u (proj2 az) ≡ px - zc14 {z} ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ upx - = ⊥-elim ( noapx ( subst (λ k → odef A k ) (trans upx (sym &iso) ) (ChainP.au is-sup ) )) - ... | tri≈ ¬a b=px ¬c = ⊥-elim ( noapx (subst (λ k → odef A k ) (trans b=px (sym &iso)) ab ) ) - ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) + ... | no noapx = no-extension -- ¬ A ∋ p, just skip ... | yes apx with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) apx f ) -- we have to check adding x preserve is-max ZChain A y f mf x - ... | case1 pr = no-extension zc7 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next - zc7 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → - HasPrev A pchain ab f ∨ IsSup A pchain ab → - * a < * b → odef pchain b - zc7 {a} {b} za b<x ab P a<b with trio< b px - ... | tri< lt ¬b ¬c = zcp za (chain-≡ (chain-x zc14)) lt ab P a<b where - zc14 : {z : Ordinal} (az : odef pchain z) → ¬ UChain.u (proj2 az) ≡ px - zc14 {z} ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ upx - = ChainP.¬u=fx is-sup (subst (λ k → k ≡ _ ) (trans &iso (sym upx) ) (HasPrev.x=fy pr) ) - ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) - ... | tri≈ ¬a b=px ¬c = zc15 where - zc14 : f (HasPrev.y pr) ≡ b - zc14 = begin f (HasPrev.y pr) ≡⟨ sym (HasPrev.x=fy pr) ⟩ - & (* px) ≡⟨ &iso ⟩ - px ≡⟨ sym b=px ⟩ - b ∎ where open ≡-Reasoning - zc15 : odef pchain b - zc15 with ZChain.f-next zc (HasPrev.ay pr) - ... | ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫ - = ⟪ subst (λ k → odef A k ) zc14 az , record { u = u ; u<x = case2 refl - ; uchain = ch-init _ (subst (λ k → FClosure A f y k ) zc14 fc) } ⟫ - ... | ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ - = ⟪ subst (λ k → odef A k ) zc14 az , record { u = u ; u<x = case1 (b<x→0<x b<x ) - ; uchain = ch-init _ (subst (λ k → FClosure A f y k ) zc14 fc) } ⟫ + ... | 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 ) apx ) ... | case1 is-sup = -- x is a sup of zc record { chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal - ; initial = pinit ; chain∋init = pcy ; is-max = p-ismax } where - p-ismax : {a b : Ordinal} → odef pchain a → - b o< x → (ab : odef A b) → - ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) → - * a < * b → odef pchain b - p-ismax {a} {b} za b<x ab P a<b with trio< b px - ... | tri< lt ¬b ¬c = zcp za (chain-≡ ? ) lt ab P a<b - ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) - ... | tri≈ ¬a b=px ¬c with P - ... | case1 hasp = ? - ... | case2 sup = ? - ... | case2 ¬x=sup = no-extension z18 where -- px is not f y' nor sup of former ZChain from y -- no extention - z18 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → - HasPrev A pchain ab f ∨ IsSup A pchain ab → - * a < * b → odef pchain b - z18 {a} {b} za b<x ab P a<b with P - ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) ) - ... | case2 b=sup with trio< b px - ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) - ... | tri≈ ¬a b=px ¬c = ⊥-elim ( ¬x=sup record { - x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=px (sym &iso)) - (IsSup.x<sup b=sup (chain-mono zy) ) } ) - ... | tri< b<px ¬b ¬c = chain-mono (ZChain.is-max zc pa b<px ab (case2 record { x<sup = sup1 }) a<b) where - -- if b=sup and ¬ Isup>b , then b is Maximal - -- px o< sup (fc u) ∈ pchain contradicts b=sup ( x o< sup x ) - z19 : {z : Ordinal} (az : odef pchain z) → ¬ UChain.u (proj2 az) ≡ px - z19 {z} za@record {proj1 = az ; proj2 = record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } } - with trio< (UChain.u (proj2 za)) px - ... | tri> ¬a ¬b₁ c = ¬b₁ - ... | tri< a₁ ¬b₁ ¬c₁ = ¬b₁ - ... | tri≈ ¬a u=px ¬c₁ with IsSup.x<sup b=sup ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ - ... | case1 z=b = ? - ... | case2 z<b = ? - pa : odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) a - pa = chain-x z19 za - sup1 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) z → (z ≡ b) ∨ (z << b) - sup1 {z} uz = IsSup.x<sup b=sup ( chain-mono uz ) + ; initial = pinit ; chain∋init = pcy } + ... | case2 ¬x=sup = no-extension -- px is not f y' nor sup of former ZChain from y -- no extention ... | no op = zc5 where pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z @@ -699,9 +618,6 @@ ... | tri< a ¬b ¬c with o<-irr z<x a ... | refl = refl - psupf-mono : {z x1 : Ordinal} → (z<x1 : z o< x1) → x1 o≤ x → psupf0 z ≡ ZChain.supf (pzc z z<x1) z - psupf-mono {z} z<x1 x1≤x =? - 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) ) @@ -726,11 +642,9 @@ pcy : odef pchain y pcy = ⟪ ay , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay) } ⟫ - no-extension : ( {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → - HasPrev A pchain ab f ∨ IsSup A pchain ab → - * a < * b → odef pchain b ) → ZChain A f mf ay x - no-extension is-max = record { initial = pinit ; chain∋init = pcy - ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; is-max = is-max } + no-extension : ZChain A f mf ay x + no-extension = record { initial = pinit ; chain∋init = pcy + ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } usup : SUP A pchain usup = supP pchain (λ lt → proj1 lt) ptotal @@ -778,34 +692,15 @@ uzc00 : ChainP A f mf ay psupf0 u b uzc00 = ? - zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x) - ... | no noax = no-extension ? where -- ¬ A ∋ p, just skip + ... | no noax = no-extension where -- ¬ A ∋ p, just skip ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f ) -- we have to check adding x preserve is-max ZChain A y f mf x - ... | case1 pr = no-extension ? - -- subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) ) + ... | case1 pr = no-extension ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax ) ... | case1 is-sup = {!!} -- x is a sup of (zc ?) - ... | case2 ¬x=sup = no-extension z18 where -- x is not f y' nor sup of former ZChain from y -- no extention - z18 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → - HasPrev A pchain ab f ∨ IsSup A pchain ab → - * a < * b → odef pchain b - z18 {a} {b} za b<x ab P a<b with P - ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) ) - ... | case2 b=sup with za - ... | ⟪ aa , record { u = _ ; u<x = u<x ; uchain = ch-init .a fca } ⟫ = uzc-mono z30 where - ob<x : osuc b o< x - ob<x = ? - z30 : odef (UnionCF A f mf ay (ZChain.supf (prev (osuc b) ob<x))(osuc b)) b - z30 = ZChain.is-max (pzc _ ob<x) ⟪ aa , record { u = _ ; u<x = case2 refl ; uchain = ch-init a fca } ⟫ <-osuc ab (case1 ?) a<b - ... | ⟪ aa , record { u = u ; u<x = case2 u=0 ; uchain = ch-is-sup is-sup fc } ⟫ = ? - ... | ⟪ aa , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = uzc-mono z30 where - ob<x : osuc b o< x - ob<x = ? - z30 : odef (UnionCF A f mf ay (ZChain.supf (prev (osuc b) ob<x))(osuc b)) b - z30 = ZChain.is-max (pzc _ ob<x) ⟪ aa , record { u = u ; u<x = case1 ? ; uchain = ch-is-sup ? ? } ⟫ <-osuc ab (case1 ?) a<b + ... | case2 ¬x=sup = no-extension -- x is not f y' nor sup of former ZChain from y -- no extention SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A) SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) (& A)