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

comparison src/zorn.agda @ 1059:bd2a258f309c

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 10 Dec 2022 17:41:17 +0900
parents	12ce8d0224d2
children	a09f5e728f92

comparison

equal deleted inserted replaced

-:12ce8d0224d2
+:bd2a258f309c
 order : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b
 asupf :  {x : Ordinal } → odef A (supf x)
 supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
+zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x
 is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x)
-sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
-→ IsSUP A (UnionCF A f ay supf b) b → supf b ≡ b
 chain : HOD
 chain = UnionCF A f ay supf z
 chain⊆A : chain ⊆' A
 chain⊆A = λ lt → proj1 lt
 ft00 :   Tri ( a <  b) ( a ≡  b) ( b <  a )
 ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca))
 f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ =
 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso  (fcn-cmp y f mf fca fcb )
-supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
-supf-idem {b} b≤z sfb≤x = z52 where
-z54 :  {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
-z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
-z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z (subst (λ k → k o< supf b) (sym su=u) u<x)  fc where
-u<b : u o< b
-u<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
-z52 : supf (supf b) ≡ supf b
-z52 = sup=u asupf sfb≤x  record { ax = asupf  ; x≤sup = z54  }
-x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x
-x≤supfx {x} x≤z sx≤z with x<y∨y≤x (supf x) x
-... | case2 le = le
-... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf x) asupf ))) where
-z46 : odef (UnionCF A f ay supf x) (f (supf x))
-z46 = ⟪ proj2 ( mf (supf x) asupf ) , ch-is-sup (supf x) spx<px z47 (fsuc _ (init asupf  z47 )) ⟫ where
-z47 : supf (supf x) ≡ supf x
-z47 = supf-idem x≤z  sx≤z
-z45 : f (supf x) ≤ supf x
-z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46
-sup=u0 : {b : Ordinal} → (ab : odef A b) → b o≤ z
-→ IsSUP A (UnionCF A f ay supf b) b  → supf b ≡ b
-sup=u0 {b} ab b≤z is-sup with trio< (supf b) b
-... | tri< sb<b ¬b ¬c = ⊥-elim ( o≤> z47 sb<b ) where
-z47 : b o≤ supf b
-z47 = x≤supfx b≤z ?
-... | tri≈ ¬a b ¬c = b
-... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb ) where
-z48 : supf b o≤ b
-z48 = IsMinSUP.minsup (is-minsup b≤z) ab (λ ux → IsSUP.x≤sup is-sup ux )
 supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b
 supf-mono< {a} {b} b≤z sa<sb  with order {a} {b} b≤z sa<sb (init asupf refl)
 ... | case2 lt = lt
 ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb )
 u<a = supf-inject ( osucprev (begin
 osuc (supf u)  ≡⟨ cong osuc su=u ⟩
 osuc u  ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩
 z  ≤⟨ z≤sa ⟩
 supf a ∎ )) where open o≤-Reasoning O
+sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
+→ IsSUP A (UnionCF A f ay supf b) b  → supf b ≡ b
+sup=u {b} ab b≤z is-sup = z50 where
+z48 : supf b o≤ b
+z48 = IsMinSUP.minsup (is-minsup b≤z) ab (λ ux → IsSUP.x≤sup is-sup ux )
+z50 : supf b ≡ b
+z50 with trio< (supf b) b
+... | tri< sb<b ¬b ¬c = ⊥-elim ( o≤> z47 sb<b ) where
+z47 : b o≤ supf b
+z47 = zo≤sz b≤z
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb )
+supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
+supf-idem {b} b≤z sfb≤x = z52 where
+z54 :  {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
+z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
+z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z (subst (λ k → k o< supf b) (sym su=u) u<x)  fc where
+u<b : u o< b
+u<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
+z52 : supf (supf b) ≡ supf b
+z52 = sup=u asupf sfb≤x  record { ax = asupf  ; x≤sup = z54  }
+x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x
+x≤supfx {x} x≤z sx≤z with x<y∨y≤x (supf x) x
+... | case2 le = le
+... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf x) asupf ))) where
+z46 : odef (UnionCF A f ay supf x) (f (supf x))
+z46 = ⟪ proj2 ( mf (supf x) asupf ) , ch-is-sup (supf x) spx<px z47 (fsuc _ (init asupf  z47 )) ⟫ where
+z47 : supf (supf x) ≡ supf x
+z47 = supf-idem x≤z  sx≤z
+z45 : f (supf x) ≤ supf x
+z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46
 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
 m13 spx<x = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1)  m14 where
 m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1)
 m14 {z} uz = MinSUP.x≤sup sup1 (case1 uz)
 zc41 : ZChain A f mf< ay x
