Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 589:b1e76b7991b0
give up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 09 Jun 2022 05:13:18 +0900 |
| parents | cc416fc0ef84 |
| children | |
| files | src/zorn.agda |
| diffstat | 1 files changed, 19 insertions(+), 16 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Jun 09 03:16:59 2022 +0900 +++ b/src/zorn.agda Thu Jun 09 05:13:18 2022 +0900 @@ -254,7 +254,6 @@ chainf : (b : Ordinal) → HOD zchain : ZChain A x f chainf z chain-mono : {a b : Ordinal} → a o< b → b o< osuc z → chainf a ⊆' chainf b - chain=zchain : chainf z ≡ ZChain.chain zchain record Maximal ( A : HOD ) : Set (Level.suc n) where field @@ -397,7 +396,7 @@ → ((z : Ordinal) → z o< x → {y : Ordinal} → odef A y → ZChain∧Chain A y f z) → {y : Ordinal} → odef A y → ZChain∧Chain A y f x ind f mf x prevzc {y} ay with Oprev-p x - ... | yes op = record { zchain = zc4 ; chainf = {!!} ; chain-mono = {!!} ; chain=zchain = {!!} } where + ... | yes op = record { zchain = zc4 ; chainf = chainf ; chain-mono = {!!} } where -- -- we have previous ordinal to use induction -- @@ -411,7 +410,16 @@ zc0-b<x : (b : Ordinal ) → b o< x → b o< osuc px zc0-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt - zc4 : ZChain A y f {!!} x + chainf : Ordinal → HOD + chainf z with ODC.∋-p O A (* x) + ... | no noax = {!!} + ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax f ) -- we have to check adding x preserve is-max ZChain A y f mf supO x + ... | case1 pr = {!!} + ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax ) + ... | case1 is-sup = {!!} -- x is a sup of zc0 + ... | case2 ¬x=sup = {!!} -- x is not f y' nor sup of former ZChain from y + + zc4 : ZChain A y f chainf x zc4 with ODC.∋-p O A (* x) ... | no noax = -- ¬ A ∋ p, just skip record { chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 @@ -432,9 +440,9 @@ zc17 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b ... | 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 y f {!!} 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 -- no extention - ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = {!!} } + zc9 : ZChain A y f chainf x + zc9 = {!!} -- record { chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} -- no extention + -- ; initial = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax ) ... | case1 is-sup = -- x is a sup of zc0 record { chain⊆A = s⊆A ; f-total = scmp ; f-next = scnext @@ -538,7 +546,7 @@ ... | case1 y=b = subst (λ k → odef chain k ) y=b ( ZChain.chain∋x zc0 ) ... | case2 y<b = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<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 + record { 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 ; fc∨sup = {!!} } where -- no extention z18 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) → @@ -554,14 +562,14 @@ ... | tri< a ¬b ¬c = record { zchain = record { chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; initial = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } - ; chainf = {!!} ; chain-mono = {!!} ; chain=zchain = {!!} } + ; chainf = {!!} ; chain-mono = {!!} } ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b y<x = record { zchain = UnionZ - ; chainf = {!!} ; chain-mono = {!!} ; chain=zchain = {!!} } where + ; chainf = {!!} ; chain-mono = {!!} } where prev : (z : Ordinal) → (z<x : z o< x )→ {y : Ordinal} → (ay : odef A y) → ZChain A y f (ZChain∧Chain.chainf (prevzc z z<x ay)) z prev z z<x ay = ZChain∧Chain.zchain (prevzc z z<x ay) UnionZ : ZChain A y f {!!} x - UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A ; f-total = u-total ; f-next = u-next + UnionZ = record { chain⊆A = Uz⊆A ; f-total = u-total ; f-next = u-next ; initial = u-initial ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } where --- limit ordinal case record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x field @@ -590,15 +598,10 @@ u0y = prevzc (UZFChain.u uy) (UZFChain.u<x uy) {y} ay u03 : odef (ZChain∧Chain.chainf u0y (UZFChain.u ux)) (& x) → odef (ZChain∧Chain.chainf u0y (UZFChain.u uy)) (& x) u03 = ZChain∧Chain.chain-mono u0y x<y {!!} - u02 : ZChain∧Chain.chainf u0x (UZFChain.u ux) ≡ ZChain.chain (ZChain∧Chain.zchain u0x) - u02 = ZChain∧Chain.chain=zchain u0x u04 : ZChain∧Chain.chainf u0y (UZFChain.u ux) ≡ ZChain.chain (ZChain∧Chain.zchain u0x) u04 = {!!} u01 : odef (ZChain.chain (uzc ux)) (& x) → odef (ZChain.chain (uzc uy)) (& x) - u01 = subst₂ (λ j k → odef j (& x) → odef k (& x)) - u04 - (ZChain∧Chain.chain=zchain u0y) - ( ZChain∧Chain.chain-mono u0y x<y {!!} ) + u01 = {!!} -- ZChain∧Chain.chain-mono u0y x<y {!!} u-total : IsTotalOrderSet Uz u-total {x} {y} ux uy with trio< (UZFChain.u ux) (UZFChain.u uy) ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-total1 ux uy a (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)