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

comparison src/zorn.agda @ 567:4d8a54e2861e

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sun, 01 May 2022 05:35:36 +0900
parents	a64dad8d2e93
children	666377324edd

comparison

equal deleted inserted replaced

-:a64dad8d2e93
+:4d8a54e2861e
 -- open import Relation.Binary.Properties.Poset as Poset
 IsTotalOrderSet : ( A : HOD ) → Set (Level.suc n)
 IsTotalOrderSet A = {a b : HOD} → odef A (& a) → odef A (& b)  → Tri (a < b) (a ≡ b) (b < a )
+⊆-IsTotalOrderSet : { A B : HOD } →  B ⊆ A  → IsTotalOrderSet A → IsTotalOrderSet B
+⊆-IsTotalOrderSet = {!!}
 record Maximal ( A : HOD )  : Set (Level.suc n) where
 field
 maximal : HOD
 A∋maximal : A ∋ maximal
 ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 --
 -- inductive maxmum tree from x
 -- tree structure
 --
-record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x)  ( f : Ordinal → Ordinal )  : Set n where
+record HasPrev (A B : HOD) {x : Ordinal } (xa : odef A x)  ( f : Ordinal → Ordinal )  : Set n where
 field
 y : Ordinal
 ay : odef B y
 x=fy :  x ≡ f y
+_⊆'_ : ( A B : HOD ) → Set n
+_⊆'_ A B = (x : Ordinal ) → odef A x → odef B x
+record IsSup (A : HOD) (T : IsTotalOrderSet A) {x : Ordinal }
+(xa : odef A x)  (sup : (C : HOD ) → ( C ⊆ A) → IsTotalOrderSet C → Ordinal) ( f : Ordinal → Ordinal )  : Set n where
+field
+chain : Ordinal
+chain⊆A : (* chain) ⊆' A
+-- ¬prev : ¬ HasPrev A (* chain) xa f
+x=sup :  x ≡ sup  (* chain)  record { incl = λ {x} → chain⊆A (& x) } ( ⊆-IsTotalOrderSet {A} {* chain} record { incl = λ {x} → chain⊆A (& x) } T )
 record SUP ( A B : HOD )  : Set (Level.suc n) where
 field
 sup : HOD
 A∋maximal : A ∋ sup
 initial : {y : Ordinal } → odef chain y → * x ≤ * y
 f-total : IsTotalOrderSet chain
 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
 f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
 is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ba : odef A b)
-→ Prev< A chain ba f ∨  ((sup  chain  chain⊆A  f-total) ≡ b )
+→ HasPrev A chain ba f ∨  ((sup  chain  chain⊆A  f-total) ≡ b )
 → * a < * b  → odef chain b
 Zorn-lemma : { A : HOD }
 → o∅ o< & A
 → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
 → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc ))
 z03 f mf zc = z14 where
 chain = ZChain.chain zc
 sp1 = sp0 f mf zc
 z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b )
-→  Prev< A chain ab f ∨  (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
+→  HasPrev A chain ab f ∨  (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
 → * a < * b  → odef chain b
 z10 = ZChain.is-max zc
 z11 : & (SUP.sup sp1) o< & A
 z11 = c<→o< ( SUP.A∋maximal sp1)
 z12 : odef chain (& (SUP.sup sp1))
 ... | no noapx =  -- ¬ A ∋ p, just skip
 record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0
 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 }  where -- no extention
 zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ba : odef A b) →
-Prev< A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0))) ≡ b) →
+HasPrev A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0))) ≡ b) →
 * a < * b → odef (ZChain.chain zc0) b
 zc11 {a} {b} za b<ox ba P a<b with osuc-≡< b<ox
 ... | case1 eq = ⊥-elim ( noapx (subst (λ k → odef A k) (trans eq (sym &iso)) ba ) )
 ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt )  ba P a<b
-... | yes apx with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) apx f )   -- we have to check adding x preserve is-max ZChain A ay f mf supO x
+... | yes apx with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) apx f )   -- we have to check adding x preserve is-max ZChain A ay f mf supO x
 ... | case1 pr = zc9 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
 chain = ZChain.chain zc0
 zc17 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ba : odef A b) →
