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

comparison src/zorn.agda @ 752:2be90b90deb3

dead end

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 23 Jul 2022 17:19:18 +0900
parents	71ad137dd101
children

comparison

equal deleted inserted replaced

-:71ad137dd101
+:2be90b90deb3
 chain⊆A : chain ⊆' A
 chain∋init : odef chain init
 initial : {y : Ordinal } → odef chain y → * init ≤ * y
 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
 f-total : IsTotalOrderSet chain
+chain∋supf : {z : Ordinal } → odef chain (supf z)
 sup=u : {b : Ordinal} → {ab : odef A b} → b o< z → IsSup A chain ab → supf b ≡ b
 order : {b sup1 z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f (supf sup1) z1 → z1 << supf b
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {init : Ordinal} (ay : odef A init)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
 ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab ,
 subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫
 zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
 zc1 x prev with Oprev-p x
-... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = fcy<sup ; sup=u = ? ; order = order } where
+... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = fcy<sup ; sup=u = sup=u ; order = order } where
 px = Oprev.oprev op
 px<x : px o< x
 px<x = subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc
 zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
 zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
 sup=u : {b : Ordinal} {ab : odef A b} → b o< x →
 IsSup A (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) ab → ZChain.supf zc b ≡ b
 sup=u {b} {ab} b<x is-sup with trio< b px
 ... | tri< b<px ¬b ¬c = ZChain1.sup=u (prev px px<x) b<px is-sup
-... | tri≈ ¬a b=px ¬c = ZChain.sup=u zc ? is-sup
+... | tri≈ ¬a b=px ¬c = ZChain.sup=u zc ? ?
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
 is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
 b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
 zc7 : y << (ZChain.supf zc) u
 zc7 = ChainP.fcy<sup is-sup (init ay)
 pcy : odef pchain y
 pcy = ⟪ ay , ch-init (init ay)    ⟫
-supf0 = ZChain.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))
+supf0 : Ordinal → Ordinal
+supf0 z with trio< z x
+... | tri< a ¬b ¬c = ZChain.supf zc z
+... | tri≈ ¬a b ¬c = ZChain.supf zc px
+... | tri> ¬a ¬b c = ZChain.supf zc px
+spuf0eq : {z : Ordinal} → z o< x → supf0 z ≡ ZChain.supf zc z
+spuf0eq {z} z<x with trio< z x
+... | tri< a ¬b ¬c = refl
+... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<x )
+... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<x )
+zc9 :  UnionCF A f mf ay (ZChain.supf zc) px ⊆'  UnionCF A f mf ay supf0 x
+zc9 ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
+zc9 {z} ⟪ az , ch-is-sup u u<px is-sup fc ⟫ with trio< z x
+... | tri< a ¬b ¬c = ⟪ az , ch-is-sup u (ordtrans u<px px<x) ? ? ⟫
+... | tri≈ ¬a b ¬c = ?
+... | tri> ¬a ¬b c = ?
+-- ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
+--- zc9 {z} ⟪ az , ch-is-sup u u<px is-sup fc ⟫ with trio< z x
+-- ... | tri< a ¬b ¬c = ⟪ az , ch-is-sup u (ordtrans u<px px<x) ? ? ⟫
+-- ... | tri≈ ¬a b ¬c = ?
+-- ... | tri> ¬a ¬b c = ?
+-- = ⟪ az , ch-is-sup u (ordtrans u<px px<x) ? ? ⟫
 -- if previous chain satisfies maximality, we caan reuse it
 --
 no-extension : ZChain A f mf ay x
 no-extension = record { supf = supf0
-; initial = pinit ; chain∋init = pcy  ; sup=u = sup=u
+; initial = ? ; chain∋init = ?  ; sup=u = sup=u  ; chain∋supf = ?
-;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ;  order = order } where
+;  chain⊆A = ?  ;  f-next = ? ;  f-total = ? ;  order = ? } where
+cs : {z : Ordinal} → odef (UnionCF A f mf ay supf0 x) (supf0 z)
+cs {z} with trio< z x
+... | tri< a ¬b ¬c = zc9 (ZChain.chain∋supf zc {z} )
+... | tri≈ ¬a b ¬c = ?
+... | tri> ¬a ¬b c = ?
+--- = subst (λ k → odef (UnionCF A f mf ay supf0 k) (supf0 z)) ? (ZChain.chain∋supf zc {z} )
 sup=u :  {b : Ordinal} {ab : odef A b} → b o< x
 → IsSup A (UnionCF A f mf ay supf0 x) ab
 → supf0 b ≡ b
 sup=u {b} {ab} b<x is-sup with trio< b px
