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

comparison src/zorn.agda @ 863:f5fc3f5f618f

u<=x to u<x

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Fri, 09 Sep 2022 20:20:39 +0900
parents	269467244745
children	06f692bf7a97

comparison

equal deleted inserted replaced

-:269467244745
+:f5fc3f5f618f
 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 : u o≤ 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
 -- data UChain is total
 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
 zc04 : odef (UnionCF A f mf ay supf (supf s))  (supf s)
 zc04 = csupf s≤<z
 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 (zc09 u≤x ) is-sup fc ⟫ where
+... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 u<x ) is-sup fc ⟫ where
 zc06 : supf u ≡ u
 zc06 = ChainP.supu=u is-sup
-zc09 : u o≤ supf s  →  u o≤ b
+zc09 : u o< supf s  →  u o< b
-zc09 u<s with osuc-≡< (subst (λ k → k o≤ supf s) (sym zc06) u<s)
+zc09 u<s = ordtrans (supf-inject (subst (λ k → k o< supf s) (sym zc06) u<s)) s<b
-... | case1 su=ss = zc08 where
-zc07 : supf u o≤ supf b
-zc07 = subst (λ k → k o≤ supf b) (sym su=ss) (supf-mono  (o<→≤ s<b)  )
-zc08 :  u o≤ b
-zc08 with osuc-≡< zc07
-... | case1 su=sb = ⊥-elim ( o<¬≡ (trans (sym su=ss) su=sb ) ss<sb )
-... | case2 lt =  o<→≤ (supf-inject lt )
-... | case2 lt =  o<→≤ (ordtrans (supf-inject lt) s<b)
 csupf-fc {b} {s} {z1} b<z ss≤sb (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 (csupf-fc b<z ss≤sb 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) ⟫
 {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 (osucc 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 )  (zc : ZChain A f mf as0 (& A) )
 (total : IsTotalOrderSet (ZChain.chain zc) )  → SUP A (ZChain.chain zc)
 sp0 f mf zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total
 zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P
 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) 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 (o<→≤ b<x) 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
 m04 : ¬ HasPrev A (UnionCF A f mf ay (ZChain.supf zc) 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 } )
 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 = chain-mono1 (osucc b<x)
-⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc )  m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+⟪ ab , ch-is-sup b <-osuc 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))
 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
 m07 {z} fc = ZChain.fcy<sup zc  m09 fc
 m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
 ... | 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  ⟫ )
 -- if previous chain satisfies maximality, we caan reuse it
 --
---  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x
+--    UninCF supf0 px  previous chain u o< px, supf0 px is not included
+--    UninCF supf0 x   supf0 px is included
+--           supf0 px ≡ px
+--           supf0 px ≡ supf0 x
 no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A pchain x f) → ZChain A f mf ay x
 no-extension P = record { supf = supf0 ;  sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono ; supf-max = supf-max
 ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) ; csupf = csupf }  where
-pchain0=1 : pchain ≡ pchain1
+zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
-pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 P } where
+zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
+zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup  fc  ⟫
-zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
+zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  (HasPrev A pchain x f )
-zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1≤x (osucc (pxo<x op))) u1-is-sup  fc  ⟫
+→ {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( supf0 px ≡ px )
-zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  (HasPrev A pchain x f )
+zc11 P {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
-→ {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
+zc11 P {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ with trio< u1 px
-zc11 P {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
+... | tri< u1<px ¬b ¬c = case1 ⟪ az , ch-is-sup u1 u1<px u1-is-sup fc  ⟫
-zc11 P {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ with osuc-≡< u1≤x
+... | tri≈ ¬a eq ¬c  = case2 (subst (λ k → supf0 k ≡ k) eq s1u=u) where
-... | case2 lt = ⟪ az , ch-is-sup u1 u1≤px u1-is-sup fc  ⟫ where
+s1u=u : supf0 u1 ≡ u1
-u1≤px : u1 o≤ px
+s1u=u = ChainP.supu=u u1-is-sup
-u1≤px = (subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) lt)
+zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = ⊥-elim (¬sp=x zcsup) where
-zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ | case1 eq = ⊥-elim (¬sp=x zcsup) where
+eq : u1 ≡ x
-s1u=x : supf0 u1 ≡ x
+eq with trio< u1 x
-s1u=x = trans (ChainP.supu=u u1-is-sup) eq
+... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ )
-zc13 : osuc px o< osuc u1
+... | tri≈ ¬a b ¬c = b
-zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq) )
+... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x c )
-x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
+s1u=x : supf0 u1 ≡ x
-x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x
+s1u=x = trans (ChainP.supu=u u1-is-sup) eq
+zc13 : osuc px o< osuc u1
+zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) )
+x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
+x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x
 ( ChainP.fcy<sup u1-is-sup {w} fc  )
