Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 604:021fcb324990
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 14 Jun 2022 15:32:01 +0900 |
| parents | d68114d45d2f |
| children | b42f0e50a831 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 26 insertions(+), 19 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Jun 14 15:14:28 2022 +0900 +++ b/src/zorn.agda Tue Jun 14 15:32:01 2022 +0900 @@ -412,11 +412,15 @@ -- -- we have previous ordinal to use induction -- + open ZChain + px = Oprev.oprev op zc0 : ZChain A y f (Oprev.oprev op) zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay 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 + px<x : px o< x + px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ys : HOD ys = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = {!!} } @@ -427,20 +431,23 @@ i-total : IsTotalOrderSet ys i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb) - fcs< : {w : Ordinal} (c z : Ordinal) (x : Ordinal) → z o< w → Fc∨sup A ay f c z x → Fc∨sup A ay f c w x - fcs< c z x z<w (Finit x₁) = Finit x₁ - fcs< {w} c z x z<w (Fsup {p} x₁ FC x₂ x₃) = Fsup x₁ (fcs< c z p z<w FC) record { sup = FSup.sup x₂ ; chain∋p = FSup.chain∋p x₂ } + fcs< : (A : HOD) {w y : Ordinal} (ay : odef A y) (c z : Ordinal) (x : Ordinal) + → z o< w → Fc∨sup A ay f c z x → Fc∨sup A ay f c w x + fcs< A ay c z x z<w (Finit x₁) = Finit x₁ + fcs< A {w} ay c z x z<w (Fsup {p} x₁ FC x₂ x₃) = Fsup x₁ (fcs< A ay c z p z<w FC) record { sup = FSup.sup x₂ ; chain∋p = FSup.chain∋p x₂ } (x<ow x₃ z<w ) where x<ow : x o< osuc z → z o< w → x o< osuc w x<ow x<z z<w = ordtrans x<z (osucc z<w) - fcs< {w} c z x z<w (Fc {p} x₁ FC x₂) = Fc x₁ (fcs< c z p z<w FC) record { fc∨sup = FChain.fc∨sup x₂; chain∋p = FChain.chain∋p x₂} + fcs< A {w} ay c z x z<w (Fc {p} x₁ FC x₂) = Fc x₁ (fcs< A ay c z p z<w FC) record { fc∨sup = FChain.fc∨sup x₂; chain∋p = FChain.chain∋p x₂} zc4 : ZChain A y f x zc4 with ODC.∋-p O A (* x) ... | no noax = -- ¬ 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 ; chain∋sup = {!!} - ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = {!!} } where -- no extention + ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = {!!} } where -- no extention + zc12 : {c : Ordinal} → odef (ZChain.chain zc0) c → Fc∨sup A (ZChain.chain⊆A zc0 (ZChain.chain∋x zc0)) f (& (ZChain.chain zc0)) x c + zc12 {c} cc = fcs< A (ZChain.chain⊆A zc0 (ZChain.chain∋x zc0)) (& (ZChain.chain zc0)) px c px<x (ZChain.fc∨sup zc0 cc) zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) → HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0) ab → * a < * b → odef (ZChain.chain zc0) b @@ -449,13 +456,13 @@ ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b ... | 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 = zc9 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next - chain = ZChain.chain zc0 + chain0 = ZChain.chain zc0 zc17 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) → HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0) ab → * a < * b → odef (ZChain.chain zc0) b 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)) + ... | case1 b=x = subst (λ k → odef chain0 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 ; chain∋sup = {!!} @@ -474,12 +481,12 @@ sp = SUP.sup sup0 x=sup : x ≡ & sp x=sup = sym &iso - chain = ZChain.chain zc0 - sc<A : {y : Ordinal} → odef chain y ∨ FClosure A f (& sp) y → y o< & A - sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A zc0 (subst (λ k → odef chain k) (sym &iso) zx ))) + chain0 = ZChain.chain zc0 + sc<A : {y : Ordinal} → odef chain0 y ∨ FClosure A f (& sp) y → y o< & A + sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A zc0 (subst (λ k → odef chain0 k) (sym &iso) zx ))) sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) ) schain : HOD - schain = record { od = record { def = λ x → odef chain x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy } + schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy } A∋schain : {x : HOD } → schain ∋ x → A ∋ x A∋schain (case1 zx ) = ZChain.chain⊆A zc0 zx A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx @@ -489,7 +496,7 @@ s-fc∨sup : {c : Ordinal} → odef schain c → Fc∨sup A (s⊆A (case1 (ZChain.chain∋x zc0))) f (& schain) x c s-fc∨sup {c} (case1 cx) = {!!} s-fc∨sup {c} (case2 fc) = {!!} - cmp : {a b : HOD} (za : odef chain (& a)) (fb : FClosure A f (& sp) (& b)) → Tri (a < b) (a ≡ b) (b < a ) + cmp : {a b : HOD} (za : odef chain0 (& a)) (fb : FClosure A f (& sp) (& b)) → Tri (a < b) (a ≡ b) (b < a ) cmp {a} {b} za fb with SUP.x<sup sup0 za | s≤fc (& sp) f mf fb ... | case1 sp=a | case1 sp=b = tri≈ (λ lt → <-irr (case1 (sym eq)) lt ) eq (λ lt → <-irr (case1 eq) lt ) where eq : a ≡ b @@ -516,15 +523,15 @@ scnext {x} (case2 sx) = case2 ( fsuc x sx ) scinit : {x : Ordinal} → odef schain x → * y ≤ * x scinit {x} (case1 zx) = ZChain.initial zc0 zx - scinit {x} (case2 sx) with (s≤fc (& sp) f mf sx ) | SUP.x<sup sup0 (subst (λ k → odef chain k ) (sym &iso) ( ZChain.chain∋x zc0 ) ) + scinit {x} (case2 sx) with (s≤fc (& sp) f mf sx ) | SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) ( ZChain.chain∋x zc0 ) ) ... | case1 sp=x | case1 y=sp = case1 (trans y=sp (subst (λ k → k ≡ * x ) *iso sp=x ) ) ... | case1 sp=x | case2 y<sp = case2 (subst (λ k → * y < k ) (trans (sym *iso) sp=x) y<sp ) ... | case2 sp<x | case1 y=sp = case2 (subst (λ k → k < * x ) (trans *iso (sym y=sp )) sp<x ) ... | case2 sp<x | case2 y<sp = case2 (ptrans y<sp (subst (λ k → k < * x ) *iso sp<x) ) - A∋za : {a : Ordinal } → odef chain a → odef A a + A∋za : {a : Ordinal } → odef chain0 a → odef A a A∋za za = ZChain.chain⊆A zc0 za - za<sup : {a : Ordinal } → odef chain a → ( * a ≡ sp ) ∨ ( * a < sp ) - za<sup za = SUP.x<sup sup0 (subst (λ k → odef chain k ) (sym &iso) za ) + za<sup : {a : Ordinal } → odef chain0 a → ( * a ≡ sp ) ∨ ( * a < sp ) + za<sup za = SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) za ) simm : {a b : Ordinal} → odef schain a → odef schain b → ¬ (* a < * b) ∧ (* b < * (f a)) simm {a} {b} (case1 za) (case1 zb) = ZChain.f-immediate zc0 za zb simm {a} {b} (case1 za) (case2 sb) p with proj1 (mf a (A∋za za) ) @@ -556,14 +563,14 @@ z22 : IsSup A (ZChain.chain zc0) ab z22 = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) } s-ismax {a} {b} (case2 sa) b<ox ab (case1 p) a<b | case2 b<x with HasPrev.ay p - ... | case1 zy = case1 (subst (λ k → odef chain k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc0 zy )) -- in previous closure of f + ... | case1 zy = case1 (subst (λ k → odef chain0 k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc0 zy )) -- in previous closure of f ... | case2 sy = case2 (subst (λ k → FClosure A f (& (* x)) k ) (sym (HasPrev.x=fy p)) (fsuc (HasPrev.y p) sy )) -- in current closure of f s-ismax {a} {b} (case2 sa) b<ox ab (case2 p) a<b | case2 b<x = case1 z23 where -- sup o< x is already in zc0 z24 : IsSup A schain ab → IsSup A (ZChain.chain zc0) ab z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) } - z23 : odef chain b + z23 : odef chain0 b z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋x zc0 ) - ... | case1 y=b = subst (λ k → odef chain k ) y=b ( ZChain.chain∋x zc0 ) + ... | case1 y=b = subst (λ k → odef chain0 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 ; chain∋sup = {!!}