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

comparison src/zorn.agda @ 957:ce42b1c5cf42

MinSup onlu ZChain1 is-max have to be hold all b o< z, by induction

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Thu, 03 Nov 2022 19:01:54 +0900
parents	a2b13a4b6727
children	33891adf80ea

comparison

equal deleted inserted replaced

-:a2b13a4b6727
+:ce42b1c5cf42
 ax : odef A x
 y : Ordinal
 ay : odef B y
 x=fy :  x ≡ f y
-record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
+-- record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
+--    field
+--       x≤sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
+record IsMinSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
 field
 x≤sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 minsup : { sup1 : Ordinal } → odef A sup1
 →  ( {z : Ordinal  } → odef B z → (z ≡ sup1 ) ∨ (z << sup1 ))  → x o≤ sup1
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
 field
 supf :  Ordinal → Ordinal
 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
-→ IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b
+→ IsMinSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b
 asupf :  {x : Ordinal } → odef A (supf x)
 supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
 supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
 -- ordering is not proved here but in ZChain1
 IsSup< : {b x : Ordinal }  (ab : odef A b )
 → b o< x
-→ IsSup A (UnionCF A f mf ay supf x) ab → IsSup A (UnionCF A f mf ay supf b) ab
+→ IsMinSup A (UnionCF A f mf ay supf x) ab → IsMinSup A (UnionCF A f mf ay supf b) ab
 IsSup< {b} {x}  ab b<x is-sup = record {
-x≤sup =  λ {z} uz → IsSup.x≤sup is-sup (chain-mono f mf ay supf supf-mono (o<→≤ b<x) uz)
+x≤sup =  λ {z} uz → IsMinSup.x≤sup is-sup (chain-mono f mf ay supf supf-mono (o<→≤ b<x) uz)
 ; minsup = m07 } where
 m10 : {s : Ordinal }  →  (odef A s )
 →  ( {w : Ordinal} → odef (UnionCF A f mf ay supf b) w → (w ≡ s) ∨ (w << s) )
 →    {w : Ordinal} → odef (UnionCF A f mf ay supf x) w → (w ≡ s) ∨ (w << s)
 m10 {s} as b-is-sup ⟪ aa , ch-init fc ⟫ = ?
 m01 : w <= s
 m01 with trio< (supf u) (supf b)
 ... | tri< a ¬b ¬c = b-is-sup ⟪ aa , ch-is-sup u {w} a is-sup-z fc ⟫
 ... | tri≈ ¬a b ¬c = ?
 ... | tri> ¬a ¬b c = ?
--- <=-trans (IsSup.x≤sup is-sup ⟪ aa , ch-is-sup u u<x is-sup-z fc ⟫) b<=s
+-- <=-trans (IsMinSup.x≤sup is-sup ⟪ aa , ch-is-sup u u<x is-sup-z fc ⟫) b<=s
 m07 :  {s : Ordinal} → odef A s → ({z : Ordinal} →
 odef (UnionCF A f mf ay supf b) z → (z ≡ s) ∨ (z << s)) → b o≤ s
-m07 {s} as b-is-sup = IsSup.minsup is-sup as (m10 as b-is-sup )
+m07 {s} as b-is-sup = IsMinSup.minsup is-sup as (m10 as b-is-sup )
 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
 supf = ZChain.supf zc
 field
 is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → supf b o< supf z  → (ab : odef A b)
-→ HasPrev A (UnionCF A f mf ay supf z) b f ∨  IsSup A (UnionCF A f mf ay supf z) ab
+→ HasPrev A (UnionCF A f mf ay supf z) b f ∨  IsMinSup A (UnionCF A f mf ay supf b) ab
 → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
 order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
 record Maximal ( A : HOD )  : Set (Level.suc n) where
 px = Oprev.oprev op
 zc-b<x : {b : Ordinal } → ZChain.supf zc b o< ZChain.supf zc x → b o< osuc px
 zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt  )
 is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
 ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
-HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
+HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsMinSup A (UnionCF A f mf ay supf b) ab →
 * a < * b → odef (UnionCF A f mf ay supf x) b
 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
 is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
 is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup
 = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
 m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
 chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
 m05 : ZChain.supf zc b ≡ b
 m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )
-⟪ record { x≤sup = λ {z} uz → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz)
+⟪ record { x≤sup = λ {z} uz → IsMinSup.x≤sup (proj2 is-sup) ? -- (chain-mono1 (o<→≤ b<x) uz)
 ; minsup = m07 }  , m04 ⟫ where
 m10 : {s : Ordinal }  →  (odef A s )
 →  ( {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s) )
-→    {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) z → (z ≡ s) ∨ (z << s)
+→    {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s)
 m10 = ?
 m07 :  {s : Ordinal} → odef A s → ({z : Ordinal} →
 odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s)) → b o≤ s
-m07 {s} as s-is-sup = IsSup.minsup (proj2 is-sup) as (m10 as s-is-sup)
+m07 {s} as s-is-sup = ? -- IsSup.minsup (proj2 is-sup) as (m10 as s-is-sup)
 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
 m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
 m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
 m09 {s} {z} s<b fcz = order b<A s<b fcz
 m06 : ChainP A f mf ay supf b
 m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
 ... | no lim = record { is-max = is-max ; order = order }  where
 is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
 ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
-HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
+HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsMinSup A (UnionCF A f mf ay supf b) ab →
 * a < * b → odef (UnionCF A f mf ay supf x) b
 is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P
 is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
