Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/zorn.agda @ 891:9fb948dac666
u < supf z
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 05 Oct 2022 13:13:35 +0900 |
| parents | 3eaf3b8b1009 |
| children | f331c8be2425 |
line wrap: on
line diff
--- a/src/zorn.agda Tue Oct 04 10:46:22 2022 +0900 +++ b/src/zorn.agda Wed Oct 05 13:13:35 2022 +0900 @@ -395,10 +395,11 @@ asupf : {x : Ordinal } → odef A (supf x) supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y supf-< : {x y : Ordinal } → supf x o< supf y → supf x << supf y - x≤supfx : {x : Ordinal } → x o≤ supf z → x o≤ supf x + x≤supfx : {x : Ordinal } → x o≤ z → x o≤ supf x + supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f mf ay supf x) - supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (M→S supf (minsup x≤z) )) + supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z ) csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain chain : HOD @@ -407,8 +408,7 @@ chain⊆A = λ lt → proj1 lt sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x) sup {x} x≤z = M→S supf (minsup x≤z) - supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z ) - supf-is-minsup {x} x≤z = trans (supf-is-sup x≤z) &iso + -- supf-sup<minsup : {x : Ordinal } → (x≤z : x o≤ z) → & (SUP.sup (M→S supf (minsup x≤z) )) o≤ supf x ... supf-mono chain∋init : odef chain y chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ @@ -442,16 +442,16 @@ ... | case2 lt = ⊥-elim ( o<> sx<sy lt ) supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b) - supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) ) + supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-minsup b≤z)) ( MinSUP.asm ( minsup b≤z ) ) -- supf-idem : {x : Ordinal } → supf x o≤ z → supf (supf x) ≡ supf x -- supf-idem {x} sx≤z = sup=u (supf∈A ?) sx≤z ? fcy<sup : {u w : Ordinal } → u o≤ z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf - fcy<sup {u} {w} u≤z fc with SUP.x<sup (sup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) + fcy<sup {u} {w} u≤z fc with MinSUP.x<sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ - ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) )) - ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt ) + ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans ? (sym (supf-is-minsup u≤z ) ) )) + ... | case2 lt = case2 ? -- (subst (λ k → * w < k ) ? )-- (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-minsup u≤z ))) ) lt ) -- ordering is not proved here but in ZChain1 @@ -459,7 +459,7 @@ {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where supf = ZChain.supf zc field - is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< supf z → (ab : odef A b) + is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< z → (ab : odef A b) → HasPrev A (UnionCF A f mf ay supf z) b f ∨ IsSup A (UnionCF A f mf ay supf z) ab → * a < * b → odef ((UnionCF A f mf ay supf z)) b @@ -599,7 +599,7 @@ → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c chain-mono1 {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) a≤b is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → - b o< ZChain.supf zc x → (ab : odef A b) → + b o< x → (ab : odef A b) → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b is-max-hp x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev @@ -641,13 +641,13 @@ ... | ⟪ 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 ≡ SUP.sup (ZChain.sup zc (o<→≤ b<z) )) ∨ ( * z1 < SUP.sup ( ZChain.sup zc (o<→≤ b<z) ) ) - zc00 = SUP.x<sup (ZChain.sup zc (o<→≤ b<z) ) (csupf-fc (o<→≤ b<z) ss<sb fc ) + zc00 : ( z1 ≡ MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1 << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) ) + zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤ b<z) ) ? -- (csupf-fc (o<→≤ b<z) ss<sb fc ) -- supf (supf b) ≡ supf b zc04 : (z1 ≡ supf b) ∨ (z1 << supf b) zc04 with zc00 - ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (ZChain.supf-is-sup zc (o<→≤ b<z)) ) (cong (&) eq) ) - ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (ZChain.supf-is-sup zc (o<→≤ b<z) ) ))) lt ) + ... | case1 eq = ? -- case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (ZChain.supf-is-minsup zc (o<→≤ b<z)) ) (cong (&) eq) ) + ... | case2 lt = ? -- case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) ) ))) lt ) zc1 : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x zc1 x prev with Oprev-p x @@ -656,13 +656,13 @@ zc-b<x : {b : Ordinal } → b o< x → b o< osuc px zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → - b o< ZChain.supf zc x → (ab : odef A b) → + b o< x → (ab : odef A b) → HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab → * a < * b → odef (UnionCF A f mf ay supf x) b 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 b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where b<A : b o< & A b<A = z09 ab m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f @@ -680,17 +680,18 @@ m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = m05 } ... | 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< ZChain.supf zc x → (ab : odef A b) → + b o< x → (ab : odef A b) → HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab → * a < * b → odef (UnionCF A f mf ay supf x) b 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 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 = chain-mono1 ? - ⟪ 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 m10 m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where m09 : b o< & A m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) + m10 : b o< ZChain.supf zc x + m10 = ordtrans<-≤ b<x ( ZChain.x≤supfx zc ? ) m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b @@ -713,16 +714,19 @@ fixpoint f mf zc = z14 where chain = ZChain.chain zc sp1 = sp0 f mf as0 zc - z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< ZChain.supf zc (& A) → (ab : odef A b ) + z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) → HasPrev A chain b f ∨ IsSup A chain {b} ab -- (supO chain (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b ) → * a < * b → odef chain b z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) + z21 : & (SUP.sup sp1) o< & A + z21 = c<→o< ( SUP.as sp1) + -- ZChain.supf zc (& A) o≤ & (SUP.sup sp1) ( minimality ) z11 : & (SUP.sup sp1) o< ZChain.supf zc (& A) z11 = ? -- c<→o< ( SUP.as sp1) z12 : odef chain (& (SUP.sup sp1)) z12 with o≡? (& s) (& (SUP.sup sp1)) ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) - ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z11 (SUP.as sp1) + ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1) (case2 z19 ) z13 where z13 : * (& s) < * (& (SUP.sup sp1)) z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc ) @@ -854,16 +858,16 @@ zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 (supf0 px) a → FClosure A f px b → a <= b zc02 {a} {b} ca fb = zc05 fb where - zc06 : & (SUP.sup (ZChain.sup zc o≤-refl)) ≡ px - zc06 = trans (sym ( ZChain.supf-is-sup zc o≤-refl )) (sym sfpx=px) + zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ px + zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) (sym sfpx=px) zc05 : {b : Ordinal } → FClosure A f px b → a <= b zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc px f mf fb )) ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb) ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) - zc05 (init b1 refl) with SUP.x<sup (ZChain.sup zc o≤-refl) + zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) ? -- (subst (λ k → odef A k ∧ UChain A f mf ay supf0 ? k) (sym &iso) ca ) - ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 (cong (&) eq)) - ... | case2 lt = case2 (subst (λ k → (* a) < k ) (trans (sym *iso) (cong (*) zc06)) lt) + ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 ? )-- (cong (&) eq)) + ... | case2 lt = case2 (subst (λ k → (* a) < k ) ? ? ) -- (trans (sym *iso) (cong (*) zc06)) lt) ptotal : IsTotalOrderSet pchainpx ptotal (case1 a) (case1 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso @@ -1083,7 +1087,7 @@ csupf17 (init as refl ) = ZChain.csupf zc sf<px csupf17 (fsuc x fc) = ? -- ZChain.f-next zc ? -- (csupf17 fc) - x≤supfx1 : {z : Ordinal} → z o≤ supf1 x → z o≤ supf1 z + x≤supfx1 : {z : Ordinal} → z o≤ x → z o≤ supf1 z x≤supfx1 {z} z≤x with trio< z (supf1 z) -- supf1 x o< x → supf1 x o≤ supf1 px → x o< px ∨ supf1 x ≡ supf1 px ... | tri< a ¬b ¬c = o<→≤ a ... | tri≈ ¬a b ¬c = o≤-refl0 b @@ -1249,14 +1253,16 @@ zc13 : odef pchain z zc13 = subst (λ k → odef pchain k) (trans (sym (HasPrev.x=fy hp)) zc14) ( ZChain.f-next zc (HasPrev.ay hp) ) zc20 {.(f w)} (fsuc w fc) = ZChain.f-next zc (zc20 fc) + record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where field - tsup : SUP A (UnionCF A f mf ay supf0 z) - tsup=sup : supf0 z ≡ & (SUP.sup tsup ) + tsup : MinSUP A (UnionCF A f mf ay supf1 z) + tsup=sup : supf1 z ≡ MinSUP.sup tsup + sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x sup {z} z≤x with trio< z px - ... | tri< a ¬b ¬c = record { tsup = ZChain.sup zc (o<→≤ a) ; tsup=sup = ZChain.supf-is-sup zc (o<→≤ a) } - ... | tri≈ ¬a b ¬c = record { tsup = ZChain.sup zc (o≤-refl0 b) ; tsup=sup = ZChain.supf-is-sup zc (o≤-refl0 b) } + ... | tri< a ¬b ¬c = ? -- jrecord { tsup = ZChain.minsup zc (o<→≤ a) ; tsup=sup = ZChain.supf-is-minsup zc (o<→≤ a) } + ... | tri≈ ¬a b ¬c = ? -- record { tsup = ZChain.minsup zc (o≤-refl0 b) ; tsup=sup = ZChain.supf-is-minsup zc (o≤-refl0 b) } ... | tri> ¬a ¬b px<z = zc35 where zc30 : z ≡ x zc30 with osuc-≡< z≤x @@ -1268,16 +1274,16 @@ ... | case1 lt = SUP.x<sup zc32 lt ... | case2 ⟪ spx=px , fc ⟫ = ⊥-elim ( ne spx=px ) zc33 : supf0 z ≡ & (SUP.sup zc32) - zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl ) + zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-minsup zc o≤-refl ) zc36 : ¬ (supf0 px ≡ px) → STMP z≤x - zc36 ne = record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 ne } ; tsup=sup = zc33 } + zc36 ne = ? -- record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 ne } ; tsup=sup = zc33 } zc35 : STMP z≤x zc35 with trio< (supf0 px) px ... | tri< a ¬b ¬c = zc36 ¬b ... | tri> ¬a ¬b c = zc36 ¬b - ... | tri≈ ¬a b ¬c = record { tsup = zc37 ; tsup=sup = ? } where - zc37 : SUP A (UnionCF A f mf ay supf0 z) - zc37 = record { sup = ? ; as = ? ; x<sup = ? } + ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ? } where + zc37 : MinSUP A (UnionCF A f mf ay supf0 z) + zc37 = record { sup = ? ; asm = ? ; x<sup = ? } sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b sup=u {b} ab b≤x is-sup with trio< b px @@ -1380,7 +1386,7 @@ sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup {!!})) sis {z} z≤x with trio< z x ... | tri< a ¬b ¬c = {!!} where - zc8 = ZChain.supf-is-sup (pzc z a) {!!} + zc8 = ZChain.supf-is-minsup (pzc z a) {!!} ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) b f ) → supf1 b ≡ b