Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/zorn.agda @ 549:f007e044b2c6
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 28 Apr 2022 11:47:18 +0900 |
| parents | 5ad7a31df4f4 |
| children | e1a33b1bc16c |
line wrap: on
line diff
--- a/src/zorn.agda Thu Apr 28 10:29:47 2022 +0900 +++ b/src/zorn.agda Thu Apr 28 11:47:18 2022 +0900 @@ -340,41 +340,30 @@ zc4 with ODC.∋-p O A (* x) ... | no noax = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A 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 = {!!} } where -- no extention - ... | yes ax with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ay f ) - ... | case1 pr = zc7 where -- we have previous < + ... | yes ax with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ax f ) -- we have to check adding x preserve is-max ZChain A ay f mf supO px + ... | case1 pr = zc9 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next + 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 + ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = {!!} } where -- no extention ay0 : odef A (& (* y)) ay0 = (subst (λ k → odef A k ) (sym &iso) ay ) Afx : { x : Ordinal } → A ∋ * x → A ∋ * (f x) Afx {x} ax = (subst (λ k → odef A k ) (sym &iso) (proj2 (mf x (subst (λ k → odef A k ) &iso ax)))) chain = ZChain.chain zc0 zc7 : ZChain A ay f mf supO x - zc7 with ODC.∋-p O (ZChain.chain zc0) (* ( f y ) ) - ... | yes pr = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 - ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = z22 - ; is-max = {!!} } where -- no extention - z22 : odef (ZChain.chain zc0) y -- y ≡ f pr , chain ∋ f y ≡ f (f pr) - z22 = {!!} - zc20 : {P : Ordinal → Set n} → ({a : Ordinal} → odef (ZChain.chain zc0) a → a o< px → P a) - → {a : Ordinal} → (za : odef (ZChain.chain zc0) a ) → (a<x : a o< x) → P a - zc20 {P} prev {a} za a<x with trio< a px - ... | tri< a₁ ¬b ¬c = prev za a₁ - ... | tri≈ ¬a b ¬c = {!!} - ... | tri> ¬a ¬b c = {!!} - z21 : {a : Ordinal} → odef (ZChain.chain zc0) a → a o< x → odef (ZChain.chain zc0) (f a) - z21 {a} za a<x with trio< a x - ... | tri< a₁ ¬b ¬c = ZChain.f-next zc0 za - ... | tri≈ ¬a b ¬c = {!!} - ... | tri> ¬a ¬b c = ⊥-elim ( o<> c a<x ) - ... | no not = record { chain = zc5 ; chain⊆A = ⊆-zc5 - ; f-total = zc6 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x = case1 {!!} ; ¬chain∋x>z = {!!} ; is-max = {!!} } where - -- extend with f x -- cahin ∋ y ∧ chain ∋ f y ∧ x ≡ f ( f y ) + zc7 with trio< (Prev<.y pr) x + ... | tri< a ¬b ¬c = {!!} -- already x ∈ chain because of is-max + ... | tri≈ ¬a b ¬c = {!!} -- x ≡ z ∈ chain + ... | tri> ¬a ¬b x<z = record { chain = zc5 ; chain⊆A = ⊆-zc5 --- + ; f-total = zc6 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x = case1 {!!} ; is-max = {!!} } where + -- extend with x ≡ f z where cahin ∋ z zc5 : HOD - zc5 = record { od = record { def = λ z → odef (ZChain.chain zc0) z ∨ (z ≡ f y) } ; odmax = & A ; <odmax = {!!} } + zc5 = record { od = record { def = λ z → odef (ZChain.chain zc0) z ∨ (z ≡ f x) } ; odmax = & A ; <odmax = {!!} } ⊆-zc5 : zc5 ⊆ A ⊆-zc5 = record { incl = λ {y} lt → zc15 lt } where - zc15 : {z : Ordinal } → ( odef (ZChain.chain zc0) z ∨ (z ≡ f y) ) → odef A z + zc15 : {z : Ordinal } → ( odef (ZChain.chain zc0) z ∨ (z ≡ f x) ) → odef A z zc15 {z} (case1 zz) = subst (λ k → odef A k ) &iso ( incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k ) (sym &iso) zz ) ) - zc15 (case2 refl) = proj2 ( mf y (subst (λ k → odef A k ) &iso {!!} ) ) + zc15 (case2 refl) = proj2 ( mf x (subst (λ k → odef A k ) &iso {!!} ) ) IPO = ⊆-IsPartialOrderSet ⊆-zc5 PO zc8 : { A B x : HOD } → (ax : A ∋ x ) → (P : Prev< A B ax f ) → * (f (& (* (Prev<.y P)))) ≡ x zc8 {A} {B} {x} ax P = subst₂ (λ j k → * ( f j ) ≡ k ) (sym &iso) *iso (sym (cong (*) ( Prev<.x=fy P))) @@ -399,19 +388,18 @@ zc10 : * y ≡ b zc10 = subst₂ (λ j k → j ≡ k ) (zc8 ay {!!} ) (zc8 (incl ( ZChain.chain⊆A zc0 ) c) fb) (cong (λ k → * ( f ( & k ))) b₁) zc11 : * (f y) ≡ a - zc11 = subst (λ k → * (f y) ≡ k ) *iso (cong (*) (sym fx)) + zc11 = subst (λ k → * (f y) ≡ k ) *iso (cong (*) (sym {!!} )) zc12 : odef chain y zc12 = subst (λ k → odef chain k ) (subst (λ k → & b ≡ k ) &iso (sym (cong (&) zc10))) c ... | tri> ¬a ¬b c₁ = {!!} zc6 : IsTotalOrderSet zc5 zc6 = record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z} ; compare = cmp } - ... | case2 not with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) {!!} {!!} ) )) - ... | case1 pr = {!!} -- x is sup - ... | case2 not = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = {!!} + ... | case2 ¬fy<x with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) {!!} {!!} ) )) + ... | case1 x=sup = {!!} -- x is sup + ... | case2 ¬x=sup = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} } -- no extention - ... | no noapx = {!!} -- we have previous ordinal but ¬ A ∋ op - ind f mf x prev ya | no ¬ox with trio< (& A) x --- limit ordinal case + ... | no ¬ox with trio< (& A) x --- limit ordinal case ... | tri< a ¬b ¬c = {!!} where zc0 = prev (& A) a ... | tri≈ ¬a b ¬c = {!!}