Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 808:81018623e3c5
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 15 Aug 2022 18:02:27 +0900 |
| parents | 2141154c521b |
| children | ab5aa49abde0 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 59 insertions(+), 44 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Aug 12 15:16:50 2022 +0900 +++ b/src/zorn.agda Mon Aug 15 18:02:27 2022 +0900 @@ -702,40 +702,55 @@ ax : odef A x not-sup : IsSup A (UnionCF A f mf ay supf0 x) ax - UnionCF⊆ : {u x : Ordinal} → (a : u o≤ x ) → UnionCF A f mf ay supf0 u ⊆' UnionCF A f mf ay supf1 x - UnionCF⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ - UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫ - UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with - UnionCF⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ - ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ - ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ - UnionCFR⊆ : {u x : Ordinal} → (a : u o≤ x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay supf0 x - UnionCFR⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ - UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫ - UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with - UnionCFR⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ - ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ - ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ + UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) → (z1≤x : z1 o≤ x ) + → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1 + UnionCF⊆ {z0} {z1} z0≤1 z1≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ + UnionCF⊆ {z0} {z1} z0≤1 z1≤x ⟪ 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 ) + record { fcy<sup = ? ; order = ? ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup) } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 ) ⟫ + ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) + record { fcy<sup = ? ; order = ? ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup) } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 ) ⟫ + ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } = ? where + zc31 : supf0 u1 ≡ u1 + zc31 = ChainP.supu=u u1-is-sup + zc32 : u1 o≤ x + zc32 = OrdTrans u1≤x (OrdTrans z0≤1 z1≤x ) + zc30 : x ≡ u1 + zc30 with osuc-≡< zc32 + ... | case1 eq = sym (eq) + ... | case2 u1<x = ⊥-elim (¬p<x<op ⟪ px<u1 , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op)) u1<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₁) ⟫ no-extension : ¬ xSUP → ZChain A f mf ay x no-extension ¬sp=x = record { supf = supf1 ; sup = sup ; 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 = ? } where + ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = ptotal1 } where + UnionCFR⊆ : {u x : Ordinal} → (a : u o≤ x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay supf0 x + UnionCFR⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ + UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫ + UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = ? -- with +-- UnionCFR⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ +-- ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ +-- ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , 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⊆ ?) ( ZChain.sup zc (o<→≤ a) ) - ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCFR⊆ ?) ( ZChain.sup zc (subst (λ k → k o≤ px) (sym b) o≤-refl )) - ... | tri> ¬a ¬b c = ? + ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ {!!}) ( ZChain.sup zc (o<→≤ a) ) + ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCFR⊆ {!!}) ( ZChain.sup zc (subst (λ k → k o≤ px) (sym b) o≤-refl )) + ... | tri> ¬a ¬b c = {!!} sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc 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) ? - ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) ? - ... | tri> ¬a ¬b c = ? + ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) {!!} + ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) {!!} + ... | tri> ¬a ¬b c = {!!} csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b) csupf {b} b≤x with trio< b px - ... | tri< a ¬b ¬c = UnionCF⊆ o≤-refl ( ZChain.csupf zc (o<→≤ a) ) - ... | tri≈ ¬a b ¬c = UnionCF⊆ o≤-refl ( ZChain.csupf zc (subst (λ k → k o≤ px) (sym b) o≤-refl )) - ... | tri> ¬a ¬b px<b = ⟪ ? , ch-is-sup b o≤-refl ? ? ⟫ where + ... | tri< a ¬b ¬c = UnionCF⊆ ? ? ( ZChain.csupf zc (o<→≤ a) ) + ... | tri≈ ¬a b ¬c = UnionCF⊆ ? ? ( ZChain.csupf zc (subst (λ k → k o≤ px) (sym b) o≤-refl )) + ... | tri> ¬a ¬b px<b = ⟪ {!!} , ch-is-sup b o≤-refl {!!} {!!} ⟫ where -- px< b ≤ x -- b ≡ x, supf x ≡ sp1 , ¬ x ≡ sp1 zc30 : x ≡ b @@ -743,7 +758,7 @@ ... | 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 ⟫ ) sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x)) - sis = ? + sis = {!!} zc4 : ZChain A f mf ay x zc4 with ODC.∋-p O A (* x) ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip @@ -767,12 +782,12 @@ 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 } = ⟪ ? , ? ⟫ - ... | tri> ¬a ¬b c | record { eq = eq1 } = ? where -- b ≡ x, supf x ≡ sp + ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫ + ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!} where -- b ≡ x, supf x ≡ sp zc30 : x ≡ b zc30 with trio< x b ... | tri< a ¬b ¬c = ? - ... | tri≈ ¬a b ¬c = b + ... | tri≈ ¬a b ¬c = ? ... | tri> ¬a ¬b c = ? ... | case2 ¬x=sup = no-extension {!!} -- px is not f y' nor sup of former ZChain from y -- no extention @@ -856,23 +871,23 @@ supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay (supfu a) x UnionCF⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ - UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫ - UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with - UnionCF⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ - ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ - ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ + UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫ + UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = ? -- with +-- UnionCF⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ +-- ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ +-- ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ UnionCF0⊆ : {z : Ordinal} → (a : z o≤ x ) → UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay psupf0 x UnionCF0⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ - UnionCF0⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫ - UnionCF0⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with - UnionCF0⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ - ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ - ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ + UnionCF0⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫ + UnionCF0⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = ? -- with +-- UnionCF0⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ +-- ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ +-- ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , 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 x - ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) ?) ? ) - ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCF0⊆ ?) usup - ... | tri> ¬a ¬b c = SUP⊆ (UnionCF0⊆ ?) usup + ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) {!!}) {!!} ) + ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCF0⊆ {!!}) usup + ... | tri> ¬a ¬b c = SUP⊆ (UnionCF0⊆ {!!}) usup sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup x≤z)) sis {z} z≤x with trio< z x ... | tri< a ¬b ¬c = {!!} where @@ -883,7 +898,7 @@ ... | case2 lt = ⊥-elim ( ¬a lt ) sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b sup=u {b} ab b<x is-sup with trio< b 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 b) (ob<x lim a)) ab {!!} record { x<sup = {!!} } ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b c = {!!} csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z) @@ -893,7 +908,7 @@ 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 ) - ... | tri≈ ¬a b ¬c = ? + ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x)) zc5 : ZChain A f mf ay x @@ -905,7 +920,7 @@ ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax ) ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!} ; supf = supf1 ; sup=u = {!!} ; sup = {!!} ; supf-is-sup = {!!} - ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} } where -- x is a sup of (zc ?) + ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} } -- where -- x is a sup of (zc ?) ... | case2 ¬x=sup = no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A)