Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 721:562ddd33fe21
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 16 Jul 2022 04:05:18 +0900 |
| parents | 6c9fed204440 |
| children | 0dd8cc755ec9 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 58 insertions(+), 59 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sat Jul 16 00:45:38 2022 +0900 +++ b/src/zorn.agda Sat Jul 16 04:05:18 2022 +0900 @@ -252,6 +252,7 @@ field y-init : supf o∅ ≡ y au : odef A u + ¬u=fx : {x : Ordinal} → ¬ ( u ≡ f x ) asup : (x : Ordinal) → odef A (supf x) fcy<sup : {z : Ordinal } → FClosure A f y z → z << supf u csupz : FClosure A f (supf u) z @@ -548,10 +549,10 @@ -- if previous chain satisfies maximality, we caan reuse it -- - no-extenion : ( {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → + 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-extenion is-max = record { initial = pinit ; chain∋init = pcy + 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 @@ -574,60 +575,42 @@ → pchain ≡ UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono } - zc11 : ( {z : Ordinal} → (az : odef pchain z) → ¬ ( UChain.u (proj2 az) ≡ px )) → pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) px - zc11 ne {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = + chain-x : ( {z : Ordinal} → (az : odef pchain z) → ¬ ( UChain.u (proj2 az) ≡ px )) → pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) px + chain-x ne {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ - zc11 ne {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ with trio< o∅ px + chain-x ne {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ with trio< o∅ px ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-init z fc } ⟫ ... | tri≈ ¬a b ¬c = ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫ ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) - zc11 ne {z} uz@record { proj1 = az ; proj2 = record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } } with trio< u px + chain-x ne {z} uz@record { proj1 = az ; proj2 = record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } } with trio< u px ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ ... | tri≈ ¬a b ¬c = ⊥-elim ( ne uz b ) ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) zc4 : ZChain A f mf ay x zc4 with ODC.∋-p O A (* px) - ... | no noapx = no-extenion zc1 where -- ¬ A ∋ p, just skip + ... | 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-≡ zc10) lt ab P a<b where - zc10 : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op) - zc10 {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = - ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ - zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ with trio< o∅ px - ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-init z fc } ⟫ - ... | tri≈ ¬a b ¬c = ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫ - ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) - zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ with trio< u px - ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ - ... | tri≈ ¬a b ¬c = ⊥-elim ( noapx ( subst (λ k → odef A k ) (trans b (sym &iso) ) (ChainP.au is-sup ) )) - ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) + ... | 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 ⟫ ) ... | 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-extenion zc7 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next + ... | 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-≡ zc10) lt ab P a<b where - zc10 : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op) - zc10 {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = - ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ - zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ with trio< o∅ px - ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-init z fc } ⟫ - ... | tri≈ ¬a b ¬c = ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫ - ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) - zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ with trio< u px - ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ - ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) - ... | tri≈ ¬a b ¬c = ? where - zc13 : odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) (HasPrev.y pr) - zc13 = HasPrev.ay pr + ... | 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 @@ -657,20 +640,30 @@ ... | tri≈ ¬a b=px ¬c with P ... | case1 hasp = ? ... | case2 sup = ? - ... | case2 ¬x=sup = no-extenion z18 where -- px is not f y' nor sup of former ZChain from y -- no extention + ... | 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 trio< b px - ... | tri< lt ¬b ¬c = ? where - z20 : odef pchain b - z20 = chain-mono ( ZChain.is-max zc ? lt ab ? a<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 with P - ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) ) - ... | case2 b=sup = ⊥-elim ( ¬x=sup record { - x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=px (sym &iso)) + ... | 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 + 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 ) ... | no op = zc5 where pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z pzc z z<x = prev z z<x @@ -705,10 +698,10 @@ pcy : odef pchain y pcy = ⟪ ay , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay) } ⟫ - no-extenion : ( {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → + 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-extenion is-max = record { initial = pinit ; chain∋init = pcy + no-extension is-max = record { initial = pinit ; chain∋init = pcy ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; is-max = is-max } usup : SUP A pchain @@ -740,11 +733,15 @@ -- ZChain.is-max (uzc za) ? ? ab (subst (λ k → HasPrev A k ab f ∨ IsSup A k ab ) cheq P) a<b chain-mono : pchain ⊆' UnionCF A f mf ay psupf x - chain-mono {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za) ; u<x = UChain.u<x (proj2 za) ; uchain = zc11 } ⟫ where - zc11 : Chain A f mf ay psupf (UChain.u (proj2 za)) a - zc11 with UChain.uchain (proj2 za) - ... | ch-init .a x = ch-init a x - ... | ch-is-sup is-sup fc = ch-is-sup ? (subst (λ k → FClosure A f k a ) ? fc ) + chain-mono {a} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ = + ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ + chain-mono {.(psupf0 u)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (init x) } ⟫ = + ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup ? ? } ⟫ + chain-mono {.(f x)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (fsuc x fc) } ⟫ = + ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup ? (fsuc x ?) } ⟫ + + chain-x : {z : Ordinal } → ¬ ( z << spu ) → odef (UnionCF A f mf ay psupf x) z → odef pchain z + chain-x = ? chain-≡ : UnionCF A f mf ay psupf x ⊆' pchain → UnionCF A f mf ay psupf x ≡ pchain @@ -752,23 +749,25 @@ zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x) - ... | no noax = no-extenion ? 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 = {!!} where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next + ... | case1 pr = no-extension ? + -- subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) ) ... | 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-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention + ... | 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 osuc-≡< ? - ... | case2 lt = zcp za ? lt ab P a<b - ... | case1 b=x with P + 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 = ⊥-elim ( ¬x=sup record { - x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) - (IsSup.x<sup b=sup ? ) } ) + ... | case2 b=sup = ? where + z30 = ZChain.is-max (uzc za) ? ? ab (case2 ?) a<b + + --⊥-elim ( ¬x=sup record { + -- x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) ? + -- (IsSup.x<sup b=sup ? ) } ) SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A)