Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 841:01361e10ad96
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 29 Aug 2022 19:56:39 +0900 |
| parents | 52bff0b4cb37 |
| children | 962a9f3dbd3c |
| files | src/zorn.agda |
| diffstat | 1 files changed, 53 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Aug 29 10:18:08 2022 +0900 +++ b/src/zorn.agda Mon Aug 29 19:56:39 2022 +0900 @@ -771,27 +771,65 @@ pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - zc10 {z} ⟪ az , ch-is-sup u u≤px is-sup fc ⟫ = zc12 fc where - zc12 : {z : Ordinal} → FClosure A f (supf0 u) z → odef pchain1 z + zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = zc12 fc where + zc12 : {z : Ordinal} → FClosure A f (supf0 u1) z → odef pchain1 z zc12 (fsuc x fc) with zc12 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ - ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ - zc12 (init asu su=z ) with trio< u px - ... | tri< a ¬b ¬c = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u (ordtrans u≤px (osucc (pxo<x op)) ) - record { fcy<sup = ? ; order = ? ; supu=u = ? } (init ? ? ) ⟫ - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ? + ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ + zc12 (init asp refl ) with trio< u1 px | inspect supf1 u1 + ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x ? ) + record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup) } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 ) ⟫ where + fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 ) + fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc ) + order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 → + (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1) + order {s} {z2} s<u1 fc with trio< s px + ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) + ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) + ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s ? )) -- px o< s < u1 < px + ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x ? ) + record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup) } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 ) ⟫ where + fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 ) + fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc ) + order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 → + (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1) + order {s} {z2} s<u1 fc with trio< s px + ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) + ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) + ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b ? ) )) -- px o< s < u1 = px + ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< u1≤x + ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) + ... | case2 lt = ⊥-elim ( o<> lt px<u1 ) + zc11 : {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where - zc13 : {z : Ordinal} → FClosure A f (supf1 u) z → odef pchain z + zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = zc13 fc where + zc13 : {z : Ordinal} → FClosure A f (supf1 u1) z → odef pchain z zc13 (fsuc x fc) with zc13 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ - zc13 (init asu su=z ) with trio< u x - ... | tri< a ¬b ¬c = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u (subst (λ k → u o< k) (sym (Oprev.oprev=x op)) a) ? (init ? ? ) ⟫ - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ⊥-elim ( o≤> u≤x c ) + zc13 (init asp refl ) with trio< u1 px | inspect supf1 u1 + ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (subst (λ k → u1 o< k ) ? a ) + record { fcy<sup = fcy<sup ; order = order ; supu=u = trans ? (ChainP.supu=u u1-is-sup) } (init ? ?) ⟫ where + fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 ) + fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc ) + order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u1 → FClosure A f (supf0 s) z2 → + (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1) + order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s + ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc )) + ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc )) + ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s ? )) -- px o< s < u1 < px + ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x ? ) + record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym ?) (ChainP.supu=u u1-is-sup) } (init ? ? ) ⟫ where + fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 ) + fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc ) + order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u1 → FClosure A f (supf0 s) z2 → + (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1) + order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s + ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc )) + ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc )) + ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s ? )) -- px o< s < u1 = px + ... | tri> ¬a ¬b c | _ = ⊥-elim ( o≤> u1≤x ? ) sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) sup {z} z≤x with trio< z px | inspect supf1 z ... | tri< a ¬b ¬c | record { eq = eq1} = ? -- ZChain.sup zc (o<→≤ a) @@ -827,21 +865,11 @@ ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x)) sis {z} z≤x = zc40 where - zc40 : supf1 z ≡ & (SUP.sup (sup z≤x)) + zc40 : supf1 z ≡ & (SUP.sup (sup z≤x)) -- direct with statment causes error zc40 with trio< z px | inspect supf1 z | inspect sup z≤x ... | tri< a ¬b ¬c | record { eq = eq1 } | record { eq = eq2 } = ? ... | tri≈ ¬a b ¬c | record { eq = eq1 } | record { eq = eq2 } = ? ... | tri> ¬a ¬b c | record { eq = eq1 } | record { eq = eq2 } = ? --- ... | tri< a ¬b ¬c = ? -- jZChain.supf-is-sup zc (o<→≤ a ) --- ... | tri≈ ¬a b ¬c = ? -- jZChain.supf-is-sup zc (o≤-refl0 b ) --- ... | tri> ¬a ¬b px<z = ? --- ... | tri< a ¬b ¬c | _ = ? -- jZChain.supf-is-sup zc (o<→≤ a ) --- ... | tri≈ ¬a b ¬c | _ = ? -- jZChain.supf-is-sup zc (o≤-refl0 b ) --- ... | tri> ¬a ¬b px<z | record { eq = eq1 } = ? where --- zc30 : z ≡ x --- zc30 with osuc-≡< z≤x --- ... | case1 eq = eq --- ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) zc4 : ZChain A f mf ay x zc4 with ODC.∋-p O A (* x)