Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1025:e4919cc0cfe8
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 25 Nov 2022 23:39:04 +0900 |
| parents | ab72526316bd |
| children | 8b3d7c461a84 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 99 insertions(+), 18 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Nov 25 18:21:08 2022 +0900 +++ b/src/zorn.agda Fri Nov 25 23:39:04 2022 +0900 @@ -987,7 +987,7 @@ zc41 : ZChain A f mf ay x zc41 with zc43 x sp1 - zc41 | (case2 sp≤x ) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? + zc41 | (case2 sp≤x ) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = ? } where supf1 : Ordinal → Ordinal @@ -1067,21 +1067,62 @@ -- supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x z50 : odef (UnionCF A f mf ay supf1 b) w z50 with osuc-≡< px≤sa - ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 ? (subst (λ k → FClosure A f k w) z52 fc) ⟫ where + ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 cp (subst (λ k → FClosure A f k w) z52 fc) ⟫ where sa≤px : supf0 a o≤ px sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x z51 : supf0 px o< b z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ cong supf0 px=sa ⟩ - supf0 (supf0 a ) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩ - supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ - supf1 a ∎ )) sa<b where open ≡-Reasoning + supf0 (supf0 a ) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩ + supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ + supf1 a ∎ )) sa<b where open ≡-Reasoning z52 : supf1 a ≡ supf1 (supf0 px) z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩ - supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ - supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px) ⟩ - supf1 (supf0 a) ≡⟨ cong supf1 (sym (ZChain.supf-idem zc mf< a≤px sa≤px )) ⟩ - supf1 (supf0 (supf0 a)) ≡⟨ cong (λ k → supf1 (supf0 k)) (sym px=sa) ⟩ - supf1 (supf0 px) ∎ where open ≡-Reasoning + supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ + supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px) ⟩ + supf1 (supf0 a) ≡⟨ cong supf1 (sym (ZChain.supf-idem zc mf< a≤px sa≤px )) ⟩ + supf1 (supf0 (supf0 a)) ≡⟨ cong (λ k → supf1 (supf0 k)) (sym px=sa) ⟩ + supf1 (supf0 px) ∎ where open ≡-Reasoning + m : MinSUP A (UnionCF A f mf ay supf0 px) + m = ZChain.minsup zc o≤-refl + m=spx : MinSUP.sup m ≡ supf1 (supf0 px) + m=spx = begin + MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc o≤-refl) ⟩ + supf0 px ≡⟨ cong supf0 px=sa ⟩ + supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩ + supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ + supf1 a ≡⟨ z52 ⟩ + supf1 (supf0 px) ∎ where open ≡-Reasoning + z53 : supf1 (supf0 px) ≡ supf0 px + z53 = begin + supf1 (supf0 px) ≡⟨ sym z52 ⟩ + supf1 a ≡⟨ sf1=sf0 a≤px ⟩ + supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ + supf0 (supf0 a) ≡⟨ sym ( cong supf0 px=sa ) ⟩ + supf0 px ∎ where open ≡-Reasoning + cp : ChainP A f mf ay supf1 (supf0 px) + cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=spx (MinSUP.x≤sup m ⟪ A∋fc _ f mf fc , ch-init fc ⟫ ) + ; order = order + ; supu=u = z53 } where + uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 + uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<px o≤-refl ss<px (subst (λ k → FClosure A f k z1) + (sf1=sf0 (o<→≤ s<px)) fc ) where + s<px : s o< px + s<px = ZChain.supf-inject zc (osucprev ( begin + osuc (supf0 s) ≡⟨ sym (cong osuc (sf1=sf0 ?) ) ⟩ + osuc (supf1 s) ≤⟨ osucc ss<sp ⟩ + supf1 (supf0 px) ≡⟨ z53 ⟩ + supf0 px ∎ )) where open o≤-Reasoning O + ss<px : supf0 s o< px + ss<px = osucprev ( begin + osuc (supf0 s) ≡⟨ sym (cong osuc (sf1=sf0 ?) ) ⟩ + osuc (supf1 s) ≤⟨ osucc ss<sp ⟩ + supf1 (supf0 px) ≡⟨ sym z52 ⟩ + supf1 a ≡⟨ sf1=sf0 a≤px ⟩ + supf0 a ≡⟨ sym px=sa ⟩ + px ∎ ) where open o≤-Reasoning O + order : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 (supf0 px) → + FClosure A f (supf1 s) z1 → (z1 ≡ supf1 (supf0 px)) ∨ (z1 << supf1 (supf0 px)) + order {s} {z} s<u fc = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=spx (MinSUP.x≤sup m (uz s<u fc) ) ... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) z53 ⟫ ) where z53 : supf1 a o< x z53 = ordtrans<-≤ sa<b b≤x @@ -1089,7 +1130,7 @@ ... | tri< a<px ¬b ¬c = z50 where z50 : odef (UnionCF A f mf ay supf1 b) w z50 with osuc-≡< b≤x - ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) ? fc + ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ ... | ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc u≤px ) ⟫ where -- u o< px → u o< b ? u≤px : u o≤ px @@ -1234,7 +1275,7 @@ ms01 {sup2} us P = MinSUP.minsup m us ? - zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? + zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs } where -- supf0 px not is included by the chain @@ -1258,7 +1299,7 @@ -- a ≡ px → supf px ≡ px → odef U w cfcs0 : a ≡ px → odef (UnionCF A f mf ay supf0 b) w - cfcs0 a=px = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) spx<b ? fc1 ⟫ where + cfcs0 a=px = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) spx<b cp fc1 ⟫ where spx<b : supf0 px o< b spx<b = subst (λ k → supf0 k o< b) a=px sa<b cs01 : supf0 a ≡ supf0 (supf0 px) @@ -1266,6 +1307,27 @@ (subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ spx<b b≤x)))) fc1 : FClosure A f (supf0 (supf0 px)) w fc1 = subst (λ k → FClosure A f k w) cs01 fc + m : MinSUP A (UnionCF A f mf ay supf0 (supf0 px)) + m = ZChain.minsup zc (zc-b<x _ (ordtrans<-≤ spx<b b≤x)) + m=sa : MinSUP.sup m ≡ supf0 (supf0 px) + m=sa = begin + MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc (zc-b<x _ (ordtrans<-≤ spx<b b≤x) )) ⟩ + supf0 (supf0 px) ∎ where open ≡-Reasoning + cp : ChainP A f mf ay supf0 (supf0 px) + cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m ⟪ A∋fc _ f mf fc , ch-init fc ⟫ ) + ; order = order + ; supu=u = sym (trans (cong supf0 (sym a=px)) cs01) } where + uz : {s z1 : Ordinal } → supf0 s o< supf0 (supf0 px) → FClosure A f (supf0 s) z1 + → odef (UnionCF A f mf ay supf0 (supf0 px)) z1 + uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<spx spx≤px + (subst (λ k → supf0 s o< k) (sym (trans (cong supf0 (sym a=px)) cs01) ) ss<sp) fc where + s<spx : s o< supf0 px + s<spx = ZChain.supf-inject zc ss<sp + spx≤px : supf0 px o≤ px + spx≤px = zc-b<x _ (ordtrans<-≤ spx<b b≤x) + order : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 (supf0 px) → + FClosure A f (supf0 s) z1 → (z1 ≡ supf0 (supf0 px)) ∨ (z1 << supf0 (supf0 px)) + order {s} {z} s<u fc = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m (uz s<u fc) ) cfcs1 : odef (UnionCF A f mf ay supf0 b) w @@ -1279,11 +1341,30 @@ ( ZChain.cfcs zc mf< a<px o≤-refl sa<x fc ) ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ sa<x) ⟫ ) ... | tri≈ ¬a sa=px ¬c with trio< a px - ... | tri< a<px ¬b ¬c = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 a) sa<b ? fc1 ⟫ where - cs01 : supf0 a ≡ supf0 (supf0 a) - cs01 = sym ( ZChain.supf-idem zc mf< (zc-b<x _ (ordtrans<-≤ a<b b≤x)) (zc-b<x _ (ordtrans<-≤ sa<b b≤x))) - fc1 : FClosure A f (supf0 (supf0 a)) w - fc1 = subst (λ k → FClosure A f k w) cs01 fc + ... | tri< a<px ¬b ¬c = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 a) sa<b cp fc1 ⟫ where + cs01 : supf0 a ≡ supf0 (supf0 a) + cs01 = sym ( ZChain.supf-idem zc mf< (zc-b<x _ (ordtrans<-≤ a<b b≤x)) (zc-b<x _ (ordtrans<-≤ sa<b b≤x))) + fc1 : FClosure A f (supf0 (supf0 a)) w + fc1 = subst (λ k → FClosure A f k w) cs01 fc + m : MinSUP A (UnionCF A f mf ay supf0 (supf0 a)) + m = ZChain.minsup zc (o≤-refl0 sa=px) + m=sa : MinSUP.sup m ≡ supf0 (supf0 a) + m=sa = begin + MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc (o≤-refl0 sa=px) ) ⟩ + supf0 (supf0 a) ∎ where open ≡-Reasoning + cp : ChainP A f mf ay supf0 (supf0 a) + cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m ⟪ A∋fc _ f mf fc , ch-init fc ⟫ ) + ; order = order + ; supu=u = sym cs01 } where + uz : {s z1 : Ordinal } → supf0 s o< supf0 (supf0 a) → FClosure A f (supf0 s) z1 + → odef (UnionCF A f mf ay supf0 (supf0 a)) z1 + uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< (ZChain.supf-inject zc ss<sp) + (zc-b<x _ (ordtrans<-≤ sa<b b≤x)) ss<sa fc where + ss<sa : supf0 s o< supf0 a + ss<sa = subst (λ k → supf0 s o< k ) (sym cs01) ss<sp + order : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 (supf0 a) → + FClosure A f (supf0 s) z1 → (z1 ≡ supf0 (supf0 a)) ∨ (z1 << supf0 (supf0 a)) + order {s} {z} s<u fc = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m (uz s<u fc) ) ... | tri≈ ¬a a=px ¬c = cfcs0 a=px ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ (ordtrans<-≤ a<b b≤x) ) ⟫ ) ... | tri≈ ¬a a=px ¬c = cfcs0 a=px