Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 970:980bc43ca6c1
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 07 Nov 2022 08:04:35 +0900 |
| parents | ec7f3473ff55 |
| children | 4fdf889ca95a |
| files | src/zorn.agda |
| diffstat | 1 files changed, 41 insertions(+), 53 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Nov 07 05:02:08 2022 +0900 +++ b/src/zorn.agda Mon Nov 07 08:04:35 2022 +0900 @@ -988,59 +988,47 @@ ... | 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 ⟫ ) 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) } + zc35 {z} ne ⟪ ua1 , ch-init fc ⟫ = ⟪ ua1 , ch-init fc ⟫ + zc35 {z} ne ⟪ 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 = zc34 where + u<x0 : u o≤ px + u<x0 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) (supf-inject0 supf1-mono u<x ) + zc34 : odef (UnionCF A f mf ay supf0 x) z + zc34 with trio< (supf0 px) px + ... | tri< sf0px<px ¬b ¬c = cp3 ( subst ( λ k → FClosure A f k z) + (trans (trans (sf1=sf0 u<x0) eq) (ZChain.supfmax zc px<x) ) fc) where + 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) + ... | tri≈ ¬a b ¬c = ⊥-elim (ne b) + ... | tri> ¬a ¬b px<sf0px = ⊥-elim (¬p<x<op ⟪ cp5 , cp4 ⟫ ) where + cp4 : u o< osuc px + cp4 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ( supf-inject0 supf1-mono u<x ) + cp5 : px o< u + cp5 = subst (λ k → px o< k ) ( begin + supf0 px ≡⟨ sym (ZChain.supfmax zc px<x) ⟩ + supf0 x ≡⟨ sym eq ⟩ + supf0 u ≡⟨ sym (sf1=sf0 u<x0) ⟩ + supf1 u ≡⟨ ChainP.supu=u is-sup ⟩ + u ∎ ) px<sf0px where open ≡-Reasoning + ... | 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