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

comparison src/zorn.agda @ 784:d83b0f7ece32

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 01 Aug 2022 10:46:21 +0900
parents	195c3c7de021
children	7472e3dc002b

comparison

equal deleted inserted replaced

-:195c3c7de021
+:d83b0f7ece32
 record SUP ( A B : HOD )  : Set (Level.suc n) where
 field
 sup : HOD
 A∋maximal : A ∋ sup
 x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
-min-sup : {z : HOD } → B ∋ z → ( {x : HOD } → B ∋ x → (x ≡ z ) ∨ (x < z ) )
-→ (z ≡ sup ) ∨ (sup < z )
 --
 --  sup and its fclosure is in a chain HOD
 --    chain HOD is sorted by sup as Ordinal and <-ordered
 --    whole chain is a union of separated Chain
 f-total : IsTotalOrderSet chain
 sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
 sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b
-csupf : (z : Ordinal ) → odef chain (supf 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)
+csupf = ?
 fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
-order : {b sup1 z1 : Ordinal} → b o< z → supf sup1 o< supf b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  , ? ⟫
-supf∈A : {u : Ordinal } → odef A (supf u)
-supf∈A = ?
-fcy<sup'  : {u w : Ordinal } → u o< z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
-fcy<sup'  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  , ? ⟫
 ... | case1 eq = ?
 ... | case2 lt = ?
-fc∈A : {s z1 : Ordinal} → FClosure A f (supf s) z1 → odef chain z1
+order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
-fc∈A {s} (fsuc x fc) = f-next (fc∈A {s} fc )  -- (supf s) ≡ z1 → init (supf s)
+order {b} {s} {.(f x)} b<z sf<sb (fsuc x fc) with proj1 (mf x (A∋fc _ f mf fc)) | order b<z sf<sb fc
-order' : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
-order' {b} {s} {.(f x)} b<z sf<sb (fsuc x fc) with proj1 (mf x (A∋fc _ f mf fc)) | order' b<z sf<sb fc
 ... | case1 eq | t = ?
 ... | case2 lt | t = ?
-order' {b} {s} {z1} b<z sf<sb (init x refl) = ? where
+order {b} {s} {z1} b<z sf<sb (init x refl) = ? where
 zc01 : s o≤ z
 zc01 = ?
 zc00 : ( * (supf s)  ≡  SUP.sup (sup (o<→≤ b<z ))) ∨ ( * (supf s)  < SUP.sup ( sup (o<→≤ b<z )) )
-zc00 with csupf' zc01
+zc00 with csupf zc01
 ... | ⟪ ss , ch-init fc ⟫ = SUP.x<sup (sup (o<→≤ b<z)) ⟪ ? , ch-init ? ⟫
 ... | ⟪ ss , ch-is-sup us is-sup fc  ⟫ = SUP.x<sup (sup (o<→≤ b<z)) ⟪ ? , ch-is-sup us ? ? ⟫
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 record Maximal ( A : HOD )  : Set (Level.suc n) where
 field
 maximal : HOD
 A∋maximal : A ∋ maximal
 ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
---
-supf-unique : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)
-→ {a b : Ordinal } → a o< b
-→ (za : ZChain A f mf ay (osuc a) ) → (zb : ZChain A f mf ay (osuc b) )
-→ odef (UnionCF A f mf ay (ZChain.supf za) (osuc a)) (ZChain.supf za a)
-→ odef (UnionCF A f mf ay (ZChain.supf zb) (osuc b)) (ZChain.supf zb a) → ZChain.supf za a ≡ ZChain.supf zb a
-supf-unique A f mf {y} ay {a} {b} a<b za zb ⟪ aa , ch-init fca ⟫ ⟪ ab , ch-init fcb ⟫ = ? where
-supf = ZChain.supf za
-supb = ZChain.supf zb
-su00 :  {u w : Ordinal } → u o< osuc a  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u )
-su00 = ZChain.fcy<sup za
-su01 :  (supf a ≡ supb b ) ∨ ( supf a << supb b )
-su01 = ZChain.fcy<sup zb <-osuc fca
-su02 :  (supb a ≡ supf a ) ∨ ( supb a << supf a )
-su02 = ZChain.fcy<sup za <-osuc fcb
-supf-unique A f mf {y} ay {a} a<b za zb ⟪ aa , ch-init fca ⟫ ⟪ ab , ch-is-sup ub is-supb fcb ⟫ = ?
-supf-unique A f mf {y} ay {a} a<b za zb ⟪ aa , ch-is-sup ua is-supa fca ⟫ ⟪ ab , ch-init fcb ⟫ = ?
-supf-unique A f mf {y} ay {a} a<b za zb ⟪ aa , ch-is-sup ua is-supa fca ⟫ ⟪ ab , ch-is-sup ub is-supb fcb ⟫ = ?
 -- data UChain is total
 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
 {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
 pcy : odef pchain y
 pcy = ⟪ ay , ch-init (init ay refl)    ⟫
 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 is-sup fc ⟫ = ⟪ az , ch-is-sup u 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 = {!!} ; order = {!!} ; fcy<sup = {!!}
 zc20 : {z : Ordinal } → z ≡ x → spu ≡ psupf x
 zc20 {z} z=x with trio< z x | inspect psupf z
 ... | tri< a ¬b ¬c | _ = ⊥-elim ( ¬b z=x)
 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = subst (λ k → spu ≡ psupf k) b (sym eq1)
 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬b z=x)
