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

comparison src/zorn.agda @ 754:db177d911091

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 23 Jul 2022 18:40:35 +0900
parents	b96491f7c775
children	b22327e78b03

comparison

equal deleted inserted replaced

-:b96491f7c775
+:db177d911091
 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
-sup=u : {b : Ordinal} → {ab : odef A b} → b o< z → IsSup A chain ab → supf b ≡ b
+csupf : {z : Ordinal } → odef chain (supf z)
-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
 field
 chain-mono2 : { a b c : Ordinal }  →
 zc1 x prev with Oprev-p x
 ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = ? ; sup=u = ? ; order = ? } where
 px = Oprev.oprev op
 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
+fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → w << ZChain.supf zc u
+fcy<sup {u} {w} u<x fc = ?
 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
 is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b
 sp1 : SUP A (ZChain.chain zc)
 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total
 c = & (SUP.sup sp1)
 inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
-inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy
+inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; csupf = ?
 ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
 isupf : Ordinal → Ordinal
 isupf z = y
 cy : odef (UnionCF A f mf ay isupf o∅) y
 cy = ⟪ ay , ch-init (init ay)  ⟫
 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 = ZChain.supf zc
+csupf : {z : Ordinal} → odef (UnionCF A f mf ay supf0 x) (supf0 z)
+csupf {z} with ZChain.csupf zc {z}
+... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
+... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u (ordtrans u<px px<x ) is-sup fc ⟫
 -- 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 = pinit ; chain∋init = pcy  ; csupf = csupf
-;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ;  order = order } where
+;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
-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
-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  ⟫
-... | 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 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)
 ... | no noapx = no-extension -- ¬ A ∋ p, just skip
 ... | 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 = ? ; csupf = ?
-; initial = ? ; chain∋init  = ? ; sup=u = ? ; order = ? }  where
+; initial = ? ; chain∋init  = ? }  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
 zc7 : y << psupf0 ?
 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
-;  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)
 psupf : Ordinal → Ordinal
 psupf z with trio< z x
 ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
 ... | tri≈ ¬a b ¬c = spu
 ... | tri> ¬a ¬b c = spu
+csupf :{z : Ordinal} → odef (UnionCF A f mf ay psupf x) (psupf z)
+csupf {z} with trio< z x
+... | tri< a ¬b ¬c = zc11 where
+zc11 : odef A (ZChain.supf (pzc z a) z) ∧ UChain A f mf ay psupf x (ZChain.supf (pzc z a) z)
+zc11 with  ZChain.csupf (pzc z a) {z}
+... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
+... | ⟪ az , ch-is-sup u u<z is-sup fc ⟫ = ⟪ az , ch-is-sup u (ordtrans u<z a)  ? (pfc a fc)  ⟫
+... | tri≈ ¬a b ¬c = ?
+... | tri> ¬a ¬b c = ?
+no-extension : ZChain A f mf ay x
+no-extension  = record { initial = ? ; chain∋init = ?  ; supf = psupf  ; csupf = ?
+;  chain⊆A = ? ;  f-next = ? ;  f-total = ? }
 zc5 : ZChain A f mf ay x
 zc5 with ODC.∋-p O A (* x)
 ... | 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  ; csupf = ?
 ;  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 @ 754:db177d911091