Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/zorn.agda @ 938:93a49ffa9183
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 28 Oct 2022 18:37:05 +0900 |
| parents | 3a511519bd10 |
| children | 187594116449 |
line wrap: on
line diff
--- a/src/zorn.agda Mon Oct 24 19:11:19 2022 +0900 +++ b/src/zorn.agda Fri Oct 28 18:37:05 2022 +0900 @@ -278,7 +278,7 @@ chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a) ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb - ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) with ChainP.fcy<sup supb fca + ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) with ChainP.fcy<sup supb fca ... | case1 eq with s≤fc (supf ub) f mf fcb ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where ct00 : * a ≡ * b @@ -286,14 +286,14 @@ ... | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where ct01 : * a < * b ct01 = subst (λ k → * k < * b ) (sym eq) lt - ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where + ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where ct00 : * a < * (supf ub) ct00 = lt ct01 : * a < * b ct01 with s≤fc (supf ub) f mf fcb ... | case1 eq = subst (λ k → * a < k ) eq ct00 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt - ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb + ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb ... | case1 eq with s≤fc (supf ua) f mf fca ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where ct00 : * a ≡ * b @@ -301,7 +301,7 @@ ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where ct01 : * b < * a ct01 = subst (λ k → * k < * a ) (sym eq) lt - ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where + ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where ct00 : * b < * (supf ua) ct00 = lt ct01 : * b < * a @@ -424,11 +424,11 @@ chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ f-next : {a z : Ordinal} → odef (UnionCF A f mf ay supf z) a → odef (UnionCF A f mf ay supf z) (f a) f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫ - f-next {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫ + f-next {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u<x is-sup (fsuc _ fc ) ⟫ initial : {z : Ordinal } → odef chain z → * y ≤ * z initial {a} ⟪ aa , ua ⟫ with ua ... | ch-init fc = s≤fc y f mf fc - ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc) where + ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc) where zc7 : y <= supf u zc7 = ChainP.fcy<sup is-sup (init ay refl) f-total : IsTotalOrderSet chain @@ -590,8 +590,8 @@ → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ - ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k ) - (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ + ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k ) + (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc)) ⟫ supf = ZChain.supf zc @@ -606,7 +606,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 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 @@ -617,7 +617,7 @@ 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 ) ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ - ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ + ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u<x is-sup (fsuc _ fc) ⟫ order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) order {b} {s} {z1} b<z ss<sb fc = zc04 where zc00 : ( z1 ≡ MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1 << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) ) @@ -889,7 +889,7 @@ 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₁) ⟫ - ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ + ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ zc21 (init asp refl ) with trio< u px | inspect supf1 u ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u ? @@ -928,7 +928,7 @@ zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) 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₁) ⟫ - ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ + ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ zc21 (init asp refl ) with osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x ) ... | case1 sfpx=px = ⟪ asp , ch-is-sup px ? -- (pxo<x op) record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where @@ -956,7 +956,7 @@ ... | case2 sfp<px with ZChain.csupf zc sfp<px -- odef (UnionCF A f mf ay supf0 px) (supf0 px) ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫ - ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u ? + ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u ? record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ ? ) ⟫ where z10 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) (ChainP.fcy<sup is-sup fc) @@ -967,7 +967,7 @@ s<u : s o< u s<u = supf-inject0 supf1-mono lt s≤px : s o≤ px - s≤px = ordtrans s<u ? -- (o<→≤ u≤x) + s≤px = ordtrans s<u ? -- (o<→≤ u<x) lt0 : supf0 s o< supf0 u lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ? ) lt z12 : supf1 u ≡ u @@ -1111,7 +1111,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 @@ -1235,9 +1235,9 @@ * a < * b → odef (UnionCF A f mf ay supf x) b is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ - ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ? -- ⟪ ab , + ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ? -- ⟪ ab , -- subst (λ k → UChain A f mf ay supf x k ) - -- (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ + -- (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc)) ⟫ zc70 : HasPrev A pchain x f → ¬ xSUP pchain x zc70 pr xsup = ? @@ -1251,23 +1251,23 @@ pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } 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 u u≤x is-sup fc ⟫ = zc12 fc where + zc10 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc12 fc where zc12 : {z : Ordinal} → FClosure A f (supf0 u) z → odef pchain1 z zc12 (fsuc x fc) with zc12 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₁) ⟫ 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) {!!}) {!!} ) @@ -1469,20 +1469,38 @@ → supf mc << MinSUP.sup spd sc<<d {mc} {asc} spd = z25 where d1 : Ordinal - d1 = MinSUP.sup spd + d1 = MinSUP.sup spd -- supf d1 ≡ d z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 ) z24 = MinSUP.x<sup spd (init asc refl) - z26 : odef (ZChain.chain zc) (supf mc) - z26 = ? z28 : supf mc o< & A z28 = z09 (ZChain.asupf zc) z25 : supf mc << d1 z25 with z24 ... | case2 lt = lt - ... | case1 eq = ? where + ... | case1 eq = ⊥-elim ( <-irr z29 (proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) ) ) where + -- supf mc ≡ d1 z27 : odef (ZChain.chain zc) (cf nmx d1) z27 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k ) eq (ZChain.csupf zc z28)) - + z31 : {z w : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z + → (* w ≡ * z) ∨ (* w < * z) + → (* w ≡ * d1) ∨ (* w < * d1) + z31 {z} uz (case1 w=z) with MinSUP.x<sup spd uz + ... | case1 eq = case1 (trans w=z (cong (*) eq) ) + ... | case2 lt = case2 (subst (λ k → k < * d1 ) (sym w=z) lt ) + z31 {z} {w} uz (case2 w<z) with MinSUP.x<sup spd uz + ... | case1 eq = case2 (subst (λ k → * w < k ) (cong (*) eq) w<z ) + ... | case2 lt = case2 ( IsStrictPartialOrder.trans PO w<z lt) + z29 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) + z29 with z27 + ... | ⟪ aa , ch-init fc ⟫ = ? where + z30 : FClosure A (cf nmx) (& s) (cf nmx d1) + z30 = fc + ... | ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ with trio< u (supf mc) -- u<x : supf u o< supf (& A) + ... | tri< a ¬b ¬c = ? -- u o< supf mc + ... | tri> ¬a ¬b c = ? -- supf mc o< u + ... | tri≈ ¬a b ¬c with MinSUP.x<sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j k ) (trans (ChainP.supu=u is-sup) b) refl fc ) + ... | case1 eq = case1 (cong (*) eq) + ... | case2 lt = case2 lt sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) ) ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd )