Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 712:92275389e623
fix is-max
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 15 Jul 2022 07:44:50 +0900 |
| parents | b1d468186e68 |
| children | 55e82405ec0d |
| files | src/OrdUtil.agda src/zorn.agda |
| diffstat | 2 files changed, 27 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/src/OrdUtil.agda Fri Jul 15 05:52:23 2022 +0900 +++ b/src/OrdUtil.agda Fri Jul 15 07:44:50 2022 +0900 @@ -40,6 +40,13 @@ osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x +open _∧_ + +¬p<x<op : { p b : Ordinal } → ¬ ( (p o< b ) ∧ (b o< osuc p ) ) +¬p<x<op {p} {b} P with osuc-≡< (proj2 P) +... | case1 eq = o<¬≡ (sym eq) (proj1 P) +... | case2 lt = o<> lt (proj1 P) + osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox osucc {ox} {oy} oy<ox with trio< (osuc oy) ox osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
--- a/src/zorn.agda Fri Jul 15 05:52:23 2022 +0900 +++ b/src/zorn.agda Fri Jul 15 07:44:50 2022 +0900 @@ -42,12 +42,10 @@ import ODC - open _∧_ open _∨_ open Bool - open HOD -- @@ -290,7 +288,7 @@ initial : {y : Ordinal } → odef chain y → * init ≤ * y f-next : {a : Ordinal } → odef chain a → odef chain (f a) f-total : IsTotalOrderSet chain - is-max : {a b : Ordinal } → (ca : odef chain a ) → b o< osuc z → (ab : odef A b) + is-max : {a b : Ordinal } → (ca : odef chain a ) → b o< z → (ab : odef A b) → HasPrev A chain ab f ∨ IsSup A chain ab → * a < * b → odef chain b @@ -414,7 +412,7 @@ fixpoint f mf zc total = z14 where chain = ZChain.chain zc sp1 = sp0 f mf zc total - z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) + z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) → HasPrev A chain ab f ∨ IsSup A chain {b} ab -- (supO chain (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b ) → * a < * b → odef chain b z10 = ZChain.is-max zc @@ -423,7 +421,7 @@ z12 : odef chain (& (SUP.sup sp1)) z12 with o≡? (& s) (& (SUP.sup sp1)) ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) - ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) (ordtrans z11 <-osuc ) (SUP.A∋maximal sp1) + ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z11 (SUP.A∋maximal sp1) (case2 z19 ) z13 where z13 : * (& s) < * (& (SUP.sup sp1)) z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc ) @@ -488,7 +486,7 @@ uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) uz01 = chain-total A f mf ay isupf (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) imax : {a b : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → - b o< osuc o∅ → (ab : odef A b) → + b o< o∅ → (ab : odef A b) → HasPrev A (UnionCF A f mf ay isupf o∅) ab f ∨ IsSup A (UnionCF A f mf ay isupf o∅) ab → * a < * b → odef (UnionCF A f mf ay isupf o∅) b imax {a} {b} ua b<ox ab (case1 hasp) a<b = subst (λ k → odef (UnionCF A f mf ay isupf o∅) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) ) @@ -544,7 +542,7 @@ -- if previous chain satisfies maximality, we caan reuse it -- - no-extenion : ( {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) → + no-extenion : ( {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → HasPrev A pchain ab f ∨ IsSup A pchain ab → * a < * b → odef pchain b ) → ZChain A f mf ay x no-extenion is-max = record { initial = pinit ; chain∋init = pcy @@ -552,11 +550,11 @@ zcp : {a b : Ordinal} → odef pchain a → pchain ≡ UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) - → b o< x → (ab : odef A b) + → b o< px → (ab : odef A b) → HasPrev A pchain ab f ∨ IsSup A pchain ab → * a < * b → odef pchain b zcp {a} {b} za cheq b<x ab P a<b = subst (λ k → odef k b ) (sym cheq) ( - ZChain.is-max zc (subst (λ k → odef k a) cheq za) (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x) ab + ZChain.is-max zc (subst (λ k → odef k a) cheq za) b<x ab (subst (λ k → HasPrev A k ab f ∨ IsSup A k ab ) cheq P) a<b ) chain-mono : UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) ⊆' pchain @@ -573,12 +571,12 @@ zc4 : ZChain A f mf ay x zc4 with ODC.∋-p O A (* x) ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip - zc1 : {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) → + zc1 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → HasPrev A pchain ab f ∨ IsSup A pchain ab → * a < * b → odef pchain b - zc1 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox + zc1 {a} {b} za b<ox ab P a<b with osuc-≡< ? ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) ) - ... | case2 lt = zcp za (chain-≡ zc10) lt ab P a<b where + ... | case2 lt = zcp za (chain-≡ zc10) ? ab P a<b where zc10 : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op) zc10 {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ @@ -589,11 +587,11 @@ ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f ) -- we have to check adding x preserve is-max ZChain A y f mf x ... | case1 pr = no-extenion ? where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next - zc7 : {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) → + zc7 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → HasPrev A pchain ab f ∨ IsSup A pchain ab → * a < * b → odef pchain b - zc7 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox - ... | case2 lt = zcp za ? lt ab P a<b + zc7 {a} {b} za b<ox ab P a<b with osuc-≡< ? + ... | case2 lt = zcp za ? ? ab P a<b ... | case1 b=x = ? -- subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr)) ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax ) @@ -601,18 +599,18 @@ record { chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; initial = pinit ; chain∋init = pcy ; is-max = p-ismax } where p-ismax : {a b : Ordinal} → odef pchain a → - b o< osuc x → (ab : odef A b) → + b o< 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 = ? p-ismax {a} {b} ua b<ox ab (case2 sup) a<b = ? ... | case2 ¬x=sup = no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention - z18 : {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) → + z18 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → HasPrev A pchain ab f ∨ IsSup A pchain ab → * a < * b → odef pchain b - z18 {a} {b} za b<x ab P a<b with osuc-≡< b<x - ... | case2 lt = zcp za ? lt ab P a<b + z18 {a} {b} za b<x ab P a<b with osuc-≡< ? + ... | case2 lt = zcp za ? ? ab P a<b ... | case1 b=x with P ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) ) ... | case2 b=sup = ⊥-elim ( ¬x=sup record { @@ -652,7 +650,7 @@ pcy : odef pchain y pcy = ⟪ ay , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay) } ⟫ - no-extenion : ( {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) → + no-extenion : ( {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → HasPrev A pchain ab f ∨ IsSup A pchain ab → * a < * b → odef pchain b ) → ZChain A f mf ay x no-extenion is-max = record { initial = pinit ; chain∋init = pcy @@ -702,10 +700,10 @@ ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain 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 - z18 : {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) → + z18 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → HasPrev A pchain ab f ∨ IsSup A pchain ab → * a < * b → odef pchain b - z18 {a} {b} za b<x ab P a<b with osuc-≡< b<x + z18 {a} {b} za b<x ab P a<b with osuc-≡< ? ... | case2 lt = zcp za ? lt ab P a<b ... | case1 b=x with P ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )