Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 953:dfb4f7e9c454
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 02 Nov 2022 03:42:53 +0900 |
| parents | 05f54e16f138 |
| children | e43a5cc72287 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 44 insertions(+), 61 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Nov 01 23:16:30 2022 +0900 +++ b/src/zorn.agda Wed Nov 02 03:42:53 2022 +0900 @@ -80,7 +80,7 @@ <-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z ) ftrans<=-< : {x y z : Ordinal } → x <= y → y << z → x << z -ftrans<=-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) ? y<z +ftrans<=-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) (sym (cong (*) eq)) y<z ftrans<=-< {x} {y} {z} (case2 lt) y<z = IsStrictPartialOrder.trans PO lt y<z <=to≤ : {x y : Ordinal } → x <= y → * x ≤ * y @@ -582,12 +582,14 @@ cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ -- - -- Second TransFinite Pass for maximality + -- maximality of chain + -- + -- supf is fixed for z ≡ & A , we can prove order and is-max -- SZ1 : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → ZChain1 A f mf ay zc x - SZ1 f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x where + SZ1 f mf {y} ay zc x = zc1 x where chain-mono1 : {a b c : Ordinal} → a o≤ b → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c chain-mono1 {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b @@ -634,8 +636,8 @@ ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z)) ) eq ) ... | case2 lt = case2 (subst₂ (λ j k → j < * k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) )) lt ) - zc1 : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x - zc1 x prev with Oprev-p x -- prev is not used now.... + zc1 : (x : Ordinal) → ZChain1 A f mf ay zc x + zc1 x with Oprev-p x -- prev is not used now.... ... | yes op = record { is-max = is-max ; order = order } where px = Oprev.oprev op zc-b<x : {b : Ordinal } → ZChain.supf zc b o< ZChain.supf zc x → b o< osuc px @@ -866,51 +868,61 @@ zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ zc11 {z} ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ = zc21 fc where u<x : u o< x - u<x = ? + u<x = supf-inject0 supf1-mono su<sx + u≤px : u o≤ px + u≤px = zc-b<x _ u<x zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ ... | case2 fc = case2 (fsuc _ fc) - zc21 (init asp refl ) with trio< u px | inspect supf1 u - ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u ? record {fcy<sup = zc13 ; order = zc17 - ; supu=u = trans (sym (sf1=sf0 (o<→≤ a))) (ChainP.supu=u is-sup) } (init asp refl) ⟫ where + zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) | inspect supf1 u + ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = zc17 + ; supu=u = trans (sym (sf1=sf0 (o<→≤ u<px))) (ChainP.supu=u is-sup) } (init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where + u<px : u o< px + u<px = ZChain.supf-inject zc a + asp0 : odef A (supf0 u) + asp0 = ZChain.asupf zc zc17 : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) - zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 zc19)) ( ChainP.order is-sup - (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 zc19)) ss<spx) (fcpu fc zc18) ) where - zc19 : u o≤ px - zc19 = o<→≤ a + zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 u≤px)) ( ChainP.order is-sup + (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 u≤px)) ss<spx) (fcpu fc zc18) ) where zc18 : s o≤ px - zc18 = ordtrans (ZChain.supf-inject zc ss<spx) zc19 + zc18 = ordtrans (ZChain.supf-inject zc ss<spx) u≤px zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc ) - ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) (cong supf0 b) asp ) (cong supf0 (sym b)) ) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ u<px)) ( ChainP.fcy<sup is-sup fc ) + ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) b ))) + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ zc12 {z} (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where - u<x : u o< x - u<x = ? + u<px : u o< px + u<px = ZChain.supf-inject zc su<sx + u<x : u o< x + u<x = ordtrans u<px px<x + u≤px : u o≤ px + u≤px = o<→≤ u<px + s1u<s1x : supf1 u o< supf1 x + s1u<s1x = ordtrans<-≤ (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 u≤px )) (sym (sf1=sf0 o≤-refl)) su<sx) (supf1-mono (o<→≤ px<x) ) zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef (UnionCF A f mf ay supf1 x) z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ zc21 (init asp refl ) with trio< u px | inspect supf1 u ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u - ? - record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup) } zc14 ⟫ where + s1u<s1x + record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 u≤px ) (ChainP.supu=u is-sup) } zc14 ⟫ where zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) - zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ ?))) ( ChainP.order is-sup - (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ ?)) ss<spx) (fcup fc s≤px) ) where - s≤px : s o≤ px - s≤px = ? -- ordtrans ( supf-inject0 supf1-mono ss<spx ) (o<→≤ u<x) + zc17 {s} {z1} ss<su fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ u<px))) ( ChainP.order is-sup + (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u<px)) ss<su) (fcup fc s≤px) ) where + s≤px : s o≤ px -- ss<su : supf1 s o< supf1 u + s≤px = ordtrans ( supf-inject0 supf1-mono ss<su ) (o<→≤ u<px) zc14 : FClosure A f (supf1 u) (supf0 u) - zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 ?)) asp) (sf1=sf0 ?) + zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 u≤px)) asp) (sf1=sf0 u≤px) zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) ( ChainP.fcy<sup is-sup fc ) - ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px ? record { fcy<sup = zc13 + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 u≤px )) ( ChainP.fcy<sup is-sup fc ) + ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px (subst (λ k → supf1 k o< supf1 x) b s1u<s1x) record { fcy<sup = zc13 ; order = zc17 ; supu=u = zc18 } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b))) ) ⟫ where zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px ) zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc ) @@ -929,17 +941,19 @@ zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b)) s≤px : s o≤ px s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , ? ⟫ ) + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px ⟫ ) zc12 {z} (case2 fc) = zc21 fc where zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ zc21 (init asp refl ) with osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x ) - ... | case1 sfpx=px = ⟪ asp , ch-is-sup px ? -- (pxo<x op) + ... | case1 sfpx=px = ⟪ asp , ch-is-sup px zc18 record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where zc15 : supf1 px ≡ px zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px) + zc18 : supf1 px o< supf1 x + zc18 = ? zc14 : FClosure A f (supf1 px) (supf0 px) zc14 = init (subst (λ k → odef A k) (sym (sf1=sf0 o≤-refl)) asp) (sf1=sf0 o≤-refl) zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px ) @@ -1309,37 +1323,6 @@ SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf ay x SZ f mf {y} ay x = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) x - data ZChainP ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) - ( supf : Ordinal → Ordinal ) (z : Ordinal) : Set n where - zchain : (uz : Ordinal ) → odef (UnionCF A f mf ay supf uz) z → ZChainP f mf ay supf z - - auzc : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) - (supf : Ordinal → Ordinal ) → {x : Ordinal } → ZChainP f mf ay supf x → odef A x - auzc f mf {y} ay supf {x} (zchain uz ucf) = proj1 ucf - - zp-uz : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) - (supf : Ordinal → Ordinal ) → {x : Ordinal } → ZChainP f mf ay supf x → Ordinal - zp-uz f mf ay supf (zchain uz _) = uz - - uzc⊆zc : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) - (supf : Ordinal → Ordinal ) → {x : Ordinal } → (zp : ZChainP f mf ay supf x ) → UChain A f mf ay supf (zp-uz f mf ay supf zp) x - uzc⊆zc f mf {y} ay supf {x} (zchain uz ⟪ ua , ch-init fc ⟫) = ch-init fc - uzc⊆zc f mf {y} ay supf {x} (zchain uz ⟪ ua , ch-is-sup u u<x is-sup fc ⟫) with ChainP.supu=u is-sup - ... | eq = ch-is-sup u u<x is-sup fc - - UnionZF : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) - (supf : Ordinal → Ordinal ) → HOD - UnionZF f mf {y} ay supf = record { od = record { def = λ x → ZChainP f mf ay supf x } - ; odmax = & A ; <odmax = λ lt → ∈∧P→o< ⟪ auzc f mf ay supf lt , lift true ⟫ } - - uzctotal : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) - → ( supf : Ordinal → Ordinal ) - → IsTotalOrderSet (UnionZF f mf ay supf ) - uzctotal f mf ay supf {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (uz01 ca cb) where - uz01 : {ua ub : Ordinal } → ZChainP f mf ay supf ua → ZChainP f mf ay supf ub - → Tri (* ua < * ub) (* ua ≡ * ub) (* ub < * ua ) - uz01 {ua} {ub} (zchain uza uca) (zchain uzb ucb) = chain-total A f mf ay supf (proj2 uca) (proj2 ucb) - msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) → (zc : ZChain A f mf ay x ) → MinSUP A (UnionCF A f mf ay (ZChain.supf zc) x)