Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1071:5463f10d6843
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 13 Dec 2022 19:58:13 +0900 |
| parents | 33d601c9ee96 |
| children | 4ce084a0dce2 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 20 insertions(+), 40 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Dec 13 18:39:15 2022 +0900 +++ b/src/zorn.agda Tue Dec 13 19:58:13 2022 +0900 @@ -348,7 +348,6 @@ asupf : {x : Ordinal } → odef A (supf x) supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y - supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x 0<supfz : {x : Ordinal } → o∅ o< supf x @@ -888,7 +887,7 @@ zc41 : ZChain A f mf< ay x zc41 = record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order ; 0<supfz = 0<supfz - ; zo≤sz = zo≤sz ; supfmax = supfmax ; is-minsup = is-minsup ; cfcs = cfcs } where + ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = cfcs } where supf1 : Ordinal → Ordinal supf1 z with trio< z px @@ -943,20 +942,6 @@ 0<supfz : {x : Ordinal } → o∅ o< supf1 x 0<supfz = ordtrans<-≤ (ZChain.0<supfz zc) (OrdTrans (o≤-refl0 (sym (sf1=sf0 o∅≤z))) (supf1-mono o∅≤z)) - sf≤ : { z : Ordinal } → x o≤ z → supf0 x o≤ supf1 z - sf≤ {z} x≤z with trio< z px - ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) ) - ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x )) - ... | tri> ¬a ¬b c = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl ) (sym (ZChain.supfmax zc px<x))) (sf1=sp1 c) - (supf1-mono (o<→≤ c )) - -- px o<z → supf x ≡ supf0 px ≡ supf1 px o≤ supf1 z - - supfmax : {z : Ordinal } → x o< z → supf1 z ≡ supf1 x - supfmax {z} x<z with trio< z px - ... | tri< a ¬b ¬c = ⊥-elim ( o<> x<z (subst (λ k → z o< k) (Oprev.oprev=x op) (ordtrans a <-osuc) )) - ... | tri≈ ¬a b ¬c = ⊥-elim ( o<> x<z (subst (λ k → k o< x ) (sym b) px<x )) - ... | tri> ¬a ¬b c = sym (sf1=sp1 px<x ) - fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px → FClosure A f (supf1 u) z @@ -1245,13 +1230,13 @@ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = ? ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s ) - ; zo≤sz = ? ; supfmax = λ _ → refl ; is-minsup = ? ; cfcs = ? } where + ; zo≤sz = ? ; is-minsup = ? ; cfcs = ? } where mf : ≤-monotonic-f A f mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where mf00 : * x < * (f x) mf00 = proj1 ( mf< x ax ) ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? ; 0<supfz = ? - ; zo≤sz = ? ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where + ; zo≤sz = ? ; is-minsup = ? ; cfcs = cfcs } where mf : ≤-monotonic-f A f mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where @@ -1406,17 +1391,17 @@ ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x) ... | tri> ¬a ¬b c = ⊥-elim (¬a z<x) - sf1=spu : {z : Ordinal } → (a : x o≤ z ) → spu o< x → supf1 z ≡ spu - sf1=spu {z} x≤z s<x with trio< z x - ... | tri< a ¬b ¬c = ⊥-elim (o≤> x≤z a) + sf1=spu : {z : Ordinal } → x ≡ z → supf1 z ≡ spu + sf1=spu {z} eq with trio< z x + ... | tri< a ¬b ¬c = ⊥-elim (¬b (sym eq)) ... | tri≈ ¬a b ¬c = refl - ... | tri> ¬a ¬b c = ? + ... | tri> ¬a ¬b c = ⊥-elim (¬b (sym eq)) - sf1=sps : {z : Ordinal } → (a : x o≤ z ) → x o≤ spu → supf1 z ≡ sps - sf1=sps {z} x≤z x≤s with trio< z x - ... | tri< a ¬b ¬c = ⊥-elim (o≤> x≤z a) - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ? + sf1=sps : {z : Ordinal } → (a : x o< z ) → supf1 z ≡ sps + sf1=sps {z} x<z with trio< z x + ... | tri< a ¬b ¬c = ⊥-elim (o<> x<z a) + ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x<z ) + ... | tri> ¬a ¬b c = refl zc11 : {z : Ordinal } → odef pchain z → odef pchainS z zc11 {z} lt = ? @@ -1439,27 +1424,22 @@ ... | tri≈ ¬a b ¬c = MinSUP.as usup ... | tri> ¬a ¬b c = MinSUP.as ssup - supfmax : {z : Ordinal } → x o< z → supf1 z ≡ supf1 x - supfmax {z} x<z with trio< z x - ... | tri< a ¬b ¬c = ⊥-elim (o<> a x<z) - ... | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (sym b) x<z) - ... | tri> ¬a ¬b c = sym ? -- (sf1=sps o≤-refl) - supf-mono : {z y : Ordinal } → z o≤ y → supf1 z o≤ supf1 y supf-mono {z} {y} z≤y with trio< y x - ... | tri< y<x ¬b ¬c = ? where + ... | tri< y<x ¬b ¬c = zc01 where open o≤-Reasoning O - zc01 : supf1 z o≤ supf1 y -- ZChain.supf (pzc (ob<x lim y<x)) y + zc01 : supf1 z o≤ ZChain.supf (pzc (ob<x lim y<x)) y zc01 with trio< z x ... | tri< z<x ¬b ¬c = begin ZChain.supf (pzc (ob<x lim z<x)) z ≡⟨ zeq _ _ (osucc z≤y) (o<→≤ <-osuc) ⟩ ZChain.supf (pzc (ob<x lim y<x)) z ≤⟨ ZChain.supf-mono (pzc (ob<x lim y<x)) z≤y ⟩ - ZChain.supf (pzc (ob<x lim y<x)) y ≡⟨ sym (sf1=sf y<x) ⟩ - supf1 y ∎ - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ? + ZChain.supf (pzc (ob<x lim y<x)) y ∎ + ... | tri> ¬a ¬b c = ? -- y<x x o< z → ⊥ + ... | tri≈ ¬a b ¬c with osuc-≡< ( subst (λ k → k o≤ y) b z≤y) + ... | case1 z=y = ? -- x=z=y ⊥ + ... | case2 z<y = subst₂ (λ j k → j o≤ k ) ? refl ( MinSUP.minsup ssup ? ? ) ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ? + ... | tri> ¬a ¬b c = o≤-refl0 ? 0<sufz : {x : Ordinal } → o∅ o< supf1 x 0<sufz = ordtrans<-≤ (ZChain.0<supfz (pzc (ob<x lim 0<x ))) (OrdTrans (o≤-refl0 (sym (sf1=sf 0<x ))) (supf-mono o∅≤z))