Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 935:ed711d7be191
mem exhaust fix on fixpoint
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 24 Oct 2022 16:06:18 +0900 |
| parents | ebcad8e5ae55 |
| children | f160556a7c9a |
| files | src/zorn.agda |
| diffstat | 1 files changed, 26 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Oct 24 09:36:07 2022 +0900 +++ b/src/zorn.agda Mon Oct 24 16:06:18 2022 +0900 @@ -1349,43 +1349,46 @@ sp0 f mf ay zc = M→S (ZChain.supf zc) (msp0 f mf ay zc ) fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) - → ZChain.supf zc (& (SUP.sup (sp0 f mf as0 zc))) o< ZChain.supf zc (& A) - → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) - fixpoint f mf zc ss<sa = z14 where + → (sp1 : SUP A (ZChain.chain zc)) -- & (SUP.sup (sp0 f mf as0 zc )) + → (ssp<as : ZChain.supf zc (& (SUP.sup sp1)) o< ZChain.supf zc (& A)) + → f (& (SUP.sup sp1)) ≡ & (SUP.sup sp1) + fixpoint f mf zc sp1 ssp<as = z14 where chain = ZChain.chain zc supf = ZChain.supf zc - sp1 : SUP A chain - sp1 = sp0 f mf as0 zc + sp : Ordinal + sp = & (SUP.sup sp1) + asp : odef A sp + asp = SUP.as sp1 z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) → HasPrev A chain b f ∨ IsSup A chain {b} ab → * a < * b → odef chain b z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) - z22 : & (SUP.sup sp1) o< & A - z22 = c<→o< ( SUP.as sp1 ) - z21 : supf (& (SUP.sup sp1)) o< supf (& A) - z21 = ss<sa - -- z21 : supf (& (SUP.sup sp1)) o< & A - -- z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) )) - z12 : odef chain (& (SUP.sup sp1)) - z12 with o≡? (& s) (& (SUP.sup sp1)) + z22 : sp o< & A + z22 = z09 asp + x<sup : {x : HOD} → chain ∋ x → (x ≡ SUP.sup sp1 ) ∨ (x < SUP.sup sp1 ) + x<sup bz with SUP.x<sup sp1 bz + ... | case1 eq = case1 ? + ... | case2 lt = case2 ? + z12 : odef chain sp + z12 with o≡? (& s) sp ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) - ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1) + ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp (case2 z19 ) z13 where - z13 : * (& s) < * (& (SUP.sup sp1)) - z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc ) + z13 : * (& s) < * sp + z13 with x<sup ( 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.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) + z20 {y} zy with x<sup (subst (λ k → odef chain k ) (sym &iso) zy) ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p )) ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) ztotal : IsTotalOrderSet (ZChain.chain zc) ztotal {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 as0 supf ( (proj2 ca)) ( (proj2 cb)) - z14 : f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) + z14 : f sp ≡ sp z14 with ztotal (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 ... | tri< a ¬b ¬c = ⊥-elim z16 where z16 : ⊥ @@ -1394,12 +1397,12 @@ ... | 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 ) ... | tri> ¬a ¬b c = ⊥-elim z17 where - z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1) - z15 = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 )) + z15 : (* (f sp) ≡ SUP.sup sp1) ∨ (* (f sp) < * sp ) + z15 = ? -- x<sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 )) z17 : ⊥ z17 with z15 ... | case1 eq = ¬b eq - ... | case2 lt = ¬a lt + ... | case2 lt = ¬a ? -- ZChain contradicts ¬ Maximal @@ -1411,7 +1414,8 @@ z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥ z04 nmx zc = <-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 ss<sa ))) -- x ≡ f x ̄ + (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc + (sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc ) ss<sa ))) -- x ≡ f x ̄ (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x supf = ZChain.supf zc msp1 : MinSUP A (ZChain.chain zc)