Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 908:d917831fb607
supf (supf x) ≡ supf x is bad
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 11 Oct 2022 22:47:13 +0900 |
| parents | a6f075a164fa |
| children | fec6064b44be |
| files | src/zorn.agda |
| diffstat | 1 files changed, 37 insertions(+), 16 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Oct 11 10:41:19 2022 +0900 +++ b/src/zorn.agda Tue Oct 11 22:47:13 2022 +0900 @@ -385,6 +385,14 @@ ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso refl lt ) +chain-mono : {A : HOD} ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) + {a b c : Ordinal} → a o≤ b + → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c +chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = + ⟪ ua , ch-init fc ⟫ +chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ uaa , ch-is-sup ua ua<x is-sup fc ⟫ = + ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b ) is-sup fc ⟫ + record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where field @@ -411,7 +419,7 @@ chain∋init : odef chain y chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ - f-next : {a : Ordinal} → odef chain a → odef chain (f a) + f-next : {a z : Ordinal} → odef (UnionCF A f mf ay supf z) a → odef (UnionCF A f mf ay supf z) (f a) f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫ f-next {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫ initial : {z : Ordinal } → odef chain z → * y ≤ * z @@ -448,7 +456,21 @@ -- ordering is not proved here but in ZChain1 - -- supf-idem : {x : Ordinal } → supf x o< z → supf (supf x) ≡ supf x + supf-¬hp : {x : Ordinal } → x o≤ z → odef (UnionCF A f mf ay supf x) (supf x) + → ( supf x ≡ f (supf x) ) ∨ ( ¬ HasPrev A chain (supf x) f ) + supf-¬hp {x} x≤z usx with proj1 ( mf (supf x) asupf ) + ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) eq)) + ... | case2 s<fs = case2 sh00 where + sh00 : ( ¬ HasPrev A chain (supf x) f ) + sh00 hp = <-irr (<=to≤ sh01) s<fs where + sh01 : ( f ( supf x ) ≡ supf x ) ∨ ( f ( supf x ) << supf x ) + sh01 = subst (λ k → ( f ( supf x ) ≡ k ) ∨ ( f ( supf x ) << k )) (sym (supf-is-minsup x≤z)) + ( MinSUP.x<sup ( minsup x≤z ) (f-next usx )) + + supf-idem : {x : Ordinal } → supf x o< z → supf (supf x) ≡ supf x + supf-idem {x} sf<z with csupf sf<z + ... | ⟪ au , ch-init fc ⟫ = ? + ... | ⟪ au , ch-is-sup u u<z is-sup fc ⟫ = ? record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where @@ -566,14 +588,6 @@ cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx ) cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ - chain-mono : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) - {a b c : Ordinal} → a o≤ b - → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c - chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = - ⟪ ua , ch-init fc ⟫ - chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ uaa , ch-is-sup ua ua<x is-sup fc ⟫ = - ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b ) is-sup fc ⟫ - sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay x ) → SUP A (ZChain.chain zc) sp0 f mf ay zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ztotal where @@ -1079,6 +1093,8 @@ -- z1 ≡ px , supf0 px ≡ px psz1≤px : supf1 z1 o≤ px psz1≤px = subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x + cs00 : supf1 (supf1 px) ≡ supf1 px + cs00 = ? csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) csupf2 with trio< z1 px | inspect supf1 z1 csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px @@ -1086,24 +1102,29 @@ record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where -- supf0 z1 ≡ supf1 z1 ≡ px, z1 o< px supu=u : supf1 (supf1 z1) ≡ supf1 z1 - supu=u = ? + supu=u = ? -- ZChain.sup=u zc ? ? ? ... | case2 lt with ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) ... | ⟪ ab , ch-init fc ⟫ = ⟪ ab , ch-init fc ⟫ ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) - record { fcy<sup = ? ; order = ? ; supu=u = ? } (fcpu fc (o<→≤ u<x)) ⟫ + record { fcy<sup = ? ; order = ? ; supu=u = ? } (fcpu fc (o<→≤ u<x)) ⟫ where + supu=u : supf1 (supf1 z1) ≡ supf1 z1 + supu=u = ? -- ZChain.sup=u zc ? ? ? csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ ZChain.asupf zc , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x) record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where -- supf1 z1 ≡ supf0 z1, z1 ≡ px - asm : odef A (supf1 z1) - asm = subst (λ k → odef A k ) ? ( MinSUP.asm sup1) - asm1 : odef A (supf1 (supf1 z1)) - asm1 = subst (λ k → odef A k ) ? ( MinSUP.asm sup1) supu=u : supf1 (supf1 z1) ≡ supf1 z1 supu=u = ? csupf2 | tri> ¬a ¬b c | record { eq = eq1 } = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x) record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where -- supf1 z1 ≡ sp1, px o< z1 + asm : odef A (supf1 z1) + asm = subst (λ k → odef A k ) (sym (sf1=sp1 c)) ( MinSUP.asm sup1) + sp1=px : sp1 ≡ px + sp1=px with trio< sp1 px + ... | tri> ¬a ¬b c = ? + ... | tri≈ ¬a b ¬c = b + ... | tri< a ¬b ¬c = ? supu=u : supf1 (supf1 z1) ≡ supf1 z1 supu=u = ?