Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/zorn.agda @ 624:d0938f220648
supf again
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 20 Jun 2022 07:49:35 +0900 |
| parents | 7c5a922931e5 |
| children | 886e1f82cca0 |
line wrap: on
line diff
--- a/src/zorn.agda Fri Jun 17 21:45:33 2022 +0900 +++ b/src/zorn.agda Mon Jun 20 07:49:35 2022 +0900 @@ -233,21 +233,13 @@ field x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) -record SupF (A : HOD) : Set n where - field - chain : Ordinal - -- sup : Ordinal - -- asup : odef A sup - -- is-sup : IsSup A (* chain) asup - -record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) (supf : Ordinal → SupF A) ( z : Ordinal ) : Set (Level.suc n) where +record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) (supf : Ordinal → HOD) ( z : Ordinal ) : Set (Level.suc n) where chain : HOD - chain = * (SupF.chain (supf z )) + chain = supf z field chain⊆A : chain ⊆' A chain∋x : odef chain x 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 → (ab : odef A b) @@ -256,9 +248,10 @@ record ZChain1 ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where field - supf : Ordinal → SupF A + supf : Ordinal → HOD zc : ZChain A x f supf z - chain-mono : {x y : Ordinal} → x o≤ y → y o< osuc z → * (SupF.chain (supf x )) ⊆' * (SupF.chain (supf y )) + chain-mono : {x y : Ordinal} → x o≤ y → y o≤ z → supf x ⊆' supf y + f-total : {x y : Ordinal} → x o≤ z → IsTotalOrderSet (supf x) record Maximal ( A : HOD ) : Set (Level.suc n) where field @@ -332,13 +325,13 @@ cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc1 : ZChain1 A (& s) f (& A) ) → SUP A (ZChain.chain (ZChain1.zc zc1)) - zsup f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc ) where + zsup f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain1.f-total zc1 {!!} ) where zc = ZChain1.zc zc1 A∋zsup : (nmx : ¬ Maximal A ) (zc1 : ZChain1 A (& s) (cf nmx) (& A) ) → A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc1 ))) A∋zsup nmx zc1 = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc1 ) ) sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc1 : ZChain1 A (& s) f (& A) ) → SUP A (ZChain.chain (ZChain1.zc zc1)) - sp0 f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain.f-total zc) where + sp0 f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain1.f-total zc1 {!!} ) where zc = ZChain1.zc zc1 zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y) @@ -375,7 +368,7 @@ ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ? (SUP.x<sup sp1 ? ) } z14 : f (& (SUP.sup (sp0 f mf zc1))) ≡ & (SUP.sup (sp0 f mf zc1)) - z14 with ZChain.f-total zc (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 + z14 with ZChain1.f-total zc1 {!!} (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 ... | tri< a ¬b ¬c = ⊥-elim z16 where z16 : ⊥ z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 )) @@ -418,7 +411,7 @@ open ZChain px = Oprev.oprev op - supf : Ordinal → SupF A + supf : Ordinal → HOD supf = ZChain1.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay) zc1 : ZChain1 A y f (Oprev.oprev op) zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay @@ -436,30 +429,29 @@ * a < * b → odef (ZChain.chain zc0) b ) → ZChain1 A y f x no-extenion is-max = record { supf = supf0 ; zc = record { chain⊆A = subst (λ k → k ⊆' A ) seq (ZChain.chain⊆A zc0) ; initial = subst (λ k → {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) seq (ZChain.initial zc0) - ; f-total = subst (λ k → IsTotalOrderSet k ) seq (ZChain.f-total zc0) ; f-next = subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) seq (ZChain.f-next zc0) ; f-immediate = subst (λ k → {x₁ : Ordinal} {y₁ : Ordinal} → odef k x₁ → odef k y₁ → ¬ (* x₁ < * y₁) ∧ (* y₁ < * (f x₁)) ) seq (ZChain.f-immediate zc0) ; chain∋x = subst (λ k → odef k y ) seq (ZChain.chain∋x zc0) ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) → HasPrev A k ab f ∨ IsSup A k ab → * a < * b → odef k b ) seq is-max } ; chain-mono = mono } where - supf0 : Ordinal → SupF A + supf0 : Ordinal → HOD supf0 z with trio< z x ... | tri< a ¬b ¬c = supf z - ... | tri≈ ¬a b ¬c = record { chain = & (ZChain.chain zc0) } - ... | tri> ¬a ¬b c = record { chain = & (ZChain.chain zc0) } - seq : ZChain.chain zc0 ≡ * (SupF.chain (supf0 x)) + ... | tri≈ ¬a b ¬c = ZChain.chain zc0 + ... | tri> ¬a ¬b c = ZChain.chain zc0 + seq : ZChain.chain zc0 ≡ supf0 x seq with trio< x x ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) - ... | tri≈ ¬a b ¬c = sym *iso - ... | tri> ¬a ¬b c = sym *iso - seq<x : {b : Ordinal } → b o< x → * (SupF.chain (supf b)) ≡ * (SupF.chain (supf0 b)) + ... | tri≈ ¬a b ¬c = refl + ... | tri> ¬a ¬b c = refl + seq<x : {b : Ordinal } → b o< x → supf b ≡ supf0 b seq<x {b} b<x with trio< b x ... | tri< a ¬b ¬c = refl ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x ) mono : {a b : Ordinal} → a o≤ b → b o< osuc x → - * (SupF.chain (supf0 a )) ⊆' * (SupF.chain (supf0 b )) + supf0 a ⊆' supf0 b mono {a} {b} a≤b b<ox with osuc-≡< a≤b ... | case1 refl = λ x → x ... | case2 a<b with osuc-≡< b<ox @@ -470,10 +462,10 @@ ... | case2 b<x = ordtrans a<b b<x a≤px : a o≤ px a≤px = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) a<x - nc00 : * (SupF.chain (supf px)) ≡ * (SupF.chain (supf0 b)) + nc00 : supf px ≡ supf0 b nc00 with trio< b x ... | tri< a ¬b ¬c = ⊥-elim ( ¬b b=x ) - ... | tri≈ ¬a b ¬c = sym *iso + ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b=x ) ... | case2 b<x = subst₂ (λ j k → j ⊆' k ) (seq<x a<x ) (seq<x b<x ) ( ZChain1.chain-mono zc1 a≤b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) b<x ) ) @@ -503,8 +495,8 @@ ... | 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)) ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax ) ... | case1 is-sup = -- x is a sup of zc0 - record { zc = record { chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; chain∋sup = {!!} - ; initial = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } ; supf = supf0 ; chain-mono = mono } where + record { zc = record { chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} + ; initial = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} } ; supf = supf0 ; chain-mono = mono } 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) @@ -542,7 +534,7 @@ a<b : a < b a<b = ptrans (subst (λ k → a < k ) (sym *iso) a<sp ) ( subst₂ (λ j k → j < k ) refl *iso sp<b ) scmp : {a b : HOD} → odef schain (& a) → odef schain (& b) → Tri (a < b) (a ≡ b) (b < a ) - scmp (case1 za) (case1 zb) = ZChain.f-total zc0 za zb + scmp (case1 za) (case1 zb) = ZChain1.f-total zc1 {!!} za zb scmp {a} {b} (case1 za) (case2 fb) = cmp za fb scmp (case2 fa) (case1 zb) with cmp zb fa ... | tri< a ¬b ¬c = tri> ¬c (λ eq → ¬b (sym eq)) a @@ -603,23 +595,22 @@ z23 with IsSup.x<sup (z24 p) ( 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 - supf0 : Ordinal → SupF A + supf0 : Ordinal → HOD supf0 z with trio< z x ... | tri< a ¬b ¬c = supf z - ... | tri≈ ¬a b ¬c = record { chain = & schain } - ... | tri> ¬a ¬b c = record { chain = & schain } - seq : schain ≡ * (SupF.chain (supf0 x)) + ... | tri≈ ¬a b ¬c = schain + ... | tri> ¬a ¬b c = schain + seq : schain ≡ supf0 x seq with trio< x x ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) - ... | tri≈ ¬a b ¬c = sym *iso - ... | tri> ¬a ¬b c = sym *iso - seq<x : {b : Ordinal } → b o< x → * (SupF.chain (supf b)) ≡ * (SupF.chain (supf0 b)) + ... | tri≈ ¬a b ¬c = refl + ... | tri> ¬a ¬b c = refl + seq<x : {b : Ordinal } → b o< x → supf b ≡ supf0 b seq<x {b} b<x with trio< b x ... | tri< a ¬b ¬c = refl ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x ) - mono : {a b : Ordinal} → a o≤ b → b o< osuc x → - * (SupF.chain (supf0 a )) ⊆' * (SupF.chain (supf0 b )) + mono : {a b : Ordinal} → a o≤ b → b o< osuc x → supf0 a ⊆' supf0 b mono {a} {b} a≤b b<ox = {!!} ... | case2 ¬x=sup = no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention @@ -655,32 +646,32 @@ 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 = {!!} ; chain∋z = ZChain.chain∋x (ZChain1.zc (prev y {!!} ay )) } - supf0 : Ordinal → SupF A + supf0 : Ordinal → HOD supf0 z with trio< z x ... | tri< a ¬b ¬c = ZChain1.supf (prev z a {y} ay) z - ... | tri≈ ¬a b ¬c = record { chain = & Uz } - ... | tri> ¬a ¬b c = record { chain = & Uz } - seq : Uz ≡ * (SupF.chain (supf0 x)) + ... | tri≈ ¬a b ¬c = Uz + ... | tri> ¬a ¬b c = Uz + seq : Uz ≡ supf0 x seq with trio< x x ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) - ... | tri≈ ¬a b ¬c = sym *iso - ... | tri> ¬a ¬b c = sym *iso - seq<x : {b : Ordinal } → (b<x : b o< x ) → * (SupF.chain (ZChain1.supf (prev b b<x {y} ay) b)) ≡ * (SupF.chain (supf0 b)) + ... | tri≈ ¬a b ¬c = refl + ... | tri> ¬a ¬b c = refl + seq<x : {b : Ordinal } → (b<x : b o< x ) → ZChain1.supf (prev b b<x {y} ay) b ≡ supf0 b seq<x {b} b<x with trio< b x - ... | tri< a ¬b ¬c = cong (λ k → * (SupF.chain (ZChain1.supf (prev b k {y} ay) b)) ) o<-irr -- b<x ≡ a + ... | tri< a ¬b ¬c = cong (λ k → ZChain1.supf (prev b k {y} ay) b) o<-irr -- b<x ≡ a ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x ) u-mono : ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain1 A y f a) (zb : ZChain1 A y f b) → ZChain.chain (ZChain1.zc za) ⊆' ZChain.chain (ZChain1.zc zb) u-mono a b b<x a≤b za zb {i} zai = ZChain1.chain-mono zb a≤b <-osuc (uz01 zai) where - uz01 : odef (* (SupF.chain (ZChain1.supf za a))) i → odef (* (SupF.chain (ZChain1.supf zb a))) i + uz01 : odef (ZChain1.supf za a) i → odef (ZChain1.supf zb a) i uz01 = {!!} 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) + ... | tri< a ¬b ¬c = ZChain1.f-total (uzc1 uy) {!!} (u-mono (UZFChain.u ux) (UZFChain.u uy) (UZFChain.u<x uy) (ordtrans a <-osuc ) (uzc1 ux) (uzc1 uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy) - ... | tri≈ ¬a b ¬c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux) + ... | tri≈ ¬a b ¬c = ZChain1.f-total (uzc1 ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux) (UZFChain.u<x ux) (subst (λ k → k o< osuc (UZFChain.u ux)) b <-osuc) (uzc1 uy) (uzc1 ux) (UZFChain.chain∋z uy)) - ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux) + ... | tri> ¬a ¬b c = ZChain1.f-total (uzc1 ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux) (UZFChain.u<x ux) (ordtrans c <-osuc) (uzc1 uy) (uzc1 ux) (UZFChain.chain∋z uy)) SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain1 A y f (& A)