Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 811:e09ba00c9b85

nvim-agda bug in zorn.agda

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Tue, 16 Aug 2022 14:34:54 +0900
parents	ae0f958e648b
children	96e6643c833d

comparison

equal deleted inserted replaced

-:ae0f958e648b
+:e09ba00c9b85
 --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x
 record xSUP : Set n where
 field
 ax : odef A x
-not-sup : IsSup A (UnionCF A f mf ay supf0 x) ax
+is-sup : IsSup A (UnionCF A f mf ay supf0 x) ax
 UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) →  (z0≤px :  z0 o≤ px ) → (z1≤x :  z1 o≤ x )
 → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1
 UnionCF⊆ {z0} {z1} z0≤1 z0≤px z1≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫
 UnionCF⊆ {z0} {z1} z0≤1 z0≤px z1≤x ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
 ... | ⟪ 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 = 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⊆ : {z0 z1 : Ordinal} → z0 o≤ z1 → z0 o≤ x → z1 o≤ px → UnionCF A f mf ay supf1 z0 ⊆' UnionCF A f mf ay supf0 z1
-UnionCFR⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫
+UnionCFR⊆ {z0} {z1} z0≤1 z0≤x z1≤px ⟪ 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⊆ {z0} {z1} z0≤1 z0≤x z1≤px ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
-UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = ? -- with
+zc60 : {w : Ordinal } → FClosure A f (supf1 u1) w → odef (UnionCF A f mf ay supf0 z1 ) w
---                         UnionCFR⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫
+zc60 {w} (init asp refl) with trio< u1 px | inspect supf1 u1
---                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
+... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 )
---                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
+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 )) 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) ) 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 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 )) 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) ) 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) )
+... | 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
+? ≡⟨ ? ⟩
+? ∎ where open ≡-Reasoning
+zcsup : xSUP
+zcsup = record { ax = subst (λ k → odef A k) zc32 asp ; is-sup = record { x<sup = {!!}  } }
+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⊆ {!!}) ( ZChain.sup zc (o<→≤ a) )
+... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl z≤x (o<→≤ a)) ( 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⊆ (UnionCFR⊆ o≤-refl z≤x (o≤-refl0 b)) ( ZChain.sup zc (subst (λ k → k o≤ px) (sym b) o≤-refl ))
-... | tri> ¬a ¬b c = {!!}
+... | tri> ¬a ¬b c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = {!!} }
 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
+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 (o<→≤ a) record { x<sup = {!!} }
-... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) {!!}
+... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) record { x<sup = {!!} }
-... | tri> ¬a ¬b c = {!!}
+... | tri> ¬a ¬b px<b = {!!} 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 ⟫ )
 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
-csupf {b} b≤x with trio< b px
+csupf {b} b≤x with trio< b px | inspect supf1 b
-... | tri< a ¬b ¬c = UnionCF⊆ o≤-refl (o<→≤ a) b≤x ( ZChain.csupf zc (o<→≤ a) )
+... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) b≤x ( ZChain.csupf zc (o<→≤ a) )
-... | tri≈ ¬a refl ¬c = UnionCF⊆ o≤-refl o≤-refl b≤x ( ZChain.csupf zc o≤-refl )
+... | tri≈ ¬a refl ¬c | _ = UnionCF⊆ o≤-refl o≤-refl b≤x ( ZChain.csupf zc o≤-refl )
-... | tri> ¬a ¬b px<b =  ⟪ {!!} , ch-is-sup b  o≤-refl {!!} {!!} ⟫  where
+... | 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))  ⟫
+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 ⟫ )
+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))
-sis = {!!}
+sis {z} z≤x = {!!}
 zc4 : ZChain A f mf ay x
 zc4 with ODC.∋-p O A (* x)
 ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )
 -- we have to check adding x preserve is-max ZChain A y f mf x
 ... | 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} 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 } = ⟪ {!!} , {!!} ⟫
 ... | 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 = {!!}
-... | tri≈ ¬a b ¬c = ?
+... | tri≈ ¬a b ¬c = {!!}
-... | 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
 ... | no lim = zc5 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
 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 ⟪ 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
+UnionCFR⊆ : {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 ⟫
+UnionCFR⊆ {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 {!!} {!!}) ⟫
+UnionCFR⊆ {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
+UnionCFR⊆ {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⊆ (UnionCFR⊆ {!!}) usup
-... | tri> ¬a ¬b c = SUP⊆ (UnionCF0⊆ {!!}) usup
+... | tri> ¬a ¬b c = SUP⊆ (UnionCFR⊆ {!!}) 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
 zc8 = ZChain.supf-is-sup (pzc z a) o≤-refl
 ... | tri≈ ¬a b ¬c = refl

Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/zorn.agda @ 811:e09ba00c9b85