Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 959:1ef03eedd148
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 04 Nov 2022 08:17:21 +0900 |
| parents | 33891adf80ea |
| children | b7370c39769e |
| files | src/zorn.agda |
| diffstat | 1 files changed, 38 insertions(+), 47 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Nov 04 06:47:23 2022 +0900 +++ b/src/zorn.agda Fri Nov 04 08:17:21 2022 +0900 @@ -668,15 +668,11 @@ chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) - ⟪ record { x≤sup = λ {z} uz → IsMinSup.x≤sup (proj2 is-sup) ? -- (chain-mono1 (o<→≤ b<x) uz) - ; minsup = m07 } , m04 ⟫ where - m10 : {s : Ordinal } → (odef A s ) - → ( {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s) ) - → {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s) - m10 = ? + ⟪ record { x≤sup = λ {z} uz → IsMinSup.x≤sup (proj2 is-sup) uz + ; minsup = m07 ; not-hp = m04 } , m04 ⟫ where m07 : {s : Ordinal} → odef A s → ({z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s)) → b o≤ s - m07 {s} as s-is-sup = ? -- IsSup.minsup (proj2 is-sup) as (m10 as s-is-sup) + m07 {s} as s-is-sup = IsMinSup.minsup (proj2 is-sup) as s-is-sup m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b @@ -709,8 +705,8 @@ ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b m05 = ZChain.sup=u zc ab (o<→≤ m09) - ⟪ record { x≤sup = λ lt → IsMinSup.x≤sup (proj2 is-sup) ? -- (chain-mono1 (o<→≤ b<x) lt ) - ; minsup = ? } , m04 ⟫ -- ZChain on x + ⟪ record { x≤sup = λ lt → IsMinSup.x≤sup (proj2 is-sup) lt + ; minsup = IsMinSup.minsup (proj2 is-sup) ; not-hp = m04 } , m04 ⟫ -- ZChain on x m06 : ChainP A f mf ay supf b m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = m05 } @@ -1356,30 +1352,27 @@ uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) - sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) - → (zc : ZChain A f mf ay x ) - → SUP A (UnionCF A f mf ay (ZChain.supf zc) x) - 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) ) - → (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) + → (sp1 : MinSUP A (ZChain.chain zc)) -- & (SUP.sup (sp0 f mf as0 zc )) + → (ssp<as : ZChain.supf zc (MinSUP.sup sp1) o< ZChain.supf zc (& A)) + → f (MinSUP.sup sp1) ≡ MinSUP.sup sp1 fixpoint f mf zc sp1 ssp<as = z14 where chain = ZChain.chain zc supf = ZChain.supf zc sp : Ordinal - sp = & (SUP.sup sp1) + sp = MinSUP.sup sp1 asp : odef A sp - asp = SUP.as sp1 + asp = MinSUP.asm sp1 z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) → HasPrev A chain f b ∨ IsMinSup A (UnionCF A f mf ab (ZChain.supf zc) b) f ab → * a < * b → odef chain b z10 = ? -- ZChain1.is-max (SZ1 f mf as0 zc (& A) ) z22 : sp o< & A z22 = z09 asp - x≤sup : {x : HOD} → chain ∋ x → (x ≡ SUP.sup sp1 ) ∨ (x < SUP.sup sp1 ) - x≤sup bz = SUP.x≤sup sp1 bz + x≤sup : {x : HOD} → chain ∋ x → (& x ≡ sp ) ∨ (x < * sp ) + x≤sup bz with MinSUP.x≤sup sp1 bz + ... | case1 eq = ? + ... | case2 lt = ? z12 : odef chain sp z12 with o≡? (& s) sp ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) @@ -1387,33 +1380,33 @@ (case2 z19 ) z13 where 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 + ... | case1 eq = ⊥-elim ( ne ? ) + ... | case2 lt = ? -- subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt z19 : IsMinSup A (UnionCF A f mf as0 (ZChain.supf zc) sp) f asp - z19 = record { x≤sup = ? ; minsup = ? } where - z20 : {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1)) - 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 ) + z19 = record { x≤sup = z20 ; minsup = ? ; not-hp = ? } where + z20 : {y : Ordinal} → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp) + z20 {y} zy with x≤sup (subst (λ k → odef chain k ) (sym &iso) ?) + ... | 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 sp ≡ sp - z14 with ztotal (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 + z14 with ztotal (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) ? ... | tri< a ¬b ¬c = ⊥-elim z16 where z16 : ⊥ - 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 ) + z16 with proj1 (mf (( MinSUP.sup sp1)) ( MinSUP.asm sp1 )) + ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym ? ) )) + ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso ? )) + ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ (MinSUP.sup sp1) ) &iso ? -- ( cong (&) b ) ... | tri> ¬a ¬b c = ⊥-elim z17 where - z15 : (* (f sp) ≡ SUP.sup sp1) ∨ (* (f sp) < SUP.sup sp1 ) - z15 = x≤sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 )) + z15 : (f sp ≡ MinSUP.sup sp1) ∨ (* (f sp) < * (MinSUP.sup sp1) ) + 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 + ... | case1 eq = ¬b ? + ... | case2 lt = ¬a ? tri : {n : Level} (u w : Ordinal ) { R : Set n } → ( u o< w → R ) → ( u ≡ w → R ) → ( w o< u → R ) → R tri {_} u w p q r with trio< u w @@ -1433,24 +1426,22 @@ -- 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 - (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 + z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} + (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.asm msp1 )))) + (subst (λ k → odef A k) ? (MinSUP.asm msp1) ) + (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc msp1 ss<sa ))) -- x ≡ f x ̄ + (proj1 (cf-is-<-monotonic nmx c (MinSUP.asm msp1 ))) where -- x < f x supf = ZChain.supf zc msp1 : MinSUP A (ZChain.chain zc) msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc - sp1 : SUP A (ZChain.chain zc) - sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc c : Ordinal - c = & ( SUP.sup sp1 ) - mc = MinSUP.sup msp1 + c = MinSUP.sup msp1 + mc = c mc<A : mc o< & A mc<A = ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ c=mc : c ≡ mc - c=mc = &iso + c=mc = refl z20 : mc << cf nmx mc z20 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1) ) asc : odef A (supf mc)