Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 892:f331c8be2425
x ≤ supf x is no good
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 05 Oct 2022 20:40:37 +0900 |
| parents | 9fb948dac666 |
| children | 290c61498d62 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 39 insertions(+), 34 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Oct 05 13:13:35 2022 +0900 +++ b/src/zorn.agda Wed Oct 05 20:40:37 2022 +0900 @@ -450,8 +450,8 @@ fcy<sup : {u w : Ordinal } → u o≤ z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf fcy<sup {u} {w} u≤z fc with MinSUP.x<sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ - ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans ? (sym (supf-is-minsup u≤z ) ) )) - ... | case2 lt = case2 ? -- (subst (λ k → * w < k ) ? )-- (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-minsup u≤z ))) ) lt ) + ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans eq (sym (supf-is-minsup u≤z ) ) )) + ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt ) -- ordering is not proved here but in ZChain1 @@ -642,12 +642,12 @@ order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) order {b} {s} {z1} b<z ss<sb fc = zc04 where zc00 : ( z1 ≡ MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1 << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) ) - zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤ b<z) ) ? -- (csupf-fc (o<→≤ b<z) ss<sb fc ) + zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤ b<z) ) (subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc (o<→≤ b<z) ss<sb fc )) -- supf (supf b) ≡ supf b zc04 : (z1 ≡ supf b) ∨ (z1 << supf b) zc04 with zc00 - ... | case1 eq = ? -- case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (ZChain.supf-is-minsup zc (o<→≤ b<z)) ) (cong (&) eq) ) - ... | case2 lt = ? -- case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) ) ))) lt ) + ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z)) ) eq ) + ... | case2 lt = case2 (subst₂ (λ j k → j < * k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) )) lt ) zc1 : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x zc1 x prev with Oprev-p x @@ -662,15 +662,20 @@ is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b is-max {a} {b} ua b<x ab P a<b | case2 is-sup - = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + = ⟪ ab , ch-is-sup b b<sfx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where b<A : b o< & A b<A = z09 ab + b<sfx : b o< ZChain.supf zc x + b<sfx with trio< x (& A) + ... | tri< a ¬b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o<→≤ a)) + ... | tri≈ ¬a b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o≤-refl0 b)) + ... | tri> ¬a ¬b c = subst (λ k → b o< k ) (sym (ZChain.supfmax zc c)) (ordtrans<-≤ b<A ( ZChain.x≤supfx zc (o≤-refl))) m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f - m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 ? (HasPrev.ay nhp) + m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (ZChain.supf-mono zc (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 → IsSup.x<sup (proj2 is-sup) (chain-mono1 ? uz ) } , m04 ⟫ + ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (ZChain.supf-mono zc (o<→≤ b<x)) uz ) } , m04 ⟫ 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 @@ -687,22 +692,25 @@ is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay ) ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl )) ⟫ - ... | case2 y<b = ⟪ ab , ch-is-sup b m10 m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + ... | case2 y<b = ⟪ ab , ch-is-sup b b<sfx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where m09 : b o< & A m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) - m10 : b o< ZChain.supf zc x - m10 = ordtrans<-≤ b<x ( ZChain.x≤supfx zc ? ) + b<sfx : b o< ZChain.supf zc x + b<sfx with trio< x (& A) + ... | tri< a ¬b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o<→≤ a)) + ... | tri≈ ¬a b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o≤-refl0 b)) + ... | tri> ¬a ¬b c = subst (λ k → b o< k ) (sym (ZChain.supfmax zc c)) (ordtrans<-≤ m09 ( ZChain.x≤supfx zc (o≤-refl))) m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b m08 {s} {z1} s<b fc = order m09 s<b fc m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f - m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 ? (HasPrev.ay nhp) + m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (ZChain.supf-mono zc (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<→≤ m09) - ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 ? lt )} , m04 ⟫ -- ZChain on x + ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 (ZChain.supf-mono zc (o<→≤ b<x)) lt )} , m04 ⟫ -- ZChain on x m06 : ChainP A f mf ay supf b m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = m05 } @@ -720,9 +728,6 @@ z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) z21 : & (SUP.sup sp1) o< & A z21 = c<→o< ( SUP.as sp1) - -- ZChain.supf zc (& A) o≤ & (SUP.sup sp1) ( minimality ) - z11 : & (SUP.sup sp1) o< ZChain.supf zc (& A) - 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 ) @@ -839,7 +844,7 @@ ... | 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 osuc-≡< (ZChain.x≤supfx zc ? ) + zc4 with osuc-≡< (ZChain.x≤supfx zc o≤-refl ) ... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1 ; x≤supfx = ? ; minsup = ? ; supf-is-sup = ? ; csupf = ? } where @@ -864,10 +869,9 @@ zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc px f mf fb )) ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb) ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) - zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) - ? -- (subst (λ k → odef A k ∧ UChain A f mf ay supf0 ? k) (sym &iso) ca ) - ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 ? )-- (cong (&) eq)) - ... | case2 lt = case2 (subst (λ k → (* a) < k ) ? ? ) -- (trans (sym *iso) (cong (*) zc06)) lt) + zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) (subst (λ k → odef A k ∧ UChain A f mf ay supf0 (supf0 px) k) (sym &iso) ca ) + ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq ) + ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt ) ptotal : IsTotalOrderSet pchainpx ptotal (case1 a) (case1 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso @@ -929,9 +933,9 @@ supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px ... | tri< a ¬b ¬c = zc19 where zc21 : MinSUP A (UnionCF A f mf ay supf0 z) - zc21 = ZChain.minsup zc ? -- (o<→≤ a) + zc21 = ZChain.minsup zc (o<→≤ a) zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) - zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 ? ux)) + zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc (o<→≤ a)) ux)) zc19 : supf0 z o≤ sp1 zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc (o<→≤ a))) ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) ... | tri≈ ¬a b ¬c = zc18 where @@ -944,7 +948,7 @@ supf0 px ≡⟨ sym sfpx=px ⟩ px ∎ where open ≡-Reasoning zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) - zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 ? ux)) + zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc (o≤-refl0 b)) ux)) zc18 : px o≤ sp1 -- supf0 z ≡ px zc18 = subst (λ k → k o≤ sp1) zc20 ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) ... | tri> ¬a ¬b c = o≤-refl @@ -1009,7 +1013,7 @@ zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 zc19)) ( ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 zc19)) ss<spx) (fcpu fc zc18) ) where zc19 : u o≤ px - zc19 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ? -- u<x + zc19 = o<→≤ a zc18 : s o≤ px zc18 = ordtrans (ZChain.supf-inject zc ss<spx) zc19 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) @@ -1085,21 +1089,21 @@ -- (sf1=sf0 ?) (trans ? sfpx=px ) ss<spx csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 csupf17 (init as refl ) = ZChain.csupf zc sf<px - csupf17 (fsuc x fc) = ? -- ZChain.f-next zc ? -- (csupf17 fc) + csupf17 (fsuc x fc) = ZChain.f-next zc ? -- (csupf17 fc) x≤supfx1 : {z : Ordinal} → z o≤ x → z o≤ supf1 z x≤supfx1 {z} z≤x with trio< z (supf1 z) -- supf1 x o< x → supf1 x o≤ supf1 px → x o< px ∨ supf1 x ≡ supf1 px ... | tri< a ¬b ¬c = o<→≤ a ... | tri≈ ¬a b ¬c = o≤-refl0 b ... | tri> ¬a ¬b c with trio< z px - ... | tri< a ¬b ¬c = ZChain.x≤supfx zc ? + ... | tri< a ¬b ¬c = ZChain.x≤supfx zc (o<→≤ a) ... | tri≈ ¬a b ¬c = subst (λ k → k o< osuc px) (sym b) <-osuc ... | tri> ¬a ¬b lt = ⊥-elim ( o≤> sf04 c ) where -- c : sp1 o< z, lt : px o< z -- supf1 z ≡ sp1 -- supf1 z o< z z=x : z ≡ x z=x with trio< z x ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ lt , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) a ⟫ ) ... | tri≈ ¬a b ¬c = b - ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤x ? ) + ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤x c ) sf01 : supf1 x ≡ sp1 sf01 with trio< x px ... | tri< a ¬b ¬c = ⊥-elim ( ¬c (pxo<x op )) @@ -1111,10 +1115,11 @@ sf00 = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl) (sym sfpx=px)) sf01 sf02 sf04 : z o≤ sp1 sf04 with osuc-≡< sf00 - ... | case1 eq = ? -- sup of U px ≡ supf1 px ≡ supf1 x ≡ sp1 ≡ sup of U x - -- px ≡ supf0 px - -- px ≡ supf1 x - -- supf1 x ≡ x ? + ... | case1 eq = ? where + sf05 : px ≡ sp1 -- z o< osuc x -- z ≡ x + sf05 = eq + sf06 : z ≡ osuc sp1 -- z o< osuc x -- z ≡ x + sf06 = trans z=x (trans (sym (Oprev.oprev=x op)) (cong osuc sf05 )) ... | case2 lt = subst (λ k → k o≤ sp1 ) (trans (Oprev.oprev=x op) (sym z=x)) (osucc lt ) record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where @@ -1140,7 +1145,7 @@ z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) sfpx=px a )) ... | tri≈ ¬a b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) zc20 (case2 (init apx sfpx=px )) where z1≤px : z1 o≤ px -- z1 o≤ supf1 z1 ≡ px - z1≤px = subst (λ k → z1 o< k) (sym (Oprev.oprev=x op)) (supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 ? ) )) + z1≤px = subst (λ k → z1 o< k) (sym (Oprev.oprev=x op)) (supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 o≤-refl ) )) zc20 : supf0 px ≡ supf1 z1 zc20 = begin supf0 px ≡⟨ sym sfpx=px ⟩ @@ -1151,7 +1156,7 @@ zc21 : px o< z1 zc21 = ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) sfpx=px c ) zc22 : z1 o< x -- c : px o< supf0 z1 - zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 ? ) ) + zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 o≤-refl ) ) -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x ... | case2 px<spfx = ? where