Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 794:0acbc2b102e9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 05 Aug 2022 11:09:04 +0900 |
| parents | bcc241fbb390 |
| children | 408e7e8a3797 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 24 insertions(+), 62 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Aug 05 09:22:47 2022 +0900 +++ b/src/zorn.agda Fri Aug 05 11:09:04 2022 +0900 @@ -816,12 +816,13 @@ pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z pzc z z<x = prev z z<x + ysp = & (SUP.sup (ysup f mf ay)) psupf0 : (z : Ordinal) → Ordinal psupf0 z with trio< z x ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z - ... | tri≈ ¬a b ¬c = & A -- Sup of FClosure A f y z ? - ... | tri> ¬a ¬b c = & A -- + ... | tri≈ ¬a b ¬c = ysp + ... | tri> ¬a ¬b c = ysp pchain0 : HOD pchain0 = UnionCF A f mf ay psupf0 x @@ -835,50 +836,13 @@ usup = supP pchain0 (λ lt → proj1 lt) ptotal0 spu = & (SUP.sup usup) - psupf : Ordinal → Ordinal - psupf z with trio< z x + supf1 : Ordinal → Ordinal + supf1 z with trio< z x ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z - ... | tri≈ ¬a b ¬c = spu -- ^^ this z dependcy have to be removed - ... | tri> ¬a ¬b c = spu ---- ∀ z o< x , max (supf (pzc (osuc z) (ob<x lim a))) - - psupf<z : {z : Ordinal } → ( a : z o< x ) → psupf z ≡ ZChain.supf (pzc (osuc z) (ob<x lim a)) z - psupf<z {z} z<x with trio< z x - ... | tri< a ¬b ¬c = cong (λ k → ZChain.supf (pzc (osuc z) (ob<x lim k)) z) ( o<-irr _ _ ) - ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<x) - ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<x) - - psupf=x : spu ≡ psupf x - psupf=x = zc20 refl where - zc20 : {z : Ordinal } → z ≡ x → spu ≡ psupf x - zc20 {z} z=x with trio< z x | inspect psupf z - ... | tri< a ¬b ¬c | _ = ⊥-elim ( ¬b z=x) - ... | tri≈ ¬a b ¬c | record { eq = eq1 } = subst (λ k → spu ≡ psupf k) b (sym eq1) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬b z=x) + ... | tri≈ ¬a b ¬c = spu + ... | tri> ¬a ¬b c = spu - csupf : (z : Ordinal) → odef (UnionCF A f mf ay psupf x) (psupf z) - csupf z with trio< z x | inspect psupf z - ... | tri< z<x ¬b ¬c | record { eq = eq1 } = zc11 where - ozc = pzc (osuc z) (ob<x lim z<x) - zc13 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) z (ZChain.supf ozc z) - zc13 = ZChain.csupf ozc (ordtrans o≤-refl <-osuc ) - zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z) - zc12 = ? - zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z) - zc11 = ⟪ az , ch-is-sup z ? cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az refl) ) ⟫ where - az : odef A ( ZChain.supf ozc z ) - az = proj1 zc12 - zc20 : {z1 : Ordinal} → FClosure A f y z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z) - zc20 {z1} fc with ZChain.fcy<sup ozc <-osuc fc - ... | case1 eq = case1 (trans eq (sym eq1) ) - ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt) - cp1 : ChainP A f mf ay psupf z - cp1 = record { fcy<sup = zc20 ; order = ? ; supu=u = ?} - --- u = supf u = supf z - ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup ? {!!} {!!} {!!} ⟫ where - sa = SUP.A∋maximal usup - ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!} - - fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → (w ≡ psupf u) ∨ (w << psupf u) + fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → (w ≡ supf1 u) ∨ (w << supf1 u) fcy<sup {u} {w} u<x fc with trio< u x ... | tri< a ¬b ¬c = ZChain.fcy<sup uzc <-osuc fc where uzc = pzc (osuc u) (ob<x lim a) @@ -886,25 +850,25 @@ ... | tri> ¬a ¬b c = ⊥-elim (¬a u<x) pchain : HOD - pchain = UnionCF A f mf ay psupf x + pchain = UnionCF A f mf ay supf1 x 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 , ch-init fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-init (fsuc _ fc) ⟫ - pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-is-sup u ? is-sup (fsuc _ fc) ⟫ + pnext {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) ⟫ pinit : {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁ pinit {a} ⟪ aa , ua ⟫ with ua ... | ch-init fc = s≤fc y f mf fc ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc) where - zc7 : y <= psupf _ + zc7 : y <= supf1 _ zc7 = ChainP.fcy<sup is-sup (init ay refl) pcy : odef pchain y pcy = ⟪ ay , ch-init (init ay refl) ⟫ ptotal : IsTotalOrderSet pchain 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 psupf ( (proj2 ca)) ( (proj2 cb)) + uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb)) is-max-hp : (supf : Ordinal → Ordinal) (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → b o< x → (ab : odef A b) → @@ -914,27 +878,25 @@ ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay supf x k ) - (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u ? is-sup (fsuc _ fc)) ⟫ + (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ - no-extension : ZChain A f mf ay x - no-extension = record { initial = pinit ; chain∋init = pcy ; supf = psupf ; sup=u = {!!} - ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } + no-extension : ¬ spu ≡ x → ZChain A f mf ay x + no-extension ¬sp=x = record { initial = pinit ; chain∋init = pcy ; supf = supf1 ; sup=u = {!!} + ; supf-is-sup = ? + ; csupf = ? ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; supf-mono = ? } where + UnionCF⊆ : UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay ? x zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x) - ... | no noax = no-extension -- ¬ A ∋ p, just skip + ... | no noax = no-extension ? -- ¬ A ∋ p, just skip ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f ) -- we have to check adding x preserve is-max ZChain A y f mf x - ... | case1 pr = no-extension + ... | case1 pr = no-extension ? ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax ) - ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!} ; supf = psupf1 ; sup=u = {!!} - ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} } where -- x is a sup of (zc ?) - psupf1 : Ordinal → Ordinal - psupf1 z with trio< z x - ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z - ... | tri≈ ¬a b ¬c = x - ... | tri> ¬a ¬b c = x - ... | case2 ¬x=sup = no-extension -- x is not f y' nor sup of former ZChain from y -- no extention + ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!} ; supf = supf1 ; sup=u = {!!} + ; supf-is-sup = ? + ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = ? ; supf-mono = ? } where -- x is a sup of (zc ?) + ... | case2 ¬x=sup = no-extension ? -- x is not f y' nor sup of former ZChain from y -- no extention SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A) SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) (& A)