-zc41 =  record { supf = supf1 ; sup=u = sup=u ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order
+zc41 =  record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order
-; supfmax = supfmax ; is-minsup = is-minsup ;  cfcs = cfcs  }  where
+; zo≤sz = zo≤sz ; supfmax = supfmax ; is-minsup = is-minsup ;  cfcs = cfcs  }  where
 supf1 : Ordinal → Ordinal
 supf1 z with trio< z px
 ... | tri< a ¬b ¬c = supf0 z
 ... | tri≈ ¬a b ¬c = supf0 z
 z25 {w} ⟪ ua , ch-is-sup u u<x su=u fc  ⟫ = sup ⟪ ua , ch-is-sup u u<x
 (trans (sf1=sf0 u≤px)  su=u)  (fcpu fc u≤px)  ⟫ where
 u≤px : u o≤ px
 u≤px = ordtrans u<x z≤px
-sup=u : {b : Ordinal} (ab : odef A b) →
-b o≤ x → IsSUP A (UnionCF A f ay supf1 b) b  → supf1 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)  zc40 where
-zc42 : {w : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) b) w → w ≤ b
-zc42 {w} ⟪ ua , ch-init fc ⟫ = IsSUP.x≤sup is-sup  ⟪ ua , ch-init fc ⟫
-zc42 {w} ⟪ ua ,  ch-is-sup u u<x su=u fc  ⟫ = IsSUP.x≤sup is-sup ⟪ ua ,
-ch-is-sup u u<x (trans (sf1=sf0 zc44) su=u) (fcpu fc zc44)  ⟫ where
-zc44 : u o≤ px
-zc44 = ordtrans u<x (o<→≤ a)
-zc40 : IsSUP A (UnionCF A f ay supf0 b) b
-zc40 = record { ax = ab ; x≤sup = zc42 }
-... | tri≈ ¬a b=px ¬c = ZChain.sup=u zc ab (o≤-refl0 b=px)  record { ax = ab ; x≤sup = zc42 } where
-zc42 : {w : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) b) w → w ≤ b
-zc42 {w} ⟪ ua , ch-init fc ⟫ = IsSUP.x≤sup is-sup  ⟪ ua , ch-init fc ⟫
-zc42 {w} ⟪ ua ,  ch-is-sup u u<x su=u fc  ⟫ = IsSUP.x≤sup is-sup ⟪ ua ,
-ch-is-sup u u<x (trans (sf1=sf0 zc44) su=u) (fcpu fc zc44)  ⟫ where
-zc44 : u o≤ px
-zc44 = o<→≤ ( subst (λ k → u o< k ) b=px u<x )
-... | tri> ¬a ¬b px<b = trans zc36 x=b where
-x=b : x ≡ b
-x=b 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 ⟫ )
-zc31 : sp1 o≤ b
-zc31 = MinSUP.minsup sup1 ab zc32 where
-zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b)
-zc32 {w} (case1 ⟪ ua , ch-init fc ⟫ ) = IsSUP.x≤sup is-sup ⟪ ua , ch-init fc ⟫
-zc32 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc ⟫ ) = IsSUP.x≤sup is-sup ⟪ ua , ch-is-sup u z01 z02 z03 ⟫ where
-z01 : u o< b
-z01 = ordtrans u<x (subst (λ k → px o< k ) x=b px<x )
-z02 : supf1 u ≡ u
-z02 = trans (sf1=sf0 (o<→≤ u<x)) su=u
-z03 : FClosure A f (supf1 u) w
-z03 = fcpu fc (o<→≤ u<x)
-zc32 {w} (case2 fc) = IsSUP.x≤sup is-sup ⟪ A∋fc _ f mf (proj1 fc) , ch-is-sup (supf0 px) sa<x su=u fc1 ⟫ where
-su=u : supf1 (supf0 px) ≡ supf0 px
-su=u = trans (sf1=sf0 (zc-b<x _ (proj2 fc))) ( ZChain.supf-idem zc o≤-refl (zc-b<x _ (proj2 fc)) )
-fc1 : FClosure A f (supf1 (supf0 px)) w
-fc1 = subst (λ k → FClosure A f k w ) (sym su=u) (proj1 fc)
-sa<x : supf0 px o< b
-sa<x = subst (λ k → supf0 px o< k ) x=b ( proj2 fc)
-zc36 : sp1 ≡ x
-zc36 with osuc-≡< zc31
-... | case1 eq = trans eq (sym x=b)
-... | case2 sp1<b = ⊥-elim ( <<-irr zc40 (proj1 ( mf< (supf0 px) (ZChain.asupf zc))) ) where
---   sp1 o< x → ⊥
---   supf0 px o≤ sp1 o< x → supf0 px o≤ px
---        px o≤ supf0 px → px ≡ spuf0 px o≤ spuf1 x o< x
---        px ≡ supf1 x
-sp1<x : sp1 o<  x
-sp1<x = subst (λ k → sp1 o< k ) (sym x=b) sp1<b
-zc38 : supf0 px o≤ px
-zc38 = begin
-supf0 px  ≡⟨ sym (sf1=sf0 o≤-refl)  ⟩
-supf1 px  ≤⟨ supf1-mono (o<→≤ px<x) ⟩
-supf1 x  ≡⟨ sf1=sp1 px<x ⟩
-sp1 ≤⟨ zc-b<x _ sp1<x ⟩
-px ∎ where open o≤-Reasoning O
-zc37 : supf0 px ≡ px
-zc37 with trio< (supf0 px) px
-... | tri< a ¬b ¬c = ⊥-elim ( o≤> (ZChain.x≤supfx zc o≤-refl zc38) a )
-... | tri≈ ¬a b ¬c = b
-... | tri> ¬a ¬b c = ⊥-elim ( o≤> zc38 c )
-zc44 : sp1 o≤ supf0 px
-zc44 = begin
-sp1 ≤⟨ zc-b<x _ sp1<x ⟩
-px ≡⟨ sym zc37 ⟩
-supf0 px ∎ where open o≤-Reasoning O
-zc45 : supf0 px o≤ sp1
-zc45 = begin
-supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩
-supf1 px ≤⟨ supf1-mono (o<→≤ px<x) ⟩
-supf1 x ≡⟨ sf1=sp1 px<x  ⟩
-sp1 ∎ where open o≤-Reasoning O
-zc39 : supf0 px ≡ sp1
-zc39 with trio< (supf0 px) sp1
-... | tri< a ¬b ¬c = ⊥-elim ( o≤> zc44 a ) ---   sp1 o< x ≡ osuc px ≡ osuc (supf0 px)
-... | tri≈ ¬a b ¬c = b
-... | tri> ¬a ¬b c = ⊥-elim ( o≤> zc45 c ) ---   supf0 px o≤ supf1 x ≡ sp1
-zc40 : f (supf0 px) ≤ supf0 px
-zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39)
-( MinSUP.x≤sup sup1 (case2 ⟪ fsuc _ (init (ZChain.asupf zc) refl) , subst (λ k → k o< x) (sym zc37) px<x ⟫  ))
 supfeq1 : {a b : Ordinal } → a o≤ x →  b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b
 supfeq1 {a} {b} a≤z b≤z ua=ub with trio< (supf1 a) (supf1 b)
 ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
 IsMinSUP.minsup (is-minsup b≤z) asupf1 (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb )
 ... | tri≈ ¬a b ¬c = b
 u<a = supf-inject0 supf1-mono ( osucprev (begin
 osuc (supf1 u)  ≡⟨ cong osuc su=u ⟩
 osuc u  ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩
 x  ≤⟨ z≤sa ⟩
 supf1 a ∎ )) where open o≤-Reasoning O
