Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 822:c97cc257374b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 18 Aug 2022 11:48:29 +0900 |
| parents | 22676639125f |
| children | 497b5db603e7 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 36 insertions(+), 75 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Aug 17 15:51:47 2022 +0900 +++ b/src/zorn.agda Thu Aug 18 11:48:29 2022 +0900 @@ -285,8 +285,8 @@ sup : {x : Ordinal } → x o< z → SUP A (UnionCF A f mf ay supf x) sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z → IsSup A (UnionCF A f mf ay supf b) ab → supf b ≡ b - supf-is-sup : {x : Ordinal } → (x<z : x o< z) → supf x ≡ & (SUP.sup (sup x<z) ) - csupf : {b : Ordinal } → b o< z → odef (UnionCF A f mf ay supf b) (supf b) + supf-is-sup : {x : Ordinal } → (x≤z : x o< z) → supf x ≡ & (SUP.sup (sup x≤z) ) + csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) -- ordering is proved here for totality and sup @@ -303,7 +303,7 @@ s<z : s o< z s<z = ordtrans s<b b<z zc03 : odef (UnionCF A f mf ay supf b) (supf s) - zc03 with csupf s<z + zc03 with csupf (o<→≤ s<z) ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u≤x (osucc s<b)) is-sup fc ⟫ zc01 (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where @@ -672,8 +672,8 @@ supf1 : Ordinal → Ordinal supf1 z with trio< z px ... | tri< a ¬b ¬c = ZChain.supf zc z - ... | tri≈ ¬a b ¬c = sp1 - ... | tri> ¬a ¬b c = sp1 + ... | tri≈ ¬a b ¬c = ZChain.supf zc z + ... | tri> ¬a ¬b c = ZChain.supf zc px pchain1 : HOD pchain1 = UnionCF A f mf ay supf1 x @@ -702,12 +702,12 @@ ax : odef A x is-sup : IsSup A (UnionCF A f mf ay supf0 px) ax - UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) → (z0≤px : z0 o< px ) → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1 - UnionCF⊆ {z0} {z1} z0<1 z0≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ - UnionCF⊆ {z0} {z1} z0<1 z0≤px ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫ = zc60 fc where + UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) → (z0≤px : z0 o≤ px ) → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1 + UnionCF⊆ {z0} {z1} z0≤1 z0≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ + UnionCF⊆ {z0} {z1} z0≤1 z0≤px ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫ = zc60 fc where zc60 : {w : Ordinal } → FClosure A f (supf0 u1) w → odef (UnionCF A f mf ay supf1 z1 ) w zc60 (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 z0<1 ) + ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 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 ) @@ -715,21 +715,21 @@ (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 s<u1 fc ) - ... | tri≈ ¬a b ¬c = ? -- subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc ) + ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc ) ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) )) -- px o< s < u1 < px - ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0<1 ) - record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 ? } ? ⟫ where + ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) + 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 ) + fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc ) order : {s : Ordinal} {z2 : Ordinal} → s o< 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 s<u1 fc ) - ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ? -- ( ChainP.order u1-is-sup s<u1 fc ) + ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc ) + ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc ) ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) )) -- px o< s < u1 = px - ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } = ? -- with osuc-≡< (OrdTrans u1≤x z0≤px) - -- ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) - -- ... | case2 lt = ⊥-elim ( o<> lt px<u1 ) + ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< (OrdTrans u1≤x z0≤px) + ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) + ... | case2 lt = ⊥-elim ( o<> lt px<u1 ) zc60 (fsuc w1 fc) with zc60 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₁) ⟫ @@ -750,70 +750,41 @@ (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) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) - ... | tri≈ ¬a b ¬c | record { eq = eq2 } = ? -- subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) + ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) )) -- px o< s < u1 < px ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) - record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym ? ) (ChainP.supu=u u1-is-sup) } (init ? ? ) ⟫ where + record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup) } (init asp refl ) ⟫ 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 ) + fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) eq1 ( ChainP.fcy<sup u1-is-sup fc ) order : {s : Ordinal} {z2 : Ordinal} → s o< 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 s<u1 (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 s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) ? )) + ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) + ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) )) -- px o< s < u1 = px ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with trio< z0 px ... | tri< a ¬b ¬c with osuc-≡< (OrdTrans u1≤x (o<→≤ a) ) ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) ... | case2 lt = ⊥-elim ( o<> lt px<u1 ) - zc60 (init asp refl) | tri> ¬a ¬b px<u1 | record { eq = eq2} | tri≈ ¬a' b ¬c with osuc-≡< (OrdTrans u1≤x (o≤-refl0 b) ) + zc60 (init asp refl) | tri> ¬a ¬b px<u1 | record { eq = eq1} | tri≈ ¬a' b ¬c with osuc-≡< (OrdTrans u1≤x (o≤-refl0 b) ) ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) ... | case2 lt = ⊥-elim ( o<> lt px<u1 ) - zc60 (init asp refl) | tri> ¬a ¬b px<u1 | record { eq = eq2} | tri> ¬a' ¬b' px<z0 = ⊥-elim ( ¬sp=x zcsup ) where - zc30 : x ≡ z0 - zc30 = ? -- with osuc-≡< z0≤x - -- ... | case1 eq = sym (eq) - -- ... | case2 z0<x = ⊥-elim (¬p<x<op ⟪ px<z0 , subst (λ k → z0 o< k ) (sym (Oprev.oprev=x op)) z0<x ⟫ ) - zc31 : x ≡ u1 - zc31 with trio< x u1 - ... | tri≈ ¬a b ¬c = b - ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ px<u1 , subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) c ⟫ ) - zc31 | tri< a ¬b ¬c with osuc-≡< (subst (λ k → u1 o≤ k ) (sym zc30) u1≤x ) -- px<u1 u1≤x, - ... | case1 u1=x = ⊥-elim ( ¬b (sym u1=x) ) - ... | case2 u1<x = ⊥-elim ( o<> u1<x a ) - zc33 : supf1 u1 ≡ u1 -- u1 ≡ supf1 u1 ≡ supf1 x ≡ sp1 - zc33 = ChainP.supu=u u1-is-sup - zc32 : sp1 ≡ x - zc32 = begin - sp1 ≡⟨ sym eq2 ⟩ - supf1 u1 ≡⟨ zc33 ⟩ - u1 ≡⟨ sym zc31 ⟩ - x ∎ where open ≡-Reasoning - zc34 : {z : Ordinal} → odef (UnionCF A f mf ay supf0 px) z → (z ≡ x) ∨ (z << x) - zc34 {z} lt with SUP.x<sup sup1 (subst (λ k → odef (UnionCF A f mf ay supf0 x) k ) (sym &iso) (chain-mono f mf ay supf0 (pxo≤x op) lt ) ) - ... | case1 eq = case1 ( begin - z ≡⟨ sym &iso ⟩ - & (* z) ≡⟨ cong (&) eq ⟩ - sp1 ≡⟨ zc32 ⟩ - x ∎ ) where open ≡-Reasoning - ... | case2 lt = case2 ( subst (λ k → * z < k ) (trans (sym *iso) (cong (*) zc32 )) lt ) - zcsup : xSUP - zcsup = record { ax = subst (λ k → odef A k) zc32 asp ; is-sup = record { x<sup = zc34 } } + zc60 (init asp refl) | tri> ¬a ¬b px<u1 | record { eq = eq1} | tri> ¬a' ¬b' px<z0 = ⊥-elim (¬p<x<op ⟪ px<z0 , subst (λ k → z0 o< k ) (sym (Oprev.oprev=x op)) z0<x ⟫ ) zc60 (fsuc w1 fc) with zc60 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₁) ⟫ sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z) sup {z} z<x with trio< z px - ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl ? ) ( ZChain.sup zc a ) + ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl z<x ) ( ZChain.sup zc a ) ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc61 } where zc61 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1) - zc61 {w} lt = SUP.x<sup sup1 (UnionCFR⊆ (o<→≤ z<x) ? lt ) + zc61 {w} lt = SUP.x<sup sup1 (UnionCFR⊆ (o<→≤ z<x) z<x lt ) ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b sup=u {b} ab b≤x is-sup with trio< b px - ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl ? lt) } - ... | tri≈ ¬a b ¬c = ? -- ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) } + ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o<→≤ a) lt) } + ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) } ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where zc30 : x ≡ b zc30 with osuc-≡< b≤x @@ -821,22 +792,12 @@ ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) zcsup : xSUP zcsup with zc30 - ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) ? lt) } } - csupf : {b : Ordinal} → b o< x → odef (UnionCF A f mf ay supf1 b) (supf1 b) + ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) o≤-refl lt) } } + csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b) csupf {b} b<x with trio< b px | inspect supf1 b - ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl a ( ZChain.csupf zc a ) - ... | tri≈ ¬a b ¬c | _ = ? -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc ? ) - ... | tri> ¬a ¬b px<b | record { eq = eq1 } = - ⟪ SUP.as sup1 , ch-is-sup ? ? ? (subst (λ k → FClosure A f k sp1) (sym eq1) (init (SUP.as sup1) refl)) ⟫ - where - -- px< b ≤ x - -- b ≡ x, supf x ≡ sp1 , ¬ x ≡ sp1 - zc30 : x ≡ b - zc30 = ? -- with osuc-≡< ? - -- ... | case1 eq = sym (eq) - -- ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) - zc31 : ChainP A f mf ay supf1 b - zc31 = record { fcy<sup = {!!} ; order = {!!} ; supu=u = {!!} } + ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) ( ZChain.csupf zc (o<→≤ a) ) + ... | tri≈ ¬a refl ¬c | _ = UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl ) + ... | tri> ¬a ¬b px<b | record { eq = eq1 } = UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl ) sis : {z : Ordinal} (z<x : z o< x) → supf1 z ≡ & (SUP.sup (sup z<x)) sis {z} z≤x = {!!} zc4 : ZChain A f mf ay x @@ -859,7 +820,7 @@ ... | tri< a ¬b ¬c = ZChain.supf zc z ... | tri≈ ¬a b ¬c = x ... | tri> ¬a ¬b c = x - csupf : {b : Ordinal} → b o< x → odef (UnionCF A f mf ay psupf1 b) (psupf1 b) + csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay psupf1 b) (psupf1 b) csupf {b} b≤x with trio< b px | inspect psupf1 b ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫ ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫ @@ -979,7 +940,7 @@ ... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b) (ob<x lim a)) ab {!!} record { x<sup = {!!} } ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?) ?) ab {!!} record { x<sup = {!!} } ... | tri> ¬a ¬b c = {!!} - csupf : {z : Ordinal} → z o< x → odef (UnionCF A f mf ay supf1 z) (supf1 z) + csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z) csupf {z} z≤x with trio< z x ... | tri< a ¬b ¬c = zc9 where zc9 : odef (UnionCF A f mf ay supf1 z) (ZChain.supf (pzc (osuc z) (ob<x lim a)) z)