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

comparison src/zorn.agda @ 976:8fe873f0c88e

is-max condition have to be b o< x

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Tue, 08 Nov 2022 18:29:35 +0900
parents	1e88cce74699
children	f0d2666fe3b2

comparison

equal deleted inserted replaced

-:1e88cce74699
+:8fe873f0c88e
 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
 ... | 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
 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 ⟫
 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) →
+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 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 )
 ... | 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
+... | case2 y<b = ⟪ ab , ch-is-sup b ? 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
+b<x  = ZChain.supf-inject zc ?
 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
 → 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 ) z22 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 a)} {* a}
 (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.asm  asup ))))
 (subst (λ k → odef A k) (sym &iso) (MinSUP.asm asup) )
-(case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc asup sa<sa ))) -- x ≡ f x ̄
+(case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc asup ))) -- x ≡ f x ̄
 (proj1 (cf-is-<-monotonic nmx a (MinSUP.asm asup ))) where                 -- x < f x
 supf = ZChain.supf zc
 asup : MinSUP A (ZChain.chain zc)
 asup = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
 a : Ordinal
 a = MinSUP.sup asup
 a<A : a o< & A
 a<A =  ∈∧P→o< ⟪ MinSUP.asm asup , lift true ⟫
-csup : MinSUP  A (UnionCF A (cf nmx)  (cf-is-≤-monotonic nmx) as0 supf a)
-csup = ZChain.minsup zc (o<→≤ a<A)
-c : Ordinal
-c = MinSUP.sup csup
-ac : odef A c
-ac = ?
-sfc=c : supf a ≡ c
-sfc=c = ZChain.supf-is-minsup zc (o<→≤ a<A)
-c<A : c o< & A
-c<A =  ∈∧P→o< ⟪ MinSUP.asm csup , lift true ⟫
-dsup : MinSUP  A (UnionCF A (cf nmx)  (cf-is-≤-monotonic nmx) as0 supf c)
-dsup = ZChain.minsup zc (o<→≤ c<A)
-d : Ordinal
-d = MinSUP.sup dsup
-ad : odef A d
-ad = ?
-sfc=d : supf c ≡ d
-sfc=d = ZChain.supf-is-minsup zc (o<→≤ c<A)
-d<A : d o< & A
-d<A =  ∈∧P→o< ⟪ MinSUP.asm dsup , lift true ⟫
-zc40 : uchain (cf nmx)  (cf-is-≤-monotonic nmx) ac  ⊆' UnionCF A (cf nmx)  (cf-is-≤-monotonic nmx) as0 supf d
-zc40 = ?
-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 = z25 where
-d1 :  Ordinal
-d1 = MinSUP.sup spd -- supf d1 ≡ d
-z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 )
-z24 = MinSUP.x≤sup spd (init asc refl)
---
---   f ( f .. ( supf mc ) <= d1
---   f d1 <= d1
---
-z25 : supf mc << d1
-z25 with z24
-... | case2 lt = lt
-... | case1 eq = ⊥-elim ( <-irr z29 (proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) ) )  where
---  supf mc ≡ d1
-z32 : ((cf nmx (supf mc)) ≡ d1) ∨ ( (cf nmx (supf mc)) << d1 )
-z32 = MinSUP.x≤sup spd (fsuc _ (init asc refl))
-z29 :  (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
-z29  with z32
-... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1)  )
-... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt)
---   supf a ≡  c o< d ≡ supf c o≤ supf (& A)
-sa<sa : supf a o< supf (& A)
-sa<sa = ?
 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 @ 976:8fe873f0c88e