Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 700:3de5a1fb8011
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 12 Jul 2022 15:49:49 +0900 |
| parents | 4df0b36db305 |
| children | 29100f14bb97 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 33 insertions(+), 71 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Jul 12 15:42:33 2022 +0900 +++ b/src/zorn.agda Tue Jul 12 15:49:49 2022 +0900 @@ -536,78 +536,40 @@ ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → (zc0 : (x : Ordinal) → ZChain1 A f mf ay x) → ((z : Ordinal) → z o< x → ZChain A f mf ay zc0 z) → ZChain A f mf ay zc0 x - ind f mf {y} ay x zc0 prev with trio< o∅ x - ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c ) - ... | tri≈ ¬a refl ¬c = record { initial = initial1 } where - initial1 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A)) z → * y ≤ * z - initial1 {z} uz = ? where - zc01 : odef A z ∧ UChain A f mf ay (ZChain1.supf (zc0 (& A))) (& A) z - zc01 = uz - ... | tri< 0<x ¬b ¬c with Oprev-p x - ... | yes op = zc4 where - -- - -- we have previous ordinal to use induction - -- - px = Oprev.oprev op - zc : ZChain A f mf ay zc0 (Oprev.oprev op) - zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) - px<x : px o< x - px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc - 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 - - - zc4 : ZChain A f mf ay zc0 x - zc4 = record { chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal + ind f mf {y} ay x zc0 prev = record { chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; initial = pinit ; chain∋init = pcy ; is-max = p-ismax } where - pchain : HOD - pchain = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A) - psupf = ZChain1.supf (zc0 (& A)) - pchain⊆A : {y : Ordinal} → odef pchain y → odef A y - pchain⊆A {y} ny = proj1 ny - pnext : {a : Ordinal} → odef pchain a → odef pchain (f a) - pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; chain∋z = fua } ⟫ where - afa : odef A ( f a ) - afa = proj2 ( mf a aa ) - fua : Chain A f mf ay psupf (UChain.u ua) (f a) - fua with UChain.chain∋z ua - ... | ch-init a fc = ch-init (f a) ( fsuc _ fc ) - ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc) - ptotal : {a b : HOD } → odef pchain (& a) → odef pchain (& b) - → Tri ( a < b) ( a ≡ b) ( b < a ) - ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where - uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) - uz01 = chain-total A f mf ay _ (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) - pinit : {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁ - pinit {a} ⟪ aa , ua ⟫ with UChain.chain∋z ua - ... | ch-init a fc = s≤fc y f mf fc - ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc) where - zc7 : y << psupf (UChain.u ua) - zc7 = ChainP.fcy<sup is-sup (init ay) - pcy : odef pchain y - pcy = ⟪ ay , record { u = y ; u<x = ∈∧P→o< ⟪ ay , lift true ⟫ ; chain∋z = ch-init _ (init ay) } ⟫ - p-ismax : {a b : Ordinal} → odef pchain a → - b o< osuc x → (ab : odef A b) → - ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) → - * a < * b → odef pchain b - p-ismax {a} {b} ua b<ox ab (case1 hasp) a<b = ⟪ ab , ? ⟫ - p-ismax {a} {b} ua b<ox ab (case2 sup) a<b = ⟪ ab , ? ⟫ - - ... | no op = zc5 where - uzc : {z : Ordinal} → (u : UChain A f mf ay (ZChain1.supf (zc0 (& A))) x z ) → ZChain A f mf ay zc0 (UChain.u u) - uzc {z} u = prev (UChain.u u) (UChain.u<x u) - UZ : HOD - UZ = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) x - zc5 : ZChain A f mf ay zc0 x - zc5 with ODC.∋-p O A (* x) - ... | no noax = {!!} where -- ¬ A ∋ p, just skip - ... | yes ax with ODC.p∨¬p O ( HasPrev A UZ ax f ) - -- we have to check adding x preserve is-max ZChain A y f mf zc0 x - ... | case1 pr = {!!} where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next - ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A UZ ax ) - ... | case1 is-sup = {!!} -- x is a sup of (zc ?) - ... | case2 ¬x=sup = {!!} -- no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention - + pchain : HOD + pchain = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A) + psupf = ZChain1.supf (zc0 (& A)) + pchain⊆A : {y : Ordinal} → odef pchain y → odef A y + pchain⊆A {y} ny = proj1 ny + pnext : {a : Ordinal} → odef pchain a → odef pchain (f a) + pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; chain∋z = fua } ⟫ where + afa : odef A ( f a ) + afa = proj2 ( mf a aa ) + fua : Chain A f mf ay psupf (UChain.u ua) (f a) + fua with UChain.chain∋z ua + ... | ch-init a fc = ch-init (f a) ( fsuc _ fc ) + ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc) + ptotal : {a b : HOD } → odef pchain (& a) → odef pchain (& b) + → Tri ( a < b) ( a ≡ b) ( b < a ) + ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where + uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) + uz01 = chain-total A f mf ay _ (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) + pinit : {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁ + pinit {a} ⟪ aa , ua ⟫ with UChain.chain∋z ua + ... | ch-init a fc = s≤fc y f mf fc + ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc) where + zc7 : y << psupf (UChain.u ua) + zc7 = ChainP.fcy<sup is-sup (init ay) + pcy : odef pchain y + pcy = ⟪ ay , record { u = y ; u<x = ∈∧P→o< ⟪ ay , lift true ⟫ ; chain∋z = ch-init _ (init ay) } ⟫ + p-ismax : {a b : Ordinal} → odef pchain a → + b o< osuc x → (ab : odef A b) → + ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) → + * a < * b → odef pchain b + p-ismax {a} {b} ua b<ox ab (case1 hasp) a<b = ⟪ ab , ? ⟫ + p-ismax {a} {b} ua b<ox ab (case2 sup) a<b = ⟪ ab , ? ⟫ SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f mf ay x SZ0 f mf ay x = TransFinite {λ z → ZChain1 A f mf ay z} (sind f mf ay ) x