Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1013:2362c2d89d36
fc-inject is no good
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 23 Nov 2022 16:12:51 +0900 |
| parents | 6f6daf464616 |
| children | 8025c5d01153 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 47 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Nov 23 09:55:38 2022 +0900 +++ b/src/zorn.agda Wed Nov 23 16:12:51 2022 +0900 @@ -511,6 +511,12 @@ fsp≤sp : f sp <= sp fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00 + supf-¬hp : {x : Ordinal } → x o≤ z + → ( {a : Ordinal } → odef A a → a << f a ) + → ¬ ( HasPrev A (UnionCF A f mf ay supf x) f (supf x) ) + supf-¬hp {x} x≤z <-mono hp = IsMinSUP→NotHasPrev asupf (λ {w} uw → + (subst (λ k → w <= k) (sym (supf-is-minsup x≤z)) ( MinSUP.x≤sup (minsup x≤z) uw) )) <-mono hp + supf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b supf-idem mf< {b} b≤z sfb≤x = z52 where z54 : {w : Ordinal} → odef (UnionCF A f mf ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b) @@ -525,10 +531,19 @@ z52 : supf (supf b) ≡ supf b z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ -spuf-unique : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) + fc-inject : ( {a : Ordinal } → odef A a → a << f a ) + → {x y wx wy : Ordinal} → FClosure A f (supf x) wx → FClosure A f (supf y) wy → wx ≡ wy → supf x ≡ supf y + fc-inject mf< (init xa eqa) (init ya eqb) refl = trans eqa (sym eqb) + fc-inject mf< {x} (init xa eqx) (fsuc ya fcy) eq = ⊥-elim ( supf-¬hp ? mf< record { ax = asupf ; y = ya ; ay = ? ; x=fy = trans eqx eq } ) where + z53 : odef (UnionCF A f mf ay supf x) ya + z53 = cfcs ? ? ? ? fcy + fc-inject mf< (fsuc xa fcx) (init ya eqy) eq = ? + fc-inject mf< (fsuc xa fcx) (fsuc ya fcy) eq = fc-inject mf< fcx fcy ? + +supf-unique : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y xa xb : Ordinal} → (ay : odef A y) → (xa o≤ xb ) → (za : ZChain A f mf ay xa ) (zb : ZChain A f mf ay xb ) → {z : Ordinal } → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z -spuf-unique A f mf {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa where +supf-unique A f mf {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa where supfa = ZChain.supf za supfb = ZChain.supf zb ind : (x : Ordinal) → ((w : Ordinal) → w o< x → w o≤ xa → supfa w ≡ supfb w) → x o≤ xa → supfa x ≡ supfb x @@ -597,6 +612,7 @@ z55 : FClosure A f (ZChain.supf zb u) z z55 = subst (λ k → FClosure A f k z ) (sym ub=ua) fc + UChain⊆ : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {z y : Ordinal} (ay : odef A y) { supf supf1 : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) @@ -1342,7 +1358,7 @@ zeq : {xa xb z : Ordinal } → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa → ZChain.supf (pzc xa<x) z ≡ ZChain.supf (pzc xb<x) z - zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa = spuf-unique A f mf ay xa≤xb + zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa = supf-unique A f mf ay xa≤xb (pzc xa<x) (pzc xb<x) z≤xa ptotalx : IsTotalOrderSet pchainx @@ -1413,20 +1429,41 @@ cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } → a o< b → b o≤ x → supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with trio< a x - ... | tri< a<x ¬b ¬c = ? where + ... | tri< a<x ¬b ¬c = zc40 where sa = ZChain.supf (pzc (ob<x lim a<x)) a m = omax a sa m<x : m o< x m<x with trio< a sa | inspect (omax a) sa ... | tri< a<sa ¬b ¬c | record { eq = eq } = ob<x lim sa<x - ... | tri≈ ¬a b ¬c | record { eq = eq } = subst ( λ k → k o< x ) ( begin - sa ≡⟨ ? ⟩ - ? ≡⟨ sym eq ⟩ - _ ∎ ) ( ob<x lim sa<x ) where open ≡-Reasoning + ... | tri≈ ¬a a=sa ¬c | record { eq = eq } = subst (λ k → k o< x) eq zc41 where + zc41 : omax a sa o< x + zc41 = osucprev ( begin + osuc ( omax a sa ) ≡⟨ cong (λ k → osuc (omax a k)) (sym a=sa) ⟩ + osuc ( omax a a ) ≡⟨ cong osuc (omxx _) ⟩ + osuc ( osuc a ) ≤⟨ o<→≤ (ob<x lim (ob<x lim a<x)) ⟩ + x ∎ ) where open o≤-Reasoning O ... | tri> ¬a ¬b c | record { eq = eq } = ob<x lim a<x + sam = ZChain.supf (pzc (ob<x lim m<x)) a + zc42 : osuc a o≤ osuc m + zc42 = osucc (o<→≤ ( omax-x _ _ ) ) + sam<m : sam o< m + sam<m = subst (λ k → k o< m ) (supf-unique A f mf ay zc42 (pzc (ob<x lim a<x)) (pzc (ob<x lim m<x)) (o<→≤ <-osuc)) ( omax-y _ _ ) + fcm : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) a) w + fcm = subst (λ k → FClosure A f k w ) (zeq (ob<x lim a<x) (ob<x lim m<x) zc42 (o<→≤ <-osuc) ) fc zc40 : odef (UnionCF A f mf ay supf1 b) w - zc40 with ZChain.cfcs (pzc (ob<x lim sa<x)) mf< ? o≤-refl ? ? - ... | t = ? + zc40 with ZChain.cfcs (pzc (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm + ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ + ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<b ? fc2 ⟫ where -- u o< px → u o< b ? + zc55 : u o< osuc m + zc55 = u<x + zc56 : u ≡ supf1 a + zc56 = ? + u<b : u o< b -- b o≤ u → b o≤ a -- u ≡ supf1 a + u<b = ? + fc1m : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) u) w + fc1m = fc1 + fc2 : FClosure A f (supf1 u) w + fc2 = ? ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x)) ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))