Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 952:05f54e16f138
z04 done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 01 Nov 2022 23:16:30 +0900 |
| parents | 86a2bfb7222e |
| children | dfb4f7e9c454 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 51 insertions(+), 27 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Nov 01 11:57:52 2022 +0900 +++ b/src/zorn.agda Tue Nov 01 23:16:30 2022 +0900 @@ -1408,6 +1408,16 @@ ... | case1 eq = ¬b eq ... | case2 lt = ¬a lt + tri : {n : Level} (u w : Ordinal ) { R : Set n } → ( u o< w → R ) → ( u ≡ w → R ) → ( w o< u → R ) → R + tri {_} u w p q r with trio< u w + ... | tri< a ¬b ¬c = p a + ... | tri≈ ¬a b ¬c = q b + ... | tri> ¬a ¬b c = r c + + or : {n m r : Level } {P : Set n } {Q : Set m} {R : Set r} → P ∨ Q → ( P → R ) → (Q → R ) → R + or (case1 p) p→r q→r = p→r p + or (case2 q) p→r q→r = q→r q + -- ZChain contradicts ¬ Maximal -- @@ -1505,7 +1515,12 @@ is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1) is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy )} not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) mc (cf nmx) - not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ? + not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where + z30 : * mc < * (cf nmx mc) + z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) + z31 : ( * (cf nmx mc) ≡ * mc ) ∨ ( * (cf nmx mc) < * mc ) + z31 = <=to≤ ( MinSUP.x≤sup msp1 (subst (λ k → odef (ZChain.chain zc) (cf nmx k)) (sym x=fy) + ⟪ proj2 (cf-is-≤-monotonic nmx _ (proj2 (cf-is-≤-monotonic nmx _ ua1 ) )) , ch-init (fsuc _ (fsuc _ fc)) ⟫ )) not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z48 z32 ) where z30 : * mc < * (cf nmx mc) z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) @@ -1518,23 +1533,44 @@ is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd) is-sup = record { x≤sup = z22 } where - z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd) - z23 lt = MinSUP.x≤sup spd lt - z22 : {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y → + z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd) + z23 lt = MinSUP.x≤sup spd lt + z22 : {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y → (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd) - z22 {a} ⟪ aa , ch-init fc ⟫ = ? - z22 {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ? + z22 {a} ⟪ aa , ch-init fc ⟫ = case2 ( ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) where + z32 : ( a ≡ supf mc ) ∨ ( * a < * (supf mc) ) + z32 = ZChain.fcy<sup zc (o<→≤ mc<A) fc + z22 {a} ⟪ aa , ch-is-sup u u<x is-sup1 fc ⟫ = tri u (supf mc) + z60 z61 ( λ sc<u → ⊥-elim ( o≤> ( subst (λ k → k o≤ supf mc) (ChainP.supu=u is-sup1) z51) sc<u )) where + z53 : supf u o< supf (& A) + z53 = ordtrans<-≤ u<x (ZChain.supf-mono zc (o<→≤ d<A) ) + z52 : ( u ≡ mc ) ∨ ( u << mc ) + z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) + , ch-is-sup u z53 is-sup1 (init (ZChain.asupf zc) (ChainP.supu=u is-sup1)) ⟫ + z56 : u ≡ mc → supf u ≡ supf mc + z56 eq = cong supf eq + z57 : u << mc → supf u o≤ supf mc + z57 lt = ZChain.supf-<= zc (case2 z58) where + z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d + z58 = subst₂ ( λ j k → j << k ) (sym (ChainP.supu=u is-sup1)) (sym sc=c) lt + z51 : supf u o≤ supf mc + z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57 + z60 : u o< supf mc → (a ≡ d ) ∨ ( * a < * d ) + z60 u<smc = case2 ( ftrans<=-< (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A + (subst (λ k → k o< supf mc) (sym (ChainP.supu=u is-sup1)) u<smc) fc ) smc<<d ) + z61 : u ≡ supf mc → (a ≡ d ) ∨ ( * a < * d ) + z61 u=sc = case2 (fsc<<d {mc} asc spd (subst (λ k → FClosure A (cf nmx) k a) (trans (ChainP.supu=u is-sup1) u=sc) fc ) ) -- u<x : ZChain.supf zc u o< ZChain.supf zc d -- supf u o< spuf c → order - z43 : (u w : Ordinal ) → ( u o< w ) ∨ ( u ≡ w ) ∨ ( w o< u ) - z43 u w with trio< u w - ... | tri< a ¬b ¬c = case1 a - ... | tri≈ ¬a b ¬c = case2 (case1 b) - ... | tri> ¬a ¬b c = case2 (case2 c) - not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) d (cf nmx) - not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ? + not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where + z30 : * d < * (cf nmx d) + z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd)) + z32 : ( cf nmx (cf nmx y) ≡ supf mc ) ∨ ( * (cf nmx (cf nmx y)) < * (supf mc) ) + z32 = ZChain.fcy<sup zc (o<→≤ mc<A) (fsuc _ (fsuc _ fc)) + z31 : ( * (cf nmx d) ≡ * d ) ∨ ( * (cf nmx d) < * d ) + z31 = case2 ( subst (λ k → * (cf nmx k) < * d ) (sym x=fy) ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z46 z30 ) where z45 : (* (cf nmx (cf nmx y)) ≡ * d) ∨ (* (cf nmx (cf nmx y)) < * d) → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) z45 p = subst (λ k → (* (cf nmx k) ≡ * d) ∨ (* (cf nmx k) < * d)) (sym x=fy) p @@ -1546,7 +1582,7 @@ z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) , ch-is-sup u z53 is-sup1 (init (ZChain.asupf zc) (ChainP.supu=u is-sup1)) ⟫ z51 : supf u o≤ supf mc - z51 = ? where + z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57 where z56 : u ≡ mc → supf u ≡ supf mc z56 eq = cong supf eq z57 : u << mc → supf u o≤ supf mc @@ -1565,7 +1601,7 @@ z30 : * d < * (cf nmx d) z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd)) z46 : (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) - z46 = ? where + z46 = or (osuc-≡< z51) z55 z54 where z55 : supf u ≡ supf mc → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) z55 eq = <=to≤ (MinSUP.x≤sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j (cf nmx k) ) eq (sym x=fy ) (fsuc _ (fsuc _ fc)) ) ) z54 : supf u o< supf mc → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) @@ -1574,15 +1610,6 @@ -- ... | case1 eq = MinSUP.x≤sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j k ) (trans (ChainP.supu=u is-sup1) eq) refl fc ) -- ... | case2 lt = z45 (case2 (z47 {mc} {d} {asc} spd (z49 lt) z48 )) --- ax : odef A d --- y : Ordinal --- ua1 : odef A y --- u : Ordinal --- u<x : supf u o< supf d --- is-sup1 : ChainP A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf u --- fc : FClosure A (cf nmx) (supf u) y --- x=fy : d ≡ cf nmx y - sd=d : supf d ≡ d sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ @@ -1591,9 +1618,6 @@ ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd ) ... | case2 lt = lt - ¬sms=sa : ¬ ( supf mc ≡ supf (& A)) -- → supf mc ≡ supf d ≡ supf (& A), supf mc << d - ¬sms=sa = ? - sms<sa : supf mc o< supf (& A) sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) )) ... | case2 lt = lt