-is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsSup.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
+is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsMinSup.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
 ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
 ... | case2 y<b = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
 m09 : b o< & A
 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
 b<x : b o< x
 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
 chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp)
 ; x=fy = HasPrev.x=fy nhp } )
 m05 : ZChain.supf zc b ≡ b
 m05 = ZChain.sup=u zc ab (o<→≤  m09)
-⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) lt )
+⟪ record { x≤sup = λ lt → IsMinSup.x≤sup (proj2 is-sup) ? -- (chain-mono1 (o<→≤ b<x) lt )
 ; minsup = ? } , m04 ⟫    -- ZChain on x
 m06 : ChainP A f mf ay supf b
 m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
 SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x≤sup = λ lt → SUP.x≤sup sup (B⊆C lt)    }
 record xSUP (B : HOD) (x : Ordinal) : Set n where
 field
 ax : odef A x
-is-sup : IsSup A B ax
+is-sup : IsMinSup A B ax
 --
 -- create all ZChains under o< x
 --
 ... | tri> ¬a ¬b c = zc36 ¬b
 ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ?  } where
 zc37 : MinSUP A (UnionCF A f mf ay supf0 z)
 zc37 = record { sup = ? ; asm = ? ; x≤sup = ? }
 sup=u : {b : Ordinal} (ab : odef A b) →
-b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b
+b o≤ x → IsMinSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b
 sup=u {b} ab b≤x is-sup with trio< b px
-... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫
+... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsMinSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫
-... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫
+... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫
 ... | tri> ¬a ¬b px<b = zc31 ? 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 ⟫ )
 zcsup : xSUP (UnionCF A f mf ay supf0 px) x
 zcsup with zc30
 ... | refl = record { ax = ab ; is-sup = record { x≤sup = λ {w} lt →
-IsSup.x≤sup (proj1 is-sup) ? ; minsup = ? } }
+IsMinSup.x≤sup (proj1 is-sup) ? ; minsup = ? } }
 zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A (UnionCF A f mf ay supf0 px) x f) → supf0 b ≡ b
 zc31 (case1 ¬sp=x) with zc30
 ... | refl = ⊥-elim (¬sp=x zcsup )
 zc31 (case2 hasPrev ) with zc30
 ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev
 sis {z} z≤x with trio< z x
 ... | tri< a ¬b ¬c = {!!} where
 zc8 = ZChain.supf-is-minsup (pzc z a) {!!}
 ... | tri≈ ¬a b ¬c = {!!}
 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x ))
-sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) b f ) → supf1 b ≡ b
+sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsMinSup A (UnionCF A f mf ay supf1 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) b f ) → supf1 b ≡ b
 sup=u {z} ab z≤x is-sup with trio< z x
 ... | tri< a ¬b ¬c = ? -- ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x≤sup = {!!} }
 ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?)  ?)  ab {!!} record { x≤sup = {!!} }
 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤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 x 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 )
+... | case2 ¬fy<x with ODC.p∨¬p O (IsMinSup A pchain ax )
 ... | case1 is-sup = ? -- record { supf = supf1  ; sup=u = {!!}
 -- ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!};  asupf = {!!}  } -- where -- x is a sup of (zc ?)
 ... | case2 ¬x=sup =  no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention
 ---
 sp : Ordinal
 sp = & (SUP.sup sp1)
 asp : odef A sp
 asp = SUP.as sp1
 z10 :  {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b )
-→  HasPrev A chain b f ∨  IsSup A chain {b} ab
+→  HasPrev A chain b f ∨  IsMinSup A (UnionCF A f mf ab (ZChain.supf zc) b) ab
 → * a < * b  → odef chain b
-z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
+z10 = ? -- ZChain1.is-max (SZ1 f mf as0 zc (& A) )
 z22 : sp o< & A
 z22 = z09 asp
 x≤sup : {x : HOD} → chain ∋ x → (x ≡ SUP.sup sp1 ) ∨ (x < SUP.sup sp1 )
 x≤sup bz = SUP.x≤sup sp1 bz
 z12 : odef chain sp
 (case2 z19 ) z13 where
 z13 :  * (& s) < * sp
 z13 with x≤sup ( ZChain.chain∋init zc )
 ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
 ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
-z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1)
+z19 : IsMinSup A (UnionCF A f mf as0 (ZChain.supf zc) sp) asp
-z19 = record {   x≤sup = z20 ; minsup = ? }  where
+z19 = record {   x≤sup = ? ; minsup = ? }  where
 z20 :  {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1))
 z20 {y} zy with x≤sup (subst (λ k → odef chain k ) (sym &iso) zy)
 ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
 ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
 ztotal : IsTotalOrderSet (ZChain.chain zc)
 sz<<c : {z : Ordinal } → z o< & A → supf z <= mc
 sz<<c z<A = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc)  ))
 sc=c : supf mc ≡ mc
 sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where
-is-sup :  IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1)
+is-sup :  IsMinSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1)
 is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy )
 ; minsup = ? }
 not-hasprev :  ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) mc (cf nmx)
 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where
 z30 : * mc < * (cf nmx mc)
 z32 : * (supf mc) < * (cf nmx (cf nmx y))
 z32 = ftrans<=-< z31 (subst (λ k → * mc < * k ) (cong (cf nmx) x=fy) z30 )
 z48 : ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
 z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A u<x (fsuc _ ( fsuc  _ fc )))
-is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd)
+is-sup : IsMinSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd)
 is-sup = record { x≤sup = z22 ; minsup = ? } where
 z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd)
 z23 lt = MinSUP.x≤sup spd lt
 z22 :  {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y →
 (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd)

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

comparison src/zorn.agda @ 957:ce42b1c5cf42