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

comparison src/zorn.agda @ 797:3a8493e6cd67

supf contraint

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 06 Aug 2022 15:06:58 +0900
parents	171123c92007
children	9cf74877efab

comparison

equal deleted inserted replaced

-:171123c92007
+:3a8493e6cd67
 f-total : IsTotalOrderSet chain
 sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
 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
 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤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)
-supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
+supf≤x :{x : Ordinal } → z o≤ x → supf z ≡  supf x
+supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
+supf-mono {x} {y} x<y = ? where
+--   z o≤ x → supf x ≡ supf y ≡ supf z
+--   x o< z → z o< y → supf x ≡ supf y ≡ supf z
+sf<sy : supf x o≤ supf y
+sf<sy with trio< x z
+... | tri> ¬a ¬b c = o≤-refl0 (( trans (sym (supf≤x (o<→≤ c))) (supf≤x (ordtrans (ordtrans c x<y ) <-osuc ) ) ))
+... | tri≈ ¬a b ¬c = o≤-refl0 (trans (sym (supf≤x (o≤-refl0 (sym b)))) (supf≤x (subst (λ k → k o< osuc y) b (o<→≤ x<y))))
+... | tri< x<z ¬b ¬c with trio< y z
+... | tri> ¬a ¬b c = ?
+... | tri≈ ¬a b ¬c = ?
+... | tri< y<z ¬b ¬c with csupf (o<→≤ x<z) | csupf (o<→≤ y<z)
+... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-init fcy ⟫  = ?
+... | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-init fcy ⟫  = ?
+... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ?
+... | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ?
+-- ... | tri< a ¬b ¬c = csupf (o<→≤ a)
+-- ... | tri≈ ¬a b ¬c = csupf (o≤-refl0 b)
+-- ... | tri> ¬a ¬b c = subst (λ k → odef (UnionCF A f mf ay supf x) k ) ? (csupf ? )
+-- csy : odef (UnionCF A f mf ay supf y) (supf y)
+-- csy = 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
 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)
 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫
 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) ))
 ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
 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} {z1} b<z sf<sb fc = zc04 where
 zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
 zc01  (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc03  where
 s<b : s o< b
 s<b with trio< s b
 ... | tri< a ¬b ¬c = a
 ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (cong supf b) sf<sb )
 ... | tri> ¬a ¬b c with osuc-≡< ( supf-mono c )
 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sf<sb )
 ... | case2 lt = ⊥-elim ( o<> lt  sf<sb   )
 s<z : s o< z
 s<z = ordtrans s<b b<z
 zc03 : odef (UnionCF A f mf ay supf b)  (supf s)
-zc03 with csupf s<z
+zc03 with csupf (o<→≤ s<z )
 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫
 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u≤x (osucc s<b)) is-sup fc ⟫
 zc01  (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
 zc04 : odef (UnionCF A f mf ay supf b) (f x)
 zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (zc01 fc  )
 ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫
 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
 zc00 : ( * z1  ≡  SUP.sup (sup (o<→≤ b<z) )) ∨ ( * z1  < SUP.sup ( sup (o<→≤ b<z) ) )
 zc00 = SUP.x<sup (sup (o<→≤ b<z)) (zc01 fc )
 zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
 zc04 with zc00
 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup  (o<→≤ b<z) ) ) (cong (&) eq) )
 ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (supf-is-sup (o<→≤ b<z) ) )))  lt )
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
 field
 uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb))
 pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
 pchain⊆A {y} ny = proj1 ny
 pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
 pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u {!!} is-sup (fsuc _ fc ) ⟫
+pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫
 pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
 pinit {a} ⟪ aa , ua ⟫  with  ua
 ... | ch-init fc = s≤fc y f mf fc
 ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
 zc7 : y <= (ZChain.supf zc) u
 subst (λ k → UChain A f mf ay supf x k )
 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫
 no-extension : ¬ spu ≡ x → ZChain A f mf ay x
 no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = {!!}
-; sup = {!!} ; supf-is-sup = {!!}
+; sup = sup ; supf-is-sup = sis
-; csupf = {!!} ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; supf-mono = {!!} } where
+; csupf = csupf ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; supf-mono = {!!} } 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 x ⊆' UnionCF A f mf ay (supfu a) x
 UnionCF⊆ = {!!}
+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⊆ {!!} (ZChain.sup (pzc z a) o≤-refl )
+... | tri≈ ¬a b ¬c = SUP⊆ {!!} usup
+... | tri> ¬a ¬b c = SUP⊆ {!!} 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
+... | tri> ¬a ¬b c with osuc-≡< z≤x
+... | case1 eq = ⊥-elim ( ¬b eq )
+... | 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 <-osuc 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)
+csupf {z} z<x with trio< z x
+... | tri< a ¬b ¬c = zc9 where
+zc9 : odef (UnionCF A f mf ay supf1 z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
+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 = ? -- ⊥-elim (¬a z<x)
+... | tri> ¬a ¬b c = ? -- ⊥-elim (¬a z<x)
+supf-mono :  {a b : Ordinal}  → a o< b → supf1 a o≤ supf1 b
+supf-mono {a0} {b0} a<b = zc10 where
+--  x o≤ a → supf1 a ≡ supf1 b ≡ spu
+--  x o≤ b → supf1 b ≡ spu
+--  a o< x → b o≤ x →   supf1 (supf1 a) ≡ supf1 a
+--                      supf1 (supf1 b) ≡ supf1 b
+usa : odef (UnionCF A f mf ay (supfu ?) (osuc a0)) (supf1 a0)
+usa = ?
+usb : odef (UnionCF A f mf ay (supfu ?) (osuc b0)) (supf1 b0)
+usb = ?
+zc10 : supf1 a0 o≤ supf1 b0
+zc10 with trio< a0 x | trio< b0 x
+... | tri< a ¬b ¬c | tri< a' ¬b' ¬c' = ? where
+zc11 = ZChain.supf-mono (pzc (osuc a0)  (ob<x lim a)) a<b
+zc12 = ZChain.supf-mono (pzc (osuc b0)  (ob<x lim a')) a<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' = ?
+... | tri≈ ¬a b ¬c | tri≈ ¬a' b' ¬c' = ?
+... | tri≈ ¬a b ¬c | tri> ¬a' ¬b c = ?
+... | tri> ¬a ¬b c | _ = ?
 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

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

comparison src/zorn.agda @ 797:3a8493e6cd67