Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 899:37a09244cebd
UChain u<x to u≤x again
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 07 Oct 2022 08:28:49 +0900 |
| parents | 37ddab37e189 |
| children | ac4daa43ef2a |
| files | src/zorn.agda |
| diffstat | 1 files changed, 21 insertions(+), 33 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Oct 06 18:59:44 2022 +0900 +++ b/src/zorn.agda Fri Oct 07 08:28:49 2022 +0900 @@ -262,7 +262,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 : supf u o< supf x) ( is-sup : ChainP A f mf ay supf u ) + ch-is-sup : (u : Ordinal) {z : Ordinal } (u≤x : supf u o≤ supf 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 -- @@ -576,7 +576,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 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 ) {x y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay x ) → SUP A (ZChain.chain zc) @@ -619,7 +619,7 @@ 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 zc08 is-sup fc ⟫ where + ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (o<→≤ zc08) is-sup fc ⟫ where zc07 : FClosure A f (supf u) (supf s) -- supf u ≤ supf s → supf u o≤ supf s zc07 = fc zc06 : supf u ≡ u @@ -654,16 +654,18 @@ 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 sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + = ⟪ ab , ch-is-sup b sb≤sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where b<A : b o< & A b<A = z09 ab + sb≤sx : supf b o≤ supf x + sb≤sx = ZChain.supf-mono zc (o<→≤ b<x ) m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = - chain-mono1 ? (HasPrev.ay nhp) + chain-mono1 sb≤sx (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) - ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 ? uz) } , m04 ⟫ + ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 sb≤sx uz) } , m04 ⟫ m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b @@ -671,22 +673,6 @@ m09 {s} {z} s<b fcz = order b<A s<b fcz m06 : ChainP A f mf ay supf b m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = m05 } - sb<sx : supf b o< supf x - sb<sx with osuc-≡< ( ZChain.supf-mono zc (o<→≤ b<x ) ) - ... | case2 lt = lt - ... | case1 eq = ⊥-elim ( <-irr (case1 (sym m11)) m12 ) where - --- supf b ≡ supf x * ( supf x ) ≤ * a < * b , * (supf x) ≡ * (supf b) ≡ * b - --- xchain = UnionCF A f mf ay supf x - --- {y : Ordinal} → odef xchain y → (y ≡ b ) ∨ (y < * b ) - --- supf x ∈ xchian → ok - --- ¬ supf x ∈ xchian → ⊥ - m10 : {a : Ordinal} → odef (UnionCF A f mf ay supf x) a → * ( supf x ) ≤ * a - m10 {a} ⟪ ua , ch-init fc ⟫ = ? - m10 {a} ⟪ ua , ch-is-sup u u<x is-sup fc ⟫ = ? - m12 : * ( supf x ) < * b - m12 = ? - m11 : * ( supf x ) ≡ * b - m11 = ? ... | no lim = record { is-max = is-max } where is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → b o< x → (ab : odef A b) → @@ -696,7 +682,9 @@ 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 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 = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + ... | case2 y<b = ⟪ ab , ch-is-sup b sb≤sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + sb≤sx : supf b o≤ supf x + sb≤sx = ZChain.supf-mono zc (o<→≤ b<x ) 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 @@ -706,11 +694,11 @@ m08 {s} {z1} s<b fc = order m09 s<b fc m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = - chain-mono1 ? (HasPrev.ay nhp) + chain-mono1 sb≤sx (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b m05 = ZChain.sup=u zc ab (o<→≤ m09) - ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 ? lt )} , m04 ⟫ -- ZChain on x + ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 sb≤sx lt )} , m04 ⟫ -- ZChain on x m06 : ChainP A f mf ay supf b m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = m05 } @@ -1003,11 +991,11 @@ fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ - zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc21 fc where + zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc21 fc where zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ - ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ + ... | case1 ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ ... | case2 fc = case2 (fsuc _ fc) zc21 (init asp refl ) with trio< u px | inspect supf1 u ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u ? record {fcy<sup = zc13 ; order = zc17 @@ -1026,7 +1014,7 @@ ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ? ⟫ ) zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ - zc12 {z} (case1 ⟪ az , ch-is-sup u u<x is-sup fc ⟫ ) = zc21 fc where + zc12 {z} (case1 ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ ) = zc21 fc where zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef (UnionCF A f mf ay supf1 x) z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ @@ -1040,7 +1028,7 @@ zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 ?)) ( ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ?) ss<spx) (fcup fc s≤px) ) where s≤px : s o≤ px - s≤px = ? -- ordtrans ( supf-inject0 supf-mono1 ss<spx ) (o<→≤ u<x) + s≤px = ? -- ordtrans ( supf-inject0 supf-mono1 ss<spx ) (o<→≤ u≤x) zc14 : FClosure A f (supf1 u) (supf0 u) zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 ?)) asp) (sf1=sf0 ?) zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) @@ -1199,7 +1187,7 @@ 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 ? - x<sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) ? )) + x<sup {w} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u≤x) ? )) ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 ? ) where zc14 : u ≡ osuc px zc14 = begin @@ -1347,15 +1335,15 @@ zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u ? ? (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 ? ? (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) {!!}) {!!} )