-x<sup {w} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans u≤x zc13 ))
+x<sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) zc13 ))
-... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 u≤x ) where
+... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 (o<→≤ u<x) ) where
 zc14 : u ≡ osuc px
 zc14 = begin
 u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩
 supf0 u ≡⟨ eq1 ⟩
 supf0 u1 ≡⟨ s1u=x ⟩
 x ≡⟨ sym (Oprev.oprev=x op) ⟩
 osuc px ∎ where open ≡-Reasoning
 ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ( ChainP.order u1-is-sup lt fc )
 zc12 : supf0 x ≡ u1
-zc12 = subst  (λ k → supf0 k ≡ u1) eq  (ChainP.supu=u u1-is-sup)
+zc12 = subst  (λ k → supf0 k ≡ u1) eq (ChainP.supu=u u1-is-sup)
 zcsup : xSUP (UnionCF A f mf ay supf0 px) x
-zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl)
+zcsup = record { ax =  subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl)
 ; is-sup = record { x<sup = x<sup } }
-zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ | case1 eq = zc20 fc where
+zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 (zc20 fc ) where
+eq : u1 ≡ x
+eq = ?
 zc20 : {z : Ordinal} → FClosure A f (supf0 u1) z → OD.def (od pchain) z
 zc20 {z} (init asu su=z ) = zc13 where
 zc14 : x ≡ z
 zc14 = begin
 x ≡⟨ sym eq ⟩
 zc30 : z ≡ x
 zc30 with osuc-≡< z≤x
 ... | case1 eq = eq
 ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
 zc34 : {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
-zc34 {w} lt = SUP.x<sup zc32 (subst (λ k → odef k (& w)) (sym pchain0=1)
+zc34 {w} lt = SUP.x<sup zc32 ? where
-(subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt ))
+zc35 : odef (UnionCF A f mf ay supf0 x) (& w)
+zc35 = subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt
 zc33 : supf0 z ≡ & (SUP.sup zc32)
 zc33 = trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl  )
 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
 sup=u {b} ab b≤x is-sup with trio< b px
 ... | 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) (subst (λ k → odef k w) pchain0=1 lt)  } }
+IsSup.x<sup (proj1 is-sup) (zc10 lt)} }
 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 (subst (λ k → HasPrev A k x f) pchain0=1 hasPrev ) )
+... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev
+; ay = zc10 (HasPrev.ay hasPrev) ; x=fy = HasPrev.x=fy hasPrev } )
 csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf0 (supf0 b)) (supf0 b)
 csupf {b} b≤x with zc04 b≤x
 ... | case2 b=x = subst (λ k → odef (UnionCF A f mf ay supf0 k) k) (ZChain.supf-max zc zc05 ) ( ZChain.csupf zc o≤-refl ) where
 zc05 : px o≤ b
 zc05 = subst (λ k → px o≤ k) (sym b=x) (o<→≤ (pxo<x op) )
 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫
 zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u u≤x ? (init ? ? ) ⟫
 zc11 :  {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
 zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where
+zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc13 fc where
 zc13 : {z : Ordinal} →  FClosure A f (supf1 u) z → odef pchain z
 zc13 (fsuc x fc) with zc13 fc
 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫
+... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫
 zc13 (init asu su=z ) with trio< u x
-... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u u≤x ? (init ? ? ) ⟫
+... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u u<x ? (init ? ? ) ⟫
 ... | tri≈ ¬a b ¬c = ?
-... | tri> ¬a ¬b c = ⊥-elim ( o≤> u≤x c )
+... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u<x c )
 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 (osuc z) {!!}) {!!} )
 ... | tri≈ ¬a b ¬c = {!!}
 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x ))

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

comparison src/zorn.agda @ 863:f5fc3f5f618f