Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 969:ec7f3473ff55
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 07 Nov 2022 05:02:08 +0900 |
| parents | 9a8041a7f3c9 |
| children | 980bc43ca6c1 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 99 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Nov 06 13:39:45 2022 +0900 +++ b/src/zorn.agda Mon Nov 07 05:02:08 2022 +0900 @@ -483,14 +483,16 @@ fsp≤sp : f sp <= sp fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00 - UChain⊆ : { supf1 : Ordinal → Ordinal } +UChain⊆ : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) + {z y : Ordinal} (ay : odef A y) { supf supf1 : Ordinal → Ordinal } + → (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) → ( { x : Ordinal } → x o< z → supf x ≡ supf1 x) → ( { x : Ordinal } → z o≤ x → supf z o≤ supf1 x) → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf1 z - UChain⊆ {supf1} eq<x lex ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - UChain⊆ {supf1} eq<x lex ⟪ az , ch-is-sup u {x} u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u u<x1 cp1 fc1 ⟫ where +UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ +UChain⊆ A f mf {z} {y} ay {supf} {supf1} spuf-mono eq<x lex ⟪ az , ch-is-sup u {x} u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u u<x1 cp1 fc1 ⟫ where u<x0 : u o< z - u<x0 = supf-inject u<x + u<x0 = supf-inject0 spuf-mono u<x u<x1 : supf1 u o< supf1 z u<x1 = subst (λ k → k o< supf1 z ) (eq<x u<x0) (ordtrans<-≤ u<x (lex o≤-refl ) ) fc1 : FClosure A f (supf1 u) x @@ -887,8 +889,9 @@ zc41 with zc43 zc41 | (case2 sp≤x ) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1 } where - -- supf0 px is included by the chain of sp1 - -- ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x + -- supf0 px is included in the chain of sp1 + -- supf0 px ≡ px ∧ supf0 px o< sp1 → ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x + -- else UnionCF A f mf ay supf0 px ≡ UnionCF supf1 x -- supf1 x ≡ sp1, which is not included now supf1 : Ordinal → Ordinal @@ -984,9 +987,77 @@ ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) b ))) ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) - zc12 : {z : Ordinal} → supf0 px ≡ px → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z - zc12 {z} sfpx=px (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ - zc12 {z} sfpx=px (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where + zc35 : {z : Ordinal} → ¬ (supf0 px ≡ px) → odef (UnionCF A f mf ay supf1 x) z → odef (UnionCF A f mf ay supf0 x) z + zc35 {z} ne with trio< (supf0 px) px + ... | tri< sf0px<px ¬b ¬c = zc34 where + zc34 : odef (UnionCF A f mf ay supf1 x) z → odef (UnionCF A f mf ay supf0 x) z + zc34 ⟪ ua1 , ch-init fc ⟫ = ⟪ ua1 , ch-init fc ⟫ + zc34 ⟪ ua1 , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( ZChain.supf-mono zc (o<→≤ (supf-inject0 supf1-mono u<x)) ) + ... | case1 eq = cp3 ( subst ( λ k → FClosure A f k z) (trans (trans (sf1=sf0 u<x0) eq) (ZChain.supfmax zc px<x) ) fc) where + u<x0 : u o≤ px + u<x0 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) (supf-inject0 supf1-mono u<x ) + cp3 : {z : Ordinal } → FClosure A f (supf0 px) z → odef (UnionCF A f mf ay supf0 x) z + cp3 (init uz refl) = chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) (ZChain.csupf zc sf0px<px) + cp3 (fsuc uz fc) = ZChain.f-next zc (cp3 fc) + ... | case2 u<x1 = ⟪ ua1 , ch-is-sup u u<x1 cp1 fc1 ⟫ where + u<x0 : u o< x + u<x0 = supf-inject0 supf1-mono u<x -- supf0 u o≤ px ≡ supf0 px → supf0 u ≡ supf0 px ∨ u o< px + sf0u=sf1u : supf0 u ≡ supf1 u + sf0u=sf1u = sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 )) + cp2 : {s : Ordinal } → supf0 s o< supf0 u → supf0 s ≡ supf1 s + cp2 {s} ss<su = sym ( sf1=sf0 ( begin + s <⟨ ZChain.supf-inject zc ss<su ⟩ + u ≤⟨ subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ⟩ + px ∎ )) where open o≤-Reasoning O + fc1 : FClosure A f (supf0 u) z + fc1 = subst (λ k → FClosure A f k z ) (sym sf0u=sf1u) fc + cp1 : ChainP A f mf ay supf0 u + cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u) (ChainP.fcy<sup is-sup fc ) + ; order = λ {s} {z} s<u fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u) + (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (cp2 s<u) sf0u=sf1u s<u) + (subst (λ k → FClosure A f k z ) (cp2 s<u) fc )) + ; supu=u = trans (sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ))) (ChainP.supu=u is-sup) } + ... | tri≈ ¬a b ¬c = ⊥-elim (ne b) + ... | tri> ¬a ¬b c = ? where + zc34 : odef (UnionCF A f mf ay supf1 x) z → odef (UnionCF A f mf ay supf0 x) z + zc34 ⟪ ua1 , ch-init fc ⟫ = ⟪ ua1 , ch-init fc ⟫ + zc34 ⟪ ua1 , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( ZChain.supf-mono zc (o<→≤ (supf-inject0 supf1-mono u<x)) ) + ... | case1 eq = ? + ... | case2 u<x1 = ⟪ ua1 , ch-is-sup u u<x1 cp1 fc1 ⟫ where + u<x0 : u o< x + u<x0 = supf-inject0 supf1-mono u<x -- supf0 u o≤ px ≡ supf0 px → supf0 u ≡ supf0 px ∨ u o< px + sf0u=sf1u : supf0 u ≡ supf1 u + sf0u=sf1u = sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 )) + cp2 : {s : Ordinal } → supf0 s o< supf0 u → supf0 s ≡ supf1 s + cp2 {s} ss<su = sym ( sf1=sf0 ( begin + s <⟨ ZChain.supf-inject zc ss<su ⟩ + u ≤⟨ subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ⟩ + px ∎ )) where open o≤-Reasoning O + fc1 : FClosure A f (supf0 u) z + fc1 = subst (λ k → FClosure A f k z ) (sym sf0u=sf1u) fc + cp1 : ChainP A f mf ay supf0 u + cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u) (ChainP.fcy<sup is-sup fc ) + ; order = λ {s} {z} s<u fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u) + (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (cp2 s<u) sf0u=sf1u s<u) + (subst (λ k → FClosure A f k z ) (cp2 s<u) fc )) + ; supu=u = trans (sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ))) (ChainP.supu=u is-sup) } + + zc33 : {z : Ordinal} → ¬ (supf0 px o< sp1) → odef (UnionCF A f mf ay supf1 x) z → odef (UnionCF A f mf ay supf0 x) z + zc33 {z} lt = UChain⊆ A f mf ay supf1-mono (λ lt → sym (sf=eq lt)) sf≤0 where + sf≤0 : { z : Ordinal } → x o≤ z → supf1 x o≤ supf0 z + sf≤0 {z} x≤z with trio< z px + ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) ) + ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x )) + ... | tri> ¬a ¬b px<z with trio< sp1 (supf0 x) -- = ? --- sp1 o≤ supf0 x + ... | tri< a ¬b ¬c = subst₂ ( λ j k → j o≤ k) (sym (sf1=sp1 px<x)) + (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z))) ( o<→≤ a ) + ... | tri≈ ¬a b ¬c = subst₂ ( λ j k → j o≤ k) (sym (sf1=sp1 px<x)) + (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z))) (o≤-refl0 b) + ... | tri> ¬a ¬b sf0<sp1 = ⊥-elim ( lt ( ordtrans≤-< (ZChain.supf-mono zc (o<→≤ px<x)) sf0<sp1 )) + + zc12 : {z : Ordinal} → supf0 px ≡ px → supf0 px o< sp1 → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z + zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ + zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where u<px : u o< px u<px = ZChain.supf-inject zc su<sx u<x : u o< x @@ -1033,7 +1104,7 @@ s≤px : s o≤ px s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx) ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px ⟫ ) - zc12 {z} sfpx=px (case2 fc) = zc21 fc where + zc12 {z} sfpx=px sfpx<sp (case2 fc) = zc21 fc where --- supf0 px o< sp1 zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc @@ -1043,8 +1114,8 @@ record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where zc15 : supf1 px ≡ px zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px) - zc18 : supf1 px o< supf1 x - zc18 = ? + zc18 : supf1 px o< supf1 x + zc18 = subst₂ ( λ j k → j o< k ) (sym (sf1=sf0 o≤-refl)) (sym (sf1=sp1 px<x)) sfpx<sp zc14 : FClosure A f (supf1 px) (supf0 px) zc14 = init (subst (λ k → odef A k) (sym (sf1=sf0 o≤-refl)) asp) (sf1=sf0 o≤-refl) zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px ) @@ -1105,14 +1176,16 @@ -- z1 ≡ px , supf0 px ≡ px psz1≤px : supf1 z1 o≤ px psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x + sf0px<sp1 : supf0 px o< sp1 -- px o< sp1 o≤ x .. sp1 ≡ x + sf0px<sp1 = ? csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) csupf2 with trio< z1 px | inspect supf1 z1 csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px - ... | case2 lt = zc12 ? (case1 cs03) where + ... | case2 lt = zc12 ? ? (case1 cs03) where cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) ) - ... | case1 sfz=sfpx = zc12 ? (case2 (init (ZChain.asupf zc) cs04 )) where + ... | case1 sfz=sfpx = zc12 ? ? (case2 (init (ZChain.asupf zc) cs04 )) where supu=u : supf1 (supf1 z1) ≡ supf1 z1 supu=u = trans (cong supf1 sfz=px) (sym sfz=sfpx) cs04 : supf0 px ≡ supf0 z1 @@ -1127,7 +1200,7 @@ cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx cs06 : supf0 px o< osuc px cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) ? - csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 ? (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) + csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 ? ? (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ? -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ ) @@ -1161,6 +1234,17 @@ ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x )) ... | tri> ¬a ¬b c = o≤-refl0 ( ZChain.supfmax zc px<x ) + sf=eq0 : { z : Ordinal } → z o< x → supf1 z ≡ supf0 z + sf=eq0 {z} z<x with trio< z px + ... | tri< a ¬b ¬c = refl + ... | tri≈ ¬a b ¬c = refl + ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → z o< k) (sym (Oprev.oprev=x op)) z<x ⟫ ) + sf≤0 : { z : Ordinal } → x o≤ z → supf1 x o≤ supf0 z + sf≤0 {z} x≤z with trio< z px + ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) ) + ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x )) + ... | tri> ¬a ¬b c = o≤-refl0 ? -- (sym ( ZChain.supfmax zc px<x )) + zc17 : {z : Ordinal } → supf0 z o≤ supf0 px zc17 = ? -- px o< z, px o< supf0 px