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

comparison src/zorn.agda @ 988:9a85233384f7

is-max and supf b = supf x

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 14 Nov 2022 07:35:18 +0900
parents	c8c60a05b39b
children	ce713b5db3f3

comparison

equal deleted inserted replaced

-:c8c60a05b39b
+:9a85233384f7
 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)
+is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< z  → (ab : odef A b)
 → HasPrev A (UnionCF A f mf ay supf z) f b ∨  IsSUP 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
 --     supf is fixed for z ≡ & A , we can prove order and is-max
 --
 SZ1 : ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal)   → ZChain1 A f mf ay zc x
-SZ1 f mf {y} ay zc x = zc1 x where
+SZ1 f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
 chain-mono1 :  {a b c : Ordinal} → a o≤ b
 → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
 chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b
 is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → (ab : odef A b)
 → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) f b
 zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
 zc04 with zc00
 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z))  ) eq )
 ... | case2 lt = case2 (subst₂ (λ j k → j < * k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) )) lt )
-zc1 :  (x : Ordinal) → ZChain1 A f mf ay zc x
+zc1 :   (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain1 A f mf ay zc y) → ZChain1 A f mf ay zc x
-zc1 x with Oprev-p x  -- prev is not used now....
+zc1 x prev with Oprev-p x
 ... | yes op = record { is-max = is-max ; order = order  } 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) →
+b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP 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
+is-max {a} {b} ua b<x 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
+= ⟪ ab , ch-is-sup b sb<sx  m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
 b<A : b o< & A
 b<A = z09 ab
-b<x : b o< x
+sb<sx : supf b o< supf x
-b<x  = ZChain.supf-inject zc sb<sx
+sb<sx  = ?
 m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
 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) uz  }  , m04 ⟫
 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 →
+b o< x → (ab : odef A b) →
+HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP 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 b<x ab P a<b | case2 is-sup with IsSUP.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))
+sb<sx : supf b o< supf x
+sb<sx  = ?
+m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
+m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
+m08 : {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
+m08 {s} {z1} s<b fc = order m09 s<b fc
-m06 : ChainP A f mf ay supf b
+m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
-m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
+m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
-... | no lim = record { is-max = is-max ; order = order }  where
+chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp)
-is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
+; x=fy = HasPrev.x=fy nhp } )
-ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
+m05 : ZChain.supf zc b ≡ b
-HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
+m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
-* a < * b → odef (UnionCF A f mf ay supf x) b
+m06 : ChainP A f mf ay supf b
-is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P
+m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
-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 )
-... | 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
-b<x  = ZChain.supf-inject zc sb<sx
-m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
-m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
-m08 : {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
-m08 {s} {z1} s<b fc = order m09 s<b fc
-m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
-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) lt } , 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
 uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax =
 λ {z} cz → subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (A∋fc y f mf cz ))) }
 → MinSUP A (UnionCF A f mf ay (ZChain.supf zc) x)
 msp0 f mf {x} ay zc = minsupP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) (ZChain.f-total zc)
 fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
 → (sp1 : MinSUP A (ZChain.chain zc))
-→ (ssp<as :  ZChain.supf zc (MinSUP.sup sp1) o< ZChain.supf zc (& A))
 → f (MinSUP.sup sp1)  ≡ MinSUP.sup sp1
-fixpoint f mf zc sp1 ssp<as = z14 where
+fixpoint f mf zc sp1 = z14 where
 chain = ZChain.chain zc
 supf = ZChain.supf zc
 sp : Ordinal
 sp = MinSUP.sup sp1
 asp : odef A sp
 asp = MinSUP.asm sp1
-z10 :  {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b )
+z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< (& A) → (ab : odef A b )
 →  HasPrev A chain f b  ∨  IsSUP A (UnionCF A f mf as0 (ZChain.supf zc) b) ab
 → * a < * b  → odef chain b
 z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
 z22 : sp o< & A
 z22 = z09 asp
 z12 : odef chain sp
 z12 with o≡? (& s) sp
 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp (case2 z19 ) z13 where
+... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) (z09 asp) asp (case2 z19 ) z13 where
 z13 :  * (& s) < * sp
 z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
 ... | case1 eq = ⊥-elim ( ne eq )
 ... | case2 lt = lt
 z19 : IsSUP A (UnionCF A f mf as0 (ZChain.supf zc) sp) asp
 z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥
 z04 nmx zc = <-irr0  {* (cf nmx c)} {* c}
 (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.asm  msp1 ))))
 (subst (λ k → odef A k) (sym &iso) (MinSUP.asm msp1) )
-(case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc msp1  ss<sa ))) -- x ≡ f x ̄
+(case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc msp1  ))) -- x ≡ f x ̄
 (proj1 (cf-is-<-monotonic nmx c (MinSUP.asm msp1 ))) where          -- x < f x
 supf = ZChain.supf zc
 msp1 : MinSUP A (ZChain.chain zc)
 msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
 c : Ordinal
 c = MinSUP.sup msp1
-c<A : c o< & A
-c<A =  ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫
-asc : odef A (supf c)
-asc = ZChain.asupf zc
-spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )
-spd = ysup (cf nmx)  (cf-is-≤-monotonic nmx) asc
-d = MinSUP.sup spd
-d<A : d o< & A
-d<A =  ∈∧P→o< ⟪ MinSUP.asm spd , lift true ⟫
-msup : MinSUP  A (UnionCF A (cf nmx)  (cf-is-≤-monotonic nmx) as0 supf d)
-msup = ZChain.minsup zc (o<→≤ d<A)
-sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) )
-sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A)
-sc<<d : {mc : Ordinal } → (asc : odef A (supf mc)) → (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc ))
-→ supf mc << MinSUP.sup spd
-sc<<d {mc} asc spd with MinSUP.x≤sup spd (init asc refl)
-... | case1 eq = ?
-... | case2 lt = ?
-ss<sa : supf c o< supf (& A)
-ss<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ c<A))
-... | case2 sc<sa = sc<sa
-... | case1 sc=sa = ⊥-elim (  nmx record { maximal = * d ; as = subst (λ k → odef A k) (sym &iso) (MinSUP.asm spd)
-; ¬maximal<x = λ {x} ax → subst₂ (λ j k → ¬ ( j < k)) refl *iso (zc10 sc=sa ax) } ) where
-zc10 : supf c ≡ supf (& A) → {x : Ordinal } → odef A x  → ¬ ( d << x )
-zc10 = ? where
-zc11 : {z : Ordinal } →  odef (ZChain.chain zc) z → supf z o< supf (& A)
-zc11 = ?
-sc≤c : c o≤ supf c
-sc≤c = MinSUP.minsup msp1 ? ?
-sc=c : supf c ≡ c
-sc=c = ?
-d≤c : c o≤ d
-d≤c = MinSUP.minsup msp1 ? ?
---    supf x o≤ supf c → supf x ≡ supf c ∨ supf x o< supf c
---      c << x → x is sup of chain or x = f ( .. ( f c ))
---      c o≤ x (by minimulity)
---  odef chain z → supf z o< supf (& A) ≡ supf c → supf c is sup of chain, by minimulity  c o≤ supf c
---   supf c o≤ supf (supf c) o≤ supf x o≤ supf (& A)
---   supf c ≡ supf (supf c) ≡ supf x  ≡ supf (& A)  means supf of FClosure of (supf c) is Maximal
 zorn00 : Maximal A
 zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM
 ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x  = zorn02 } where
 -- yes we have the maximal

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

comparison src/zorn.agda @ 988:9a85233384f7