+zo≤sz : {z : Ordinal} →  z o≤ x → z o≤ supf1 z
+zo≤sz {z} z≤x with osuc-≡< z≤x
+... | case2 z<x = subst (λ k → z o≤ k) (sym (sf1=sf0 (zc-b<x _ z<x ))) (ZChain.zo≤sz zc (zc-b<x _ z<x ))
+... | case1 refl with osuc-≡< (supf1-mono (o<→≤ (px<x))) --   px o≤ supf1 px o≤ supf1 x ≡ sp1 → x o≤ sp1
+... | case2 lt = begin
+x ≡⟨ sym (Oprev.oprev=x op) ⟩
+osuc px ≤⟨ osucc (ZChain.zo≤sz zc o≤-refl)  ⟩
+osuc (supf0 px) ≡⟨ sym (cong osuc (sf1=sf0 o≤-refl )) ⟩
+osuc (supf1 px) ≤⟨ osucc lt ⟩
+supf1 x ∎ where open o≤-Reasoning O
+... | case1 spx=sx with osuc-≡< ( ZChain.zo≤sz zc o≤-refl )
+... | case2 lt = begin
+x ≡⟨ sym (Oprev.oprev=x op) ⟩
+osuc px ≤⟨ osucc lt ⟩
+supf0 px ≡⟨ sym (sf1=sf0 o≤-refl)  ⟩
+supf1 px ≤⟨ supf1-mono (o<→≤ px<x)  ⟩
+supf1 x ∎ where open o≤-Reasoning O
+... | case1 px=spx =  ⊥-elim ( <<-irr zc40 (proj1 ( mf< (supf0 px) (ZChain.asupf zc))) ) where
+zc37 : supf0 px ≡ px
+zc37 = sym px=spx
+zc39 : supf0 px ≡ sp1
+zc39 = begin
+supf0 px ≡⟨ sym (sf1=sf0 o≤-refl)  ⟩
+supf1 px ≡⟨ spx=sx ⟩
+supf1 x ≡⟨ sf1=sp1 px<x ⟩
+sp1 ∎ where open ≡-Reasoning
+zc40 :  f (supf0 px) ≤ supf0 px
+zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39)
+( MinSUP.x≤sup sup1 (case2 ⟪ fsuc _ (init (ZChain.asupf zc) refl) , subst (λ k → k o< x) (sym zc37) px<x ⟫  ))
 order : {a b : Ordinal} {w : Ordinal} →
 b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
 order {a} {b} {w} b≤x sa<sb fc = z20 where
 a<b : a o< b
 z27 = trans ( supfeq1 a≤x b≤x ( union-max1 (subst (λ k → k o≤ supf1 a) b=x b≤sa)
 b≤x (subst (λ k → supf1 a o< k ) (sym sf1b=sp1)  sa<sb )  ) ) sf1b=sp1
 ... | no lim with trio< x o∅
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
-... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; sup=u = ? ; asupf = MinSUP.as (ysup f mf ay)
+... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay)
 ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s )