-... | tri< a ¬b ¬c = ZChain.sup=u zc {b} {ab} a record { x<sup = pc20 } where
+... | tri< a ¬b ¬c = ? where --  ZChain.sup=u zc {b} {ab} a record { x<sup = pc20 } where
 pc20 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) z → (z ≡ b) ∨ (z << b)
 pc20 {z} ⟪ az , ch-init fc  ⟫ =
 IsSup.x<sup is-sup ⟪ az ,  ch-init fc  ⟫
 pc20 {z} ⟪ az , ch-is-sup u u<x is-sup-c fc  ⟫ = IsSup.x<sup is-sup
-⟪ az , ch-is-sup u (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc)) is-sup-c fc  ⟫
+⟪ az , ch-is-sup u (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc)) ? ?  ⟫
 ... | tri≈ ¬a refl ¬c = ?
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
 order : {b sup1 z1 : Ordinal} → b o< x → sup1 o< b → FClosure A f (supf0 sup1) z1 → z1 << supf0 b
 order {b} {s} {z1} b<x s<b fc with trio< b px
-... | tri< a ¬b ¬c = ZChain.order zc a s<b fc
+... | tri< a ¬b ¬c = ? -- ZChain.order zc a s<b ?
 ... | tri≈ ¬a refl ¬c = ?
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
 zc4 : ZChain A f mf ay x
 zc4 with ODC.∋-p O A (* px)
 ... | yes apx with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) apx f )
 -- we have to check adding x preserve is-max ZChain A y f mf x
 ... | case1 pr = no-extension -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx )
 ... | case1 is-sup = -- x is a sup of zc
-record {  supf = psupf1 ; chain⊆A = ? ; f-next = ? ; f-total = ?
+record {  supf = psupf1 ; chain⊆A = ? ; f-next = ? ; f-total = ? ; chain∋supf = ?
 ; initial = ? ; chain∋init  = ? ; sup=u = ? ; order = ? }  where
 psupf1 : Ordinal → Ordinal
 psupf1 z with trio< z x
 ... | tri< a ¬b ¬c = ZChain.supf zc z
 ... | tri≈ ¬a b ¬c = x
 ... | tri> ¬a ¬b c = x
+cA : UnionCF A f mf ay psupf1 x ⊆' A
+cA {z} uz with trio< z x
+... | tri< a ¬b ¬c = ZChain.chain⊆A zc ⟪ proj1 uz , ? ⟫
+... | 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
 pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
 pzc z z<x = prev z z<x
 zc7 = ChainP.fcy<sup is-sup (init ay)
 pcy : odef pchain y
 pcy = ⟪ ay , ch-init (init ay)    ⟫
 no-extension : ZChain A f mf ay x
-no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf0
+no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf0  ; chain∋supf = ?
 ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; sup=u = ? ; order = ? }
 usup : SUP A pchain
 usup = supP pchain (λ lt → proj1 lt) ptotal
 spu = & (SUP.sup usup)
 ... | no noax = no-extension -- ¬ A ∋ p, just skip
 ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )
 -- we have to check adding x preserve is-max ZChain A y f mf x
 ... | case1 pr = no-extension
 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; sup=u = ? ; order = ?
+... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; sup=u = ? ; order = ? ; chain∋supf = ?
 ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = ? } where -- x is a sup of (zc ?)
 psupf1 : Ordinal → Ordinal
 psupf1 z with trio< z x
 ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
 ... | tri≈ ¬a b ¬c = x

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

comparison src/zorn.agda @ 752:2be90b90deb3