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

comparison src/zorn.agda @ 900:ac4daa43ef2a

roll back to u<x

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Fri, 07 Oct 2022 17:13:41 +0900
parents	37a09244cebd
children	6146d75131f5

comparison

equal deleted inserted replaced

-:37a09244cebd
+:ac4daa43ef2a
 supu=u   : supf u ≡ u
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
 (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where
 ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z
-ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u≤x : supf u o≤ supf x) ( is-sup : ChainP A f mf ay supf u )
+ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u≤x : u o< x) ( is-sup : ChainP A f mf ay supf u )
 ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 --
 --         f (f ( ... (sup y))) f (f ( ... (sup z1)))
 --        /          |         /             |
 cf-is-<-monotonic nmx x ax = ⟪ proj2 (is-cf nmx ax ) , proj1 (is-cf nmx ax ) ⟫
 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
 cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
 chain-mono :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
-{a b c : Ordinal} → supf a o≤ supf b
+{a b c : Ordinal} → a o≤ b
 → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c
 chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ =
 ⟪ ua , ch-init fc  ⟫
 chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ uaa ,  ch-is-sup ua ua<x is-sup fc  ⟫ =
-⟪ uaa , ch-is-sup ua (OrdTrans ua<x a≤b ) is-sup fc  ⟫
+⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b ) is-sup fc  ⟫
 sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
 (zc : ZChain A f mf ay x ) → SUP A (ZChain.chain zc)
 sp0 f mf ay zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ztotal where
 ztotal : IsTotalOrderSet (ZChain.chain zc)
 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
 uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb))
 --
 -- Second TransFinite Pass for maximality
 --
 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 = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
-chain-mono1 :  {a b c : Ordinal} → (ZChain.supf zc a) o≤ (ZChain.supf zc b)
+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) a≤b
 is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
 b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f →
 zc04 : odef (UnionCF A f mf ay supf (& A))  (supf s)
 zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc))
 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
 zc05 with zc04
 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫
-... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (o<→≤ zc08) is-sup fc ⟫ where
+... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ZChain.supf-inject zc zc08) is-sup fc ⟫ where
 zc07 : FClosure A f (supf u) (supf s)   -- supf u ≤ supf s  → supf u o≤ supf s
 zc07 = fc
 zc06 : supf u ≡ u
 zc06 = ChainP.supu=u is-sup
 zc08 : supf u o< 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) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
-zc1 x prev with Oprev-p x
+zc1 x prev with Oprev-p x  -- prev is not used now....
 ... | yes op = record { is-max = is-max } where
 px = Oprev.oprev op
 zc-b<x : {b : Ordinal } → b o< x → b o< osuc px
 zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt
 is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
 HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) 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 b<x ab has-prev a<b
 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 b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
 b<A : b o< & A
 b<A = z09 ab
 sb≤sx : supf b o≤ supf x
 sb≤sx = ZChain.supf-mono zc (o<→≤ b<x )
+sb<sx : supf b o< supf x
+sb<sx with osuc-≡< sb≤sx
+... | case2 lt = lt
+... | case1 sb=sx = ? where
+-- b ≡ x
+-- b o< px → a < * b → odef (UnionCF A f mf ay supf px) b
 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 sb≤sx  (HasPrev.ay  nhp)
+chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy 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 sb≤sx uz) }  , m04 ⟫
+⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) 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
 * 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 b<x 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
+... | case2 y<b = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
 sb≤sx : supf b o≤ supf x
 sb≤sx = ZChain.supf-mono zc (o<→≤ b<x )
+sb<sx : supf b o< supf x
+sb<sx = ?
 m09 : b o< & A
 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
 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) b f
 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
-chain-mono1 sb≤sx (HasPrev.ay  nhp)
+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 sb≤sx lt )} , m04 ⟫    -- ZChain on x
+⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) lt )} , m04 ⟫    -- ZChain on x
 m06 : ChainP A f mf ay supf b
 m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 ---
 --- the maximum chain  has fix point of any ≤-monotonic function
 ... | tri> ¬a ¬b px<b with osuc-≡< b≤x
 ... | case1 eq = case2 eq
 ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ )
 zc4 : ZChain A f mf ay x     --- supf px ≤ supf x
-zc4 with osuc-≡< ?
+zc4 with trio< x (supf0 px)
-... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1
+... | tri> ¬a ¬b c =  record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where
+... | tri≈ ¬a b ¬c =  ? where
+-- ... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1
+--    ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where
 --  we are going to determine (supf x), which is not specified in previous zc
 --  case1 : supf px ≡ px
 --     supf px is MinSUP of previous chain , supf x ≡ MinSUP of Union of UChain and  FClosure px
+sfpx=px = ?
 pchainpx : HOD
 pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z  } ; odmax = & A ; <odmax = zc00 } where
 zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → z o< & A
 zc00 {z} (case1 lt) = z07 lt
 supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
 ... | tri< a ¬b ¬c = zc19 where
 zc21 : MinSUP A (UnionCF A f mf ay supf0 z)
 zc21 = ZChain.minsup zc (o<→≤ a)
 zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
-zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc (o<→≤ a))  ux))
+zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o<→≤ a) ux))
 zc19 : supf0 z o≤ sp1
 zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a))) ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
 ... | tri≈ ¬a b ¬c = zc18 where
 zc21 : MinSUP A (UnionCF A f mf ay supf0 z)
 zc21 = ZChain.minsup zc (o≤-refl0 b)
 MinSUP.sup zc21 ≡⟨ sym (ZChain.supf-is-minsup zc (o≤-refl0 b)) ⟩
 supf0 z ≡⟨ cong supf0 b ⟩
 supf0 px ≡⟨ sym sfpx=px ⟩
 px ∎ where open ≡-Reasoning
 zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
-zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc (o≤-refl0 b)) ux))
+zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 ? ux))
 zc18 : px o≤ sp1 -- supf0 z ≡ px
 zc18 = subst (λ k → k o≤ sp1) zc20 ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
 ... | tri> ¬a ¬b c = o≤-refl
 supf-<1 : {z0 z1 : Ordinal} → supf1 z0 o< supf1 z1 → supf1 z0 << supf1 z1
 zc21 =  ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) sfpx=px c  )
 zc22 : z1 o< x -- c : px o< supf0 z1
 zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? )
 -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x
-... | case2 px<spfx = ? where
+... | tri< a ¬b ¬c = ? where
 --  case2 : px o< supf px
 --     supf px is not MinSUP of previous chain , supf x ≡ supf px
 -- record { supf = supf0 ;  asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono

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

comparison src/zorn.agda @ 900:ac4daa43ef2a