-; supfmax = λ _ → refl ; is-minsup = ? ; cfcs = ?    } where
+; zo≤sz = ? ; supfmax = λ _ → refl ; is-minsup = ? ; cfcs = ?    } where
 mf : ≤-monotonic-f A f
 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
 mf00 : * x < * (f x)
 mf00 = proj1 ( mf< x ax )
-... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ?
+... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = ? ; supf-mono = supf-mono ; order = ?
-; supfmax = ? ; is-minsup = ? ; cfcs = cfcs    }  where
+; zo≤sz = λ _ → ?   ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs    }  where
 -- mf : ≤-monotonic-f A f
 -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫  will result memory exhaust
 mf : ≤-monotonic-f A f
 zc40 : odef (UnionCF A f ay supf1 b) w
 zc40 with zcb
 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
 ... | ⟪ az , ch-is-sup u u<x su=u fc ⟫ = ⟪ az , ch-is-sup u ? ? ?  ⟫
-sup=u : {b : Ordinal} (ab : odef A b) →
-b o≤ x → IsMinSUP A (UnionCF A f ay supf1 b) b  → supf1 b ≡ b
-sup=u {b} ab b≤x is-sup with osuc-≡< b≤x
-... | case1 b=x = ? where
-zc31 : spu o≤ b
-zc31 = MinSUP.minsup usup ab zc32 where
-zc32 : {w : Ordinal } → odef pchainx w → (w ≡ b) ∨ (w << b)
-zc32 = ?
-... | case2 b<x = trans (sf1=sf ?) (ZChain.sup=u (pzc (ob<x lim b<x)) ab ? ? )
 ---
 --- the maximum chain  has fix point of any ≤-monotonic function
 ---
 SZ : ( f : Ordinal → Ordinal ) → (mf< : <-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf< ay x

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

comparison src/zorn.agda @ 1059:bd2a258f309c