Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 863:f5fc3f5f618f
u<=x to u<x
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 09 Sep 2022 20:20:39 +0900 |
| parents | 269467244745 |
| children | 06f692bf7a97 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 54 insertions(+), 52 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Sep 09 08:19:50 2022 +0900 +++ b/src/zorn.agda Fri Sep 09 20:20:39 2022 +0900 @@ -258,7 +258,7 @@ data UChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z - ch-is-sup : (u : Ordinal) {z : Ordinal } (u≤x : u o≤ x) ( is-sup : ChainP A f mf ay supf u ) + ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : u o< x) ( is-sup : ChainP A f mf ay supf u ) ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z -- data UChain is total @@ -414,19 +414,11 @@ zc05 : odef (UnionCF A f mf ay supf b) (supf s) zc05 with zc04 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ - ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 u≤x ) is-sup fc ⟫ where + ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 u<x ) is-sup fc ⟫ where zc06 : supf u ≡ u zc06 = ChainP.supu=u is-sup - zc09 : u o≤ supf s → u o≤ b - zc09 u<s with osuc-≡< (subst (λ k → k o≤ supf s) (sym zc06) u<s) - ... | case1 su=ss = zc08 where - zc07 : supf u o≤ supf b - zc07 = subst (λ k → k o≤ supf b) (sym su=ss) (supf-mono (o<→≤ s<b) ) - zc08 : u o≤ b - zc08 with osuc-≡< zc07 - ... | case1 su=sb = ⊥-elim ( o<¬≡ (trans (sym su=ss) su=sb ) ss<sb ) - ... | case2 lt = o<→≤ (supf-inject lt ) - ... | case2 lt = o<→≤ (ordtrans (supf-inject lt) s<b) + zc09 : u o< supf s → u o< b + zc09 u<s = ordtrans (supf-inject (subst (λ k → k o< supf s) (sym zc06) u<s)) s<b csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where zc04 : odef (UnionCF A f mf ay supf b) (f x) zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc ) @@ -550,7 +542,7 @@ 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 (osucc a≤b )) 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 ) (zc : ZChain A f mf as0 (& A) ) (total : IsTotalOrderSet (ZChain.chain zc) ) → SUP A (ZChain.chain zc) @@ -590,7 +582,7 @@ is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b is-max {a} {b} ua b<x ab P a<b | case2 is-sup - = ⟪ ab , ch-is-sup b (o<→≤ b<x) m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where b<A : b o< & A b<A = z09 ab m04 : ¬ HasPrev A (UnionCF A f mf ay (ZChain.supf zc) b) b f @@ -616,7 +608,7 @@ is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay ) ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl )) ⟫ ... | case2 y<b = chain-mono1 (osucc b<x) - ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc ) m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + ⟪ ab , ch-is-sup b <-osuc m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where m09 : b o< & A m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b @@ -776,33 +768,40 @@ -- if previous chain satisfies maximality, we caan reuse it -- - -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x + -- UninCF supf0 px previous chain u o< px, supf0 px is not included + -- UninCF supf0 x supf0 px is included + -- supf0 px ≡ px + -- supf0 px ≡ supf0 x no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f) → ZChain A f mf ay x no-extension P = record { supf = supf0 ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono ; supf-max = supf-max ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) ; csupf = csupf } where - pchain0=1 : pchain ≡ pchain1 - pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 P } where - zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z - zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1≤x (osucc (pxo<x op))) u1-is-sup fc ⟫ - zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ (HasPrev A pchain x f ) - → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z - zc11 P {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - zc11 P {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ with osuc-≡< u1≤x - ... | case2 lt = ⟪ az , ch-is-sup u1 u1≤px u1-is-sup fc ⟫ where - u1≤px : u1 o≤ px - u1≤px = (subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) lt) - zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ | case1 eq = ⊥-elim (¬sp=x zcsup) where - s1u=x : supf0 u1 ≡ x - s1u=x = trans (ChainP.supu=u u1-is-sup) eq - zc13 : osuc px o< osuc u1 - zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq) ) - x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x) - x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x + zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z + zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ + zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup fc ⟫ + zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ (HasPrev A pchain x f ) + → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( supf0 px ≡ px ) + zc11 P {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ + zc11 P {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ with trio< u1 px + ... | tri< u1<px ¬b ¬c = case1 ⟪ az , ch-is-sup u1 u1<px u1-is-sup fc ⟫ + ... | tri≈ ¬a eq ¬c = case2 (subst (λ k → supf0 k ≡ k) eq s1u=u) where + s1u=u : supf0 u1 ≡ u1 + s1u=u = ChainP.supu=u u1-is-sup + zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = ⊥-elim (¬sp=x zcsup) where + eq : u1 ≡ x + eq with trio< u1 x + ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ ) + ... | tri≈ ¬a b ¬c = b + ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x c ) + s1u=x : supf0 u1 ≡ x + s1u=x = trans (ChainP.supu=u u1-is-sup) eq + zc13 : osuc px o< osuc u1 + zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) ) + x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x) + x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ( ChainP.fcy<sup u1-is-sup {w} fc ) - x<sup {w} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans u≤x zc13 )) - ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 u≤x ) where + x<sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) zc13 )) + ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 (o<→≤ u<x) ) where zc14 : u ≡ osuc px zc14 = begin u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩ @@ -810,13 +809,15 @@ supf0 u1 ≡⟨ s1u=x ⟩ x ≡⟨ sym (Oprev.oprev=x op) ⟩ osuc px ∎ where open ≡-Reasoning - ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ( ChainP.order u1-is-sup lt fc ) - zc12 : supf0 x ≡ u1 - zc12 = subst (λ k → supf0 k ≡ u1) eq (ChainP.supu=u u1-is-sup) - zcsup : xSUP (UnionCF A f mf ay supf0 px) x - zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl) + ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ( ChainP.order u1-is-sup lt fc ) + zc12 : supf0 x ≡ u1 + zc12 = subst (λ k → supf0 k ≡ u1) eq (ChainP.supu=u u1-is-sup) + zcsup : xSUP (UnionCF A f mf ay supf0 px) x + zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl) ; is-sup = record { x<sup = x<sup } } - zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ | case1 eq = zc20 fc where + zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 (zc20 fc ) where + eq : u1 ≡ x + eq = ? zc20 : {z : Ordinal} → FClosure A f (supf0 u1) z → OD.def (od pchain) z zc20 {z} (init asu su=z ) = zc13 where zc14 : x ≡ z @@ -843,8 +844,9 @@ ... | case1 eq = eq ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) zc34 : {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32) - zc34 {w} lt = SUP.x<sup zc32 (subst (λ k → odef k (& w)) (sym pchain0=1) - (subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt )) + zc34 {w} lt = SUP.x<sup zc32 ? where + zc35 : odef (UnionCF A f mf ay supf0 x) (& w) + zc35 = subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt zc33 : supf0 z ≡ & (SUP.sup zc32) zc33 = trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl ) sup=u : {b : Ordinal} (ab : odef A b) → @@ -860,13 +862,13 @@ zcsup : xSUP (UnionCF A f mf ay supf0 px) x zcsup with zc30 ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → - IsSup.x<sup (proj1 is-sup) (subst (λ k → odef k w) pchain0=1 lt) } } + IsSup.x<sup (proj1 is-sup) (zc10 lt)} } zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A (UnionCF A f mf ay supf0 px) x f) → supf0 b ≡ b zc31 (case1 ¬sp=x) with zc30 ... | refl = ⊥-elim (¬sp=x zcsup ) zc31 (case2 hasPrev ) with zc30 - ... | refl = ⊥-elim ( proj2 is-sup (subst (λ k → HasPrev A k x f) pchain0=1 hasPrev ) ) - + ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev + ; ay = zc10 (HasPrev.ay hasPrev) ; x=fy = HasPrev.x=fy hasPrev } ) csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf0 (supf0 b)) (supf0 b) csupf {b} b≤x with zc04 b≤x ... | case2 b=x = subst (λ k → odef (UnionCF A f mf ay supf0 k) k) (ZChain.supf-max zc zc05 ) ( ZChain.csupf zc o≤-refl ) where @@ -1015,15 +1017,15 @@ zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u u≤x ? (init ? ? ) ⟫ zc11 : {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where + zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc13 fc where zc13 : {z : Ordinal} → FClosure A f (supf1 u) z → odef pchain z zc13 (fsuc x fc) with zc13 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ - ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ + ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫ zc13 (init asu su=z ) with trio< u x - ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u u≤x ? (init ? ? ) ⟫ + ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u u<x ? (init ? ? ) ⟫ ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ⊥-elim ( o≤> u≤x c ) + ... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u<x c ) sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) sup {z} z≤x with trio< z x ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup (pzc (osuc z) {!!}) {!!} )