Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 819:89c4e8f06ce1
xSUP on px
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 17 Aug 2022 14:32:33 +0900 |
| parents | 80df9b356e2c |
| children | d395f1827e6a |
| files | src/zorn.agda |
| diffstat | 1 files changed, 18 insertions(+), 23 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Aug 17 09:20:32 2022 +0900 +++ b/src/zorn.agda Wed Aug 17 14:32:33 2022 +0900 @@ -286,7 +286,7 @@ 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) + 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 (o<→≤ s<z ) + zc03 with csupf 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 @@ -700,7 +700,7 @@ record xSUP : Set n where field ax : odef A x - is-sup : IsSup A (UnionCF A f mf ay supf0 x) ax + 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 ⟫ @@ -789,8 +789,8 @@ supf1 u1 ≡⟨ zc33 ⟩ u1 ≡⟨ sym zc31 ⟩ x ∎ where open ≡-Reasoning - zc34 : {z : Ordinal} → odef (UnionCF A f mf ay supf0 x) 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) lt ) + 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 ⟩ @@ -814,32 +814,27 @@ 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 (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 = ? where + ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where zc30 : x ≡ b zc30 with osuc-≡< b≤x ... | 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 ⟫ ) - zcsup0 : supf1 b ≡ b - zcsup0 with zc30 | trio< b px - ... | refl | tri< a ¬b ¬c = ? - ... | refl | tri≈ ¬a b ¬c = ? - ... | refl | tri> ¬a ¬b c = refl zcsup : xSUP zcsup with zc30 - ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono ? ? ? ? ? (UnionCF⊆ o≤-refl ? 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 (o<→≤ a) ( ZChain.csupf zc (o<→≤ a) ) - ... | tri≈ ¬a refl ¬c | _ = UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl ) + ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ 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 b o≤-refl zc31 (subst (λ k → FClosure A f k sp1) (sym eq1) (init (SUP.as sup1) refl)) ⟫ + ⟪ 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-≡< b≤x - ... | 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 ⟫ ) + 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 = {!!} } sis : {z : Ordinal} (z<x : z o< x) → supf1 z ≡ & (SUP.sup (sup z<x)) @@ -864,7 +859,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 } = ⟪ {!!} , {!!} ⟫ @@ -984,15 +979,15 @@ ... | 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) zc9 = {!!} 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 ) + 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 z≤x)) + ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z ? )) zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x)