Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 843:ef0433f41e55
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 30 Aug 2022 14:30:36 +0900 |
| parents | 962a9f3dbd3c |
| children | 0855fce6ee92 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 61 insertions(+), 27 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Aug 30 09:49:25 2022 +0900 +++ b/src/zorn.agda Tue Aug 30 14:30:36 2022 +0900 @@ -765,6 +765,12 @@ pcy1 : odef pchain1 y pcy1 = ⟪ ay , ch-init (init ay refl) ⟫ + supf1≤sp1 : {a : Ordinal } → supf1 a o≤ sp1 + supf1≤sp1 = ? + + supf-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b + supf-mono = ? + -- zc100 : xSUP (UnionCF A f mf ay supf0 px) x → x ≡ sp1 -- zc100 = ? @@ -776,8 +782,6 @@ no-extension ¬sp=x = record { supf = supf1 ; sup = sup ; supf-mono = supf-mono ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = ptotal1 } where - supf-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b - supf-mono = ? pchain0=1 : pchain ≡ pchain1 pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z @@ -825,27 +829,57 @@ ... | ⟪ 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 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 + ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (o<→≤ a) + record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup) } (init (A∋fcs _ f mf fc) 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} → 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) ) eq1 ( ChainP.order u1-is-sup (subst₂ (λ j k → j o< k) (sym eq2) (sym eq1) 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 (subst₂ (λ j k → j o< k) (sym eq2) (sym eq1) 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 zc14 a ))) where -- px o< s < u1 < px + zc14 : s o< u1 + zc14 = ZChain.supf-inject zc s<u1 + ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (o≤-refl0 b) + record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup) } (init (A∋fcs _ f mf fc) 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 )) eq1 ( 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 ? ) + ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup (subst₂ (λ j k → j o< k) (sym eq2) (sym eq1) 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 (subst₂ (λ j k → j o< k) (sym eq2) (sym eq1) 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 zc14))) where -- px o< s < u1 = px + zc14 : s o< u1 + zc14 = ZChain.supf-inject zc s<u1 + ... | tri> ¬a ¬b px<u1 | record { eq = eq2 } = ⊥-elim ? where + 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 ) refl 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 px) k ) (sym &iso) 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 (UnionCF A f mf ay supf0 px) x + zcsup = record { ax = subst (λ k → odef A k) zc32 asp ; is-sup = record { x<sup = zc34 } } + 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) @@ -992,7 +1026,7 @@ no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) ∨ HasPrev A pchain x f → ZChain A f mf ay x no-extension ¬sp=x = record { initial = pinit ; chain∋init = pcy ; supf = supf1 ; sup=u = sup=u ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} - ; csupf = {!!} ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } where + ; csupf = csupf ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } where supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z pchain0=1 : pchain ≡ pchain1 @@ -1020,19 +1054,19 @@ sup {z} z≤x with trio< z x ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup (pzc (osuc z) {!!}) {!!} ) ... | tri≈ ¬a b ¬c = {!!} - ... | tri> ¬a ¬b c = {!!} + ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup {!!})) - sis {z} z<x with trio< z x + sis {z} z≤x with trio< z x ... | tri< a ¬b ¬c = {!!} where zc8 = ZChain.supf-is-sup (pzc z a) {!!} ... | tri≈ ¬a b ¬c = {!!} - ... | tri> ¬a ¬b c = {!!} + ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z 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 x + sup=u {z} ab z≤x is-sup with trio< z x ... | 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) + ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) + csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 (supf1 z)) (supf1 z) csupf {z} z≤x with trio< z x ... | tri< a ¬b ¬c = ? where zc9 : odef (UnionCF A f mf ay supf1 z) (ZChain.supf (pzc (osuc z) (ob<x lim a)) z) @@ -1040,7 +1074,7 @@ zc8 : odef (UnionCF A f mf ay (supfu a) z) (ZChain.supf (pzc (osuc z) (ob<x lim a)) z) zc8 = {!!} -- ZChain.csupf (pzc (osuc z) (ob<x lim a)) ? -- (o<→≤ <-osuc ) ... | tri≈ ¬a b ¬c = {!!} - ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z {!!} )) + ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x)