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

comparison src/zorn.agda @ 661:9142e834c4c6

fix

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sun, 03 Jul 2022 06:10:51 +0900
parents	db9477c80dce
children	a45ec34b9fa7

comparison

equal deleted inserted replaced

-:db9477c80dce
+:9142e834c4c6
 field
 sup : HOD
 A∋maximal : A ∋ sup
 x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
-record UChain (chain : Ordinal → HOD) (x : Ordinal) (z : Ordinal) : Set n where
+record UChain (x : Ordinal) (chain : (z : Ordinal ) → z o< x → HOD)  (z : Ordinal) : Set n where
 -- Union of supf z which o< x
 field
 u : Ordinal
 u<x : u o< x
-chain∋z : odef (chain u) z
+chain∋z : odef (chain u u<x) z
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal} (ay : odef A y) : Ordinal →  HOD  → Set (Level.suc n) where
 ( c : Chain A f ay (Oprev.oprev op) chain) ( nh :  ¬ HasPrev A chain  ax f ) ( sup : IsSup A chain   ax ) → Chain A f ay x
 record { od = record { def = λ x → odef A x ∧ (odef chain x ∨ (FClosure A f y x)) } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 ch-skip : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x )
 ( c : Chain A f ay (Oprev.oprev op) chain) ( nh : ¬  HasPrev A chain ax f ) ( nsup : ¬ IsSup A chain ax ) → Chain A f ay x chain
 ch-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x )
-→ ( chainf : Ordinal → HOD ) → ( lt : ( z : Ordinal ) → z o< x → Chain A f ay z ( chainf z ))
+→ ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f ay z ( chainf z z<x ))
 → Chain A f ay x
-record { od = record { def = λ z → odef A z ∧ (UChain chainf x z ∨ FClosure A f y z ) }
+record { od = record { def = λ z → odef A z ∧ (UChain x chainf z ∨ FClosure A f y z ) }
-; odmax = & A ; <odmax = λ {y} sy → {!!}   }
+; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
-Chain-uniq : (A : HOD ) ( f : Ordinal → Ordinal ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal)
-→ ( Ordinal → HOD ) → Set (Level.suc n)
-Chain-uniq A f {y} ay x chain  with Oprev-p x
-... | yes op = st1 where
-px = Oprev.oprev op
-st1 : Set (Level.suc n)
-st1 with ODC.∋-p O A (* x)
-... | no noax = chain x ≡ chain px
-... | yes ax with ODC.p∨¬p O ( HasPrev A (chain px) ax f )
-... | case1 pr = chain x ≡ chain px
-... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (chain px) ax )
-... | case1 is-sup = chain x ≡ schain where
-schain : HOD
-schain = record { od = record { def = λ x → odef (chain px) x ∨ (FClosure A f y x) } ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
-... | case2 ¬x=sup = chain x ≡ chain px
-... | no ¬ox = chain x ≡ record { od = record { def = λ z → odef A z ∧ ( UChain chain x z ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = λ {y} sy → {!!}   }
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
 field
-chain : Ordinal → HOD
+chain : HOD
-chain-mono : {x : Ordinal} → x o≤ z → chain x ⊆' chain z
+chain-uniq : Chain A f ay z chain
-chain-uniq : Chain-uniq A f ay z chain
+record ZChain ( A : HOD )    ( f : Ordinal → Ordinal ) {init : Ordinal} (ay : odef A init)  (zc0 : (x : Ordinal) → ZChain1 A f ay x ) ( z : Ordinal ) : Set (Level.suc n) where
-record ZChain ( A : HOD )    ( f : Ordinal → Ordinal ) {init : Ordinal} (ay : odef A init)  (zc0 : ZChain1 A f ay (& A) ) ( z : Ordinal ) : Set (Level.suc n) where
 chain : HOD
-chain = ZChain1.chain zc0 z
+chain = ZChain1.chain (zc0 z)
 field
 chain⊆A : chain ⊆' A
 chain∋init : odef chain init
 initial : {y : Ordinal } → odef chain y → * init ≤ * y
 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
 cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) →  odef A x → ( * x < * (cf nmx x) ) ∧  odef A (cf nmx x )
 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  ) ⟫
-sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f as0 (& A) ) (zc : ZChain A f as0 zc0 (& A) )
+sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : (x : Ordinal) → ZChain1 A f as0 x ) (zc : ZChain A f as0 zc0 (& A) )
 (total : IsTotalOrderSet (ZChain.chain zc) )  → SUP A (ZChain.chain zc)
 sp0 f mf zc0 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
 zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y)
 ---
 --- the maximum chain  has fix point of any ≤-monotonic function
 ---
-fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f as0 (& A)) (zc : ZChain A f as0 zc0 (& A) )
+fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : (x : Ordinal) → ZChain1 A f as0 x) (zc : ZChain A f as0 zc0 (& A) )
 → (total : IsTotalOrderSet (ZChain.chain zc) )
 → f (& (SUP.sup (sp0 f mf zc0 zc total ))) ≡ & (SUP.sup (sp0 f mf zc0 zc  total))
 fixpoint f mf zc0 zc total = z14 where
 chain = ZChain.chain zc
 sp1 = sp0 f mf zc0 zc total
 -- ZChain contradicts ¬ Maximal
 --
 -- ZChain forces fix point on any ≤-monotonic function (fixpoint)
 -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain
 --
-z04 :  (nmx : ¬ Maximal A ) → (zc0 : ZChain1 A (cf nmx) as0 (& A)) (zc : ZChain A (cf nmx) as0 zc0 (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥
+z04 :  (nmx : ¬ Maximal A ) → (zc0 : (x : Ordinal) → ZChain1 A (cf nmx) as0 x) (zc : ZChain A (cf nmx) as0 zc0 (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥
 z04 nmx zc0 zc total = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal  sp1 ))))
 (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) )
 (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc0 zc total ))) -- x ≡ f x ̄
 (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1 ))) where          -- x < f x
 sp1 : SUP A (ZChain.chain zc)
 px = Oprev.oprev op
 px<x : px o< x
 px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
 sc : ZChain1 A f ay px
 sc = prev px px<x
-no-ext : ZChain1 A f ay x
-no-ext = record { chain = s01 ; chain-mono = ? ; chain-uniq = s02 } where
-s01 : Ordinal → HOD
-s01 z with trio< z x
-... | tri< a ¬b ¬c = chain (prev z a ) z
-... | tri≈ ¬a b ¬c = chain (prev px px<x ) px
-... | tri> ¬a ¬b c = chain (prev px px<x ) px
-s02 : Chain-uniq A f ay x s01
-s02 with trio< x x
-... | tri< a ¬b ¬c = ?
-... | tri≈ ¬a refl ¬c = ?
-... | tri> ¬a ¬b c = ?
 sc4 : ZChain1 A f ay x
 sc4 with ODC.∋-p O A (* x)
-... | no noax = {!!}
+... | no noax = record { chain = ? ; chain-uniq = ? }
-... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain1.chain sc x) ax f )
+... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain1.chain sc ) ax f )
 ... | case1 pr = {!!}
-... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.chain sc x) ax )
+... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.chain sc ) ax )
 ... | case1 is-sup = {!!} where
 -- A∋sc -- x is a sup of zc
-sup0 : SUP A (ZChain1.chain sc x )
+sup0 : SUP A (ZChain1.chain sc  )
 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
-x21 :  {y : HOD} → (ZChain1.chain sc x) ∋ y → (y ≡ * x) ∨ (y < * x)
+x21 :  {y : HOD} → (ZChain1.chain sc ) ∋ y → (y ≡ * x) ∨ (y < * x)
 x21 {y} zy with IsSup.x<sup is-sup zy
 ... | case1 y=x = case1 (subst₂ (λ j k → j ≡ * k ) *iso &iso ( cong (*) y=x)  )
 ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x  )
 sp : HOD
 sp = SUP.sup sup0
 schain : HOD