-order :  {b sup1 z1 : Ordinal} → b o< x →
-psupf sup1 o< psupf b →
-FClosure A f (psupf sup1) z1 → (z1 ≡ psupf b) ∨ (z1 << psupf b)
-order {b} {s} {z1}  b<x ps<pb fc with trio< b x
-... | tri< a ¬b ¬c = ZChain.order uzc <-osuc zc21 zc20 where
-uzc = pzc (osuc b) (ob<x lim a)
-zc22 : psupf s ≡ ZChain.supf uzc s
-zc22 with trio< s x
-... | tri< s<x ¬b ¬c = zc23 where
-szc = pzc (osuc s) (ob<x lim s<x)
-zc23 :  ZChain.supf (pzc (osuc s) (ob<x lim s<x)) s ≡ ZChain.supf (pzc (osuc b) (ob<x lim a)) s
-zc23 = ?
-zc24 : odef (UnionCF A f mf ay (ZChain.supf (pzc (osuc s) (ob<x lim s<x))) (osuc s))
-(ZChain.supf (pzc (osuc s) (ob<x lim s<x)) s )
-zc24 = ZChain.csupf (pzc (osuc s) (ob<x lim s<x)) s
-zc25 : odef (UnionCF A f mf ay (ZChain.supf (pzc (osuc b) (ob<x lim a))) (osuc b))
-(ZChain.supf (pzc (osuc b) (ob<x lim a)) b )
-zc25 = ZChain.csupf (pzc (osuc b) (ob<x lim a)) b
-... | tri≈ ¬a b ¬c = ?
-... | tri> ¬a ¬b c = ?
-zc21 :  ZChain.supf uzc s o< ZChain.supf uzc b
-zc21 = subst (λ k → k o< _) zc22 ps<pb
-zc20 : FClosure A f (ZChain.supf uzc s ) z1
-zc20 = subst (λ k → FClosure A f k z1) zc22 fc
-... | tri≈ ¬a b ¬c = ⊥-elim (¬a b<x)
-... | tri> ¬a ¬b c = ⊥-elim (¬a b<x)
-csupf : (z : Ordinal) → odef (UnionCF A f mf ay psupf x) (psupf z)
-csupf z with trio< z x | inspect psupf z
-... | tri< z<x ¬b ¬c | record { eq = eq1 } = zc11 where
-ozc = pzc (osuc z) (ob<x lim z<x)
-zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z)
-zc12  = ZChain.csupf ozc z
-zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
-zc11 = ⟪ az , ch-is-sup z cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az refl) ) ⟫ where
-az : odef A ( ZChain.supf ozc z )
-az = proj1 zc12
-zc20 : {z1  : Ordinal} → FClosure A f y z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
-zc20 {z1} fc with ZChain.fcy<sup ozc <-osuc fc
-... | case1 eq = case1 (trans eq (sym eq1) )
-... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
-cp1 : ChainP A f mf ay psupf z (ZChain.supf ozc z)
-cp1 = record {  fcy<sup = zc20   ; order = order z<x  }
----  u = supf u = supf z
-... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup {!!} {!!} {!!} ⟫ where
-sa = SUP.A∋maximal usup
-... | tri> ¬a ¬b c | record { eq = eq1 } = {!!}
 fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → (w ≡ psupf u) ∨ (w << psupf u)
 fcy<sup {u} {w} u<x fc with trio< u x
 ... | tri< a ¬b ¬c = ZChain.fcy<sup uzc <-osuc fc where
 ... | ⟪ ab0 , ch-is-sup u is-sup fc ⟫ = ⟪ ab ,
 subst (λ k → UChain A f mf ay supf x k )
 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫
 no-extension : ZChain A f mf ay x
-no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; sup=u = {!!} ; order = order ; fcy<sup = fcy<sup
+no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; sup=u = {!!}
 ; supf-mono = {!!} ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
 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 )

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

comparison src/zorn.agda @ 784:d83b0f7ece32