-Prev< A (ZChain.chain zc0) ba f ∨ (supO (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0) ≡ b) →
+HasPrev A (ZChain.chain zc0) ba f ∨ (supO (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0) ≡ b) →
 * a < * b → odef (ZChain.chain zc0) b
 zc17 {a} {b} za b<ox ba P a<b with osuc-≡< b<ox
 ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt) ba P a<b
-... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (Prev<.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (Prev<.ay pr))
+... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
 zc9 :  ZChain A ay f mf supO x
 zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
 ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 }  -- no extention
 ... | case2 ¬fy<x with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) ))
 ... | case1 x=sup = -- previous ordinal is a sup of a smaller ZChain
 ... | case1 sp=a | case2 b<sp = <-irr (case2 (subst (λ k → * b < k ) (trans (sym *iso) sp=a)  b<sp ) ) (proj1 p )
 ... | case2 sp<a | case1 b=sp = <-irr (case2 (subst ( λ  k → k < * a ) (trans *iso (sym b=sp)) sp<a  )) (proj1 p )
 ... | case2 sp<a | case2 b<sp = <-irr (case2 (ptrans b<sp (subst (λ k → k < * a) *iso sp<a ))) (proj1 p )
 simm {a} {b} (case2 sa) (case2 sb) p = fcn-imm {A} (& sp) {a} {b} f mf sa sb p
 s-ismax : {a b : Ordinal} → odef schain a → b o< osuc x → (ba : odef A b) →
-Prev< A schain ba f ∨ (& (SUP.sup (supP schain record { incl = A∋schain } scmp)) ≡ b)
+HasPrev A schain ba f ∨ (& (SUP.sup (supP schain record { incl = A∋schain } scmp)) ≡ b)
 → * a < * b → odef schain b
-s-ismax {a} {b} (case1 za) b<x ba p a<b with osuc-≡< b<x
+s-ismax {a} {b} (case1 za) b<x ba (case1 p) a<b with osuc-≡< b<x
-... | case2 b<x = case1 (ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  b<x ) ba ? a<b )
+... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) (sym (trans b=x x=sup )) (init (SUP.A∋maximal sup0) ))
-... | case1 b=x = {!!}
+... | case2 b<x = z21 p where
-s-ismax {a} {b} (case2 sa) b<x ba p a<b = ?
+z21 : HasPrev A schain ba f → odef schain b
+z21 record { y = y ; ay = (case1 zy) ; x=fy = x=fy } =
+case1 (ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  b<x ) ba (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b )
+z21 record { y = y ; ay = (case2 sy) ; x=fy = x=fy } = subst (λ k → odef schain k) (sym x=fy) (case2 (fsuc y sy) )
+s-ismax {a} {b} (case1 za) b<x ba (case2 p) a<b with osuc-≡< b<x
+... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) (sym (trans b=x x=sup )) (init (SUP.A∋maximal sup0) ))
+... | case2 b<x = z22 p  where
+z22 : & (SUP.sup (supP schain record { incl = A∋schain } scmp)) ≡ b → odef schain b
+z22 p = {!!}
+-- case1 (ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  b<x ) ba {!!} a<b )
+s-ismax {a} {b} (case2 sa) b<x ba p a<b = {!!}
 ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
 record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
 ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 }  where -- no extention
 z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ba : odef A b) →
-Prev< A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0))) ≡ b) →
+HasPrev A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0))) ≡ b) →
 * a < * b → odef (ZChain.chain zc0) b
 z18 {a} {b} za b<x ba p a<b with osuc-≡< b<x
 ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  lt ) ba p a<b
 ... | case1 b=x with p
-... | case1 pr = ⊥-elim ( ¬fy<x record {y = Prev<.y pr ; ay = Prev<.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (Prev<.x=fy pr ) } )
+... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
 ... | case2 b=sup = ⊥-elim ( ¬x=sup (sym (trans  b=sup  b=x )) )
 ... | no ¬ox =  {!!}  where --- limit ordinal case
 record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
 field
 u : Ordinal

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

comparison src/zorn.agda @ 567:4d8a54e2861e