Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 607:74c0ae81e482
SupF and ChainMono
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 16 Jun 2022 09:58:13 +0900 |
| parents | 9bdb671cbffd |
| children | 6655f03984f9 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 17 insertions(+), 68 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Jun 14 18:24:17 2022 +0900 +++ b/src/zorn.agda Thu Jun 16 09:58:13 2022 +0900 @@ -233,20 +233,17 @@ field x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) -record FChain ( A : HOD ) ( f : Ordinal → Ordinal ) (p c z : Ordinal) ( x : Ordinal ) : Set n where - field - fc∨sup : FClosure A f p x - chain∋p : odef (* c) p - -record FSup ( A : HOD ) ( f : Ordinal → Ordinal ) (p c z : Ordinal) ( x : Ordinal ) : Set n where +record SupF (A : HOD) : Set n where field - sup : (z : Ordinal) → FClosure A f p z → * z < * x - chain∋p : odef (* c) p + chain : Ordinal + sup : Ordinal + asup : odef A sup + supf-isSup : IsSup A (* chain) asup -data Fc∨sup (A : HOD) {y : Ordinal} (ay : odef A y) ( f : Ordinal → Ordinal ) (c z : Ordinal) : (x : Ordinal) → Set n where - Finit : {i : Ordinal} → i ≡ y → Fc∨sup A ay f c z i - Fsup : {p x : Ordinal} → p o< x → Fc∨sup A ay f c z p → FSup A f p c z x → x o< osuc z → Fc∨sup A ay f c z x - Fc : {p x : Ordinal} → p o< x → Fc∨sup A ay f c z p → FChain A f p c z x → Fc∨sup A ay f c z x +record ChainMono (A chain : HOD) (z : Ordinal) : Set n where + supf : (x : Ordinal) → SupF A + supfz=chain : SupF.chain z ≡ & chain + supf-mono : {x y : Ordinal} → x o< y → y o< osuc z → SupF.sup (supf x ) o< SupF.sup (supf y ) record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where field @@ -260,9 +257,7 @@ is-max : {a b : Ordinal } → (ca : odef chain a ) → b o< osuc z → (ab : odef A b) → HasPrev A chain ab f ∨ IsSup A chain ab → * a < * b → odef chain b - chain∋sup : (s : HOD) → s ⊆' chain → {b : Ordinal} (ab : odef A b) → b o< osuc z → IsSup A s ab → odef chain b - fc∨sup : {c : Ordinal } → ( ca : odef chain c ) → Fc∨sup A (chain⊆A chain∋x) f (& chain) z c - + fc∨sup : ChainMono A chain z record Maximal ( A : HOD ) : Set (Level.suc n) where field @@ -407,15 +402,13 @@ init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain A y f x init-chain {y} {x} ay f mf x≤y = record { chain = ys ay f mf ; chain⊆A = λ fx → A∋fc y f mf fx ; f-total = i-total ; f-next = λ {x} sx → fsuc x sx ; chain∋sup = {!!} - ; initial = {!!} ; f-immediate = {!!} ; chain∋x = init ay ; is-max = is-max ; fc∨sup = it01 } where + ; initial = {!!} ; f-immediate = {!!} ; chain∋x = init ay ; is-max = is-max ; fc∨sup = {!!} } where i-total : IsTotalOrderSet (ys ay f mf ) i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb) is-max : {a b : Ordinal} → odef (ys ay f mf) a → b o< osuc x → (ab : odef A b) → HasPrev A (ys ay f mf) ab f ∨ IsSup A (ys ay f mf) ab → * a < * b → odef (ys ay f mf) b is-max {a} {b} yca b≤x ab P a<b = {!!} - it01 : {c : Ordinal} → odef (ys ay f mf) c → Fc∨sup A (A∋fc y f mf (init ay)) f (& (ys ay f mf)) x c - it01 {c} cc = Fsup {!!} (Finit refl) record { fc∨sup = {!!} ; chain∋p = {!!} } {!!} initial : {i : Ordinal} → odef (ys ay f mf) i → * y ≤ * i initial {i} (init ai) = case1 refl initial .{f x} (fsuc x lt) = {!!} @@ -440,23 +433,12 @@ px<x : px o< x px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc - 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< 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 = zc12 } 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) + ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = {!!} } where -- no extention 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 @@ -475,11 +457,11 @@ 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 = {!!} - ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = {!!} } + ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc17 ; 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 = schain ; chain⊆A = s⊆A ; f-total = scmp ; f-next = scnext ; chain∋sup = {!!} - ; initial = scinit ; f-immediate = simm ; chain∋x = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax ; fc∨sup = s-fc∨sup} where + ; initial = scinit ; f-immediate = simm ; chain∋x = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax ; fc∨sup = {!!} } where sup0 : SUP A (ZChain.chain zc0) sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where x21 : {y : HOD} → ZChain.chain zc0 ∋ y → (y ≡ * x) ∨ (y < * x) @@ -502,9 +484,6 @@ s⊆A : schain ⊆' A s⊆A {x} (case1 zx) = ZChain.chain⊆A zc0 zx s⊆A {x} (case2 fx) = A∋fc (& sp) f mf fx - 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 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 @@ -594,10 +573,7 @@ ... | 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 record { x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy) } ) - ... | no ¬ox with trio< x y - ... | tri< a ¬b ¬c = init-chain ay f mf {!!} - ... | tri≈ ¬a b ¬c = init-chain ay f mf {!!} - ... | tri> ¬a ¬b y<x = UnionZ where + ... | no ¬ox = UnionZ where UnionZ : ZChain A y f x UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A ; f-total = u-total ; f-next = u-next ; chain∋sup = {!!} ; initial = u-initial ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } where --- limit ordinal case @@ -618,7 +594,7 @@ u-initial : {z : Ordinal} → odef Uz z → * y ≤ * z u-initial {z} u = ZChain.initial ( uzc u ) (UZFChain.chain∋z u) u-chain∋x : odef Uz y - u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) } + u-chain∋x = record { u = y ; u<x = {!!} ; chain∋z = ZChain.chain∋x (prev y {!!} ay ) } u-mono : ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b) → ZChain.chain za ⊆' ZChain.chain zb u-mono a b b<x a≤b za zb {i} zai = TransFinite0 {λ i → odef (chain za) i → odef (chain zb) i } uind i zai where open ZChain @@ -626,35 +602,8 @@ → ((j : Ordinal) → j o< i → odef (chain za) j → odef (chain zb) j) → odef (chain za) i → odef (chain zb) i uind i previ zai = um01 where - FC : Fc∨sup A (chain⊆A za (chain∋x za)) f (& (chain za)) a i - FC = fc∨sup za zai um01 : odef (chain zb) i - um01 with FC - ... | Finit i=y = subst (λ k → odef (chain zb) k ) (sym i=y) ( chain∋x zb ) - ... | Fsup {p} {i} p<i pFC sup i≤b = cb∋i where - i-asup : (z : Ordinal) → FClosure A f p z → * z < * i - i-asup = FSup.sup sup - um06 : odef (chain za) p - um06 = subst (λ k → odef k p ) *iso ( FSup.chain∋p sup ) - -- FClosure A f p is a subset of chain zb - um07 : (i2 : Ordinal) → FClosure A f p i2 → odef (chain zb) i2 - um07 i2 (init ap ) = previ p p<i um06 - um07 i (fsuc j fc) = f-next zb ( um07 j fc ) - um08 : odef (chain zb) p - um08 = previ p p<i um06 - cl : HOD - cl = record { od = record { def = λ x → FClosure A f p x } ; odmax = & A ; <odmax = cl<A } where - cl<A : {i2 : Ordinal} → FClosure A f p i2 → i2 o< & A - cl<A {i2} cl = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (A∋fc p f mf cl) ) ) - cb∋i : odef (chain zb) i - cb∋i = ZChain.chain∋sup zb cl (λ {i2} lt → um07 i2 lt) (chain⊆A za zai) {!!} record { x<sup = λ {i2} cl → case2 (i-asup i2 cl) } - ... | Fc {p} {i} p<i pFC FC with (FChain.fc∨sup FC) - ... | fc = um02 i fc where - um02 : (i2 : Ordinal) → FClosure A f p i2 → odef (chain zb) i2 - um02 i2 (init ap ) = previ p p<i um04 where - um04 : odef (chain za) p - um04 = subst (λ k → odef k p ) *iso ( FChain.chain∋p FC ) - um02 i (fsuc j fc) = f-next zb ( um02 j fc ) + um01 = ? 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-mono (UZFChain.u ux) (UZFChain.u uy)