-schain = record { od = record { def = λ x → odef (ZChain1.chain sc x) x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
+schain = record { od = record { def = λ x → odef A x ∧ ( odef (ZChain1.chain sc ) x ∨ (FClosure A f (& sp) x)) }
+; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 ... | case2 ¬x=sup = {!!}
 ... | no ¬ox = ? where
+supf : (z : Ordinal) → z o< x → HOD
+supf = ?
 sc5 : HOD
-sc5 = record { od = record { def = λ z → odef A z ∧ (UChain ? x z ∨ FClosure A f y z)} ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
+sc5 = record { od = record { def = λ z → odef A z ∧ (UChain x supf z ∨ FClosure A f y z)} ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
-ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → (zc0 : ZChain1 A f ay (& A))
+ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → (zc0 : (x : Ordinal) → ZChain1 A f ay x)
 → ((z : Ordinal) → z o< x → ZChain A f ay zc0 z) → ZChain A f ay zc0 x
 ind f mf {y} ay x zc0 prev with Oprev-p x
 ... | yes op = zc4 where
 --
 -- we have previous ordinal to use induction
 --
 px = Oprev.oprev op
 supf : Ordinal → HOD
-supf = ZChain1.chain zc0
+supf x = ZChain1.chain (zc0 x)
 zc : ZChain A f ay zc0 (Oprev.oprev op)
 zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )
 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
 px<x : px o< x
 ... | case2 b=sup = ⊥-elim ( ¬x=sup record {
 x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } )
 ... | no ¬ox = record { chain⊆A = {!!} ; f-next = {!!} ; f-total = ?
 ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!} }   where --- limit ordinal case
 supf : Ordinal → HOD
-supf = ZChain1.chain zc0
+supf x = ZChain1.chain (zc0 x)
-uzc : {z : Ordinal} → (u : UChain supf x z) → ZChain A f ay zc0 (UChain.u u)
+uzc : {z : Ordinal} → (u : UChain x ? z) → ZChain A f ay zc0 (UChain.u u)
 uzc {z} u =  prev (UChain.u u) (UChain.u<x u)
 Uz : HOD
-Uz = record { od = record { def = λ z → odef A z ∧ ( UChain supf z x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = ?  }
+Uz = record { od = record { def = λ z → odef A z ∧ ( UChain z ? x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = ?  }
 u-next : {z : Ordinal} → odef Uz z → odef Uz (f z)
 u-next {z} = ?
 -- (case1 u) = case1 record { u = UChain.u u ; u<x = UChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UChain.chain∋z u)  }
 -- u-next {z} (case2 u) = case2 ( fsuc _ u )
 u-initial :  {z : Ordinal} → odef Uz z → * y ≤ * z
 -- u-initial {z} (case2 u) = s≤fc _ f mf u
 u-chain∋init :  odef Uz y
 u-chain∋init = ? -- case2 ( init ay )
 supf0 : Ordinal → HOD
 supf0 z with trio< z x
-... | tri< a ¬b ¬c = ZChain1.chain zc0 z
+... | tri< a ¬b ¬c = ZChain1.chain (zc0 z)
 ... | tri≈ ¬a b ¬c = Uz
 ... | tri> ¬a ¬b c = Uz
 u-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w
 u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
 ... | s | t = ?
 seq : Uz ≡ supf0 x
 seq with trio< x x
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
 ... | tri≈ ¬a b ¬c = refl
 ... | tri> ¬a ¬b c = refl
-seq<x : {b : Ordinal } → (b<x : b o< x ) →  ZChain1.chain zc0 b  ≡ supf0 b
+seq<x : {b : Ordinal } → (b<x : b o< x ) →  ZChain1.chain (zc0 b)  ≡ supf0 b
 seq<x {b} b<x with trio< b x
-... | tri< a ¬b ¬c = cong (λ k → ZChain1.chain zc0 b) o<-irr --  b<x ≡ a
+... | tri< a ¬b ¬c = cong (λ k → ZChain1.chain (zc0 b)) o<-irr --  b<x ≡ a
 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
 ord≤< : {x y z : Ordinal} → x o< z → z o≤ y → x o< y
 ord≤< {x} {y} {z} x<z z≤y  with  osuc-≡< z≤y
 ... | case1 z=y  = subst (λ k → x o< k ) z=y x<z
 ... | case2 z<y  = ordtrans x<z z<y
-SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain1 A f ay (& A)
+SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f ay x
-SZ0 f mf ay = TransFinite {λ z → ZChain1 A f ay z} (sind f mf ay ) (& A)
+SZ0 f mf ay x = TransFinite {λ z → ZChain1 A f ay z} (sind f mf ay ) x
 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f ay (SZ0 f mf ay)  (& A)
 SZ f mf {y} ay = TransFinite {λ z → ZChain A f ay (SZ0 f mf ay)  z  } (λ x → ind f mf ay x (SZ0 f mf ay)  ) (& A)
 zorn00 : Maximal A
 -- if we have no maximal, make ZChain, which contradict SUP condition
 nmx : ¬ Maximal A
 nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
 zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y))
 zc5 = ⟪  Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫
-zc0 : ZChain1 A  (cf nmx) as0 (& A)
+zc0 : (x : Ordinal) → ZChain1 A  (cf nmx) as0 x
-zc0 = TransFinite {λ z → ZChain1 A (cf nmx) as0 z} (sind (cf nmx) (cf-is-≤-monotonic nmx)  as0) (& A)
+zc0 x = TransFinite {λ z → ZChain1 A (cf nmx) as0 z} (sind (cf nmx) (cf-is-≤-monotonic nmx)  as0) x
 zorn04 : ZChain A (cf nmx) as0 zc0 (& A)
 zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
 total : IsTotalOrderSet (ZChain.chain zorn04)
 total {a} {b} = zorn06  where
 zorn06 :  odef (ZChain.chain zorn04) (& a) → odef (ZChain.chain zorn04) (& b) → Tri (a < b) (a ≡ b) (b < a)

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

comparison src/zorn.agda @ 661:9142e834c4c6