Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 781:460df9965d63
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 31 Jul 2022 19:45:40 +0900 |
| parents | 10a036aeb688 |
| children | e8cf9c453431 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 25 insertions(+), 45 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Jul 31 17:57:15 2022 +0900 +++ b/src/zorn.agda Sun Jul 31 19:45:40 2022 +0900 @@ -265,8 +265,6 @@ sup : HOD A∋maximal : A ∋ sup x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup ) -- B is Total, use positive - min-sup : {z : HOD } → B ∋ z → ( {x : HOD } → B ∋ x → (x ≡ z ) ∨ (x < z ) ) - → (z ≡ sup ) ∨ (sup < z ) -- -- sup and its fclosure is in a chain HOD @@ -314,11 +312,6 @@ f-next : {a : Ordinal } → odef chain a → odef chain (f a) f-total : IsTotalOrderSet chain - sup : SUP A chain - supf=sup : supf z ≡ & (SUP.sup sup) - - supf-mono : { a b : Ordinal } → a o< b → supf a o≤ supf b - csupf : (z : Ordinal ) → odef chain (supf z) sup=u : {b : Ordinal} → (ab : odef A b) → b o< z → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b fcy<sup : {u w : Ordinal } → u o< z → FClosure A f init w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf order : {b sup1 z1 : Ordinal} → b o< z → supf sup1 o< supf b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) @@ -724,16 +717,11 @@ supf0 = ZChain.supf zc - csupf : (z : Ordinal) → odef (UnionCF A f mf ay supf0 x) (supf0 z) - csupf z with ZChain.csupf zc z - ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , ch-is-sup u is-sup fc ⟫ - -- if previous chain satisfies maximality, we caan reuse it -- no-extension : ZChain A f mf ay x no-extension = record { supf = supf0 - ; initial = pinit ; chain∋init = pcy ; csupf = csupf ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!} ; supf-mono = ZChain.supf-mono zc + ; initial = pinit ; chain∋init = pcy ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!} ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } zc4 : ZChain A f mf ay x @@ -799,38 +787,30 @@ order : {b sup1 z1 : Ordinal} → b o< x → psupf sup1 o< psupf b → FClosure A f (psupf sup1) z1 → (z1 ≡ psupf b) ∨ (z1 << psupf b) - order {b} {s} {z1} b<x ps<pb fc = ? where - bzc = pzc (osuc b) (ob<x lim b<x) - Sb : SUP A ? - Sb = ZChain.sup bzc - sb = & (SUP.sup (ZChain.sup bzc)) - zc21 : ZChain.supf bzc (osuc b) ≡ sb - zc21 = ZChain.supf=sup bzc - zc22 : {z : HOD} → UnionCF A f mf ay (ZChain.supf bzc) (osuc b) ∋ z - → (z ≡ SUP.sup (ZChain.sup bzc)) ∨ (z < SUP.sup (ZChain.sup bzc)) - zc22 = SUP.x<sup (ZChain.sup bzc) - zc23 = SUP.min-sup (ZChain.sup bzc) + order {b} {s} {z1} b<x ps<pb fc with trio< b x + ... | tri< a ¬b ¬c = ZChain.order uzc <-osuc zc21 zc20 where + uzc = pzc (osuc b) (ob<x lim a) + zc22 : psupf s ≡ ZChain.supf uzc s + zc22 with trio< s x + ... | tri< s<x ¬b ¬c = zc23 where + szc = pzc (osuc s) (ob<x lim s<x) + zc23 : ZChain.supf (pzc (osuc s) (ob<x lim s<x)) s ≡ ZChain.supf (pzc (osuc b) (ob<x lim a)) s + zc23 = ? + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c = ? + zc21 : ZChain.supf uzc s o< ZChain.supf uzc b + zc21 = subst (λ k → k o< _) zc22 ps<pb + zc20 : FClosure A f (ZChain.supf uzc s ) z1 + zc20 = subst (λ k → FClosure A f k z1) zc22 fc + ... | tri≈ ¬a b ¬c = ⊥-elim (¬a b<x) + ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x) - 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) - zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z) - zc12 = ZChain.csupf ozc z - 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) ) ⟫ 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 (ZChain.supf ozc z) - cp1 = record { fcy<sup = zc20 ; order = order z<x } - --- 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} 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) + ... | tri≈ ¬a b ¬c = ⊥-elim (¬a u<x) + ... | tri> ¬a ¬b c = ⊥-elim (¬a u<x) pchain : HOD pchain = UnionCF A f mf ay psupf x @@ -864,7 +844,7 @@ (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u (ChainP-next A f mf ay _ is-sup) (fsuc _ fc)) ⟫ no-extension : ZChain A f mf ay x - no-extension = record { initial = pinit ; chain∋init = pcy ; supf = psupf ; csupf = csupf ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!} + no-extension = record { initial = pinit ; chain∋init = pcy ; supf = psupf ; sup=u = {!!} ; order = order ; fcy<sup = fcy<sup ; supf-mono = {!!} ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x)