Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/zorn.agda @ 842:962a9f3dbd3c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Aug 2022 09:49:25 +0900
parents 01361e10ad96
children ef0433f41e55
comparison
equal deleted inserted replaced
841:01361e10ad96 842:962a9f3dbd3c
268 -- 268 --
269 UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) 269 UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
270 ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD 270 ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
271 UnionCF A f mf ay supf x 271 UnionCF A f mf ay supf x
272 = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } 272 = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
273
274 supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y )
275 → supf x o< supf y → x o< y
276 supf-inject0 {x} {y} {supf} supf-mono sx<sy with trio< x y
277 ... | tri< a ¬b ¬c = a
278 ... | tri≈ ¬a refl ¬c = ⊥-elim ( o<¬≡ (cong supf refl) sx<sy )
279 ... | tri> ¬a ¬b y<x with osuc-≡< (supf-mono (o<→≤ y<x) )
280 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
281 ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
273 282
274 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 283 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
275 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where 284 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where
276 field 285 field
277 supf : Ordinal → Ordinal 286 supf : Ordinal → Ordinal
762 -- if previous chain satisfies maximality, we caan reuse it 771 -- if previous chain satisfies maximality, we caan reuse it
763 -- 772 --
764 -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 773 -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x
765 774
766 no-extension : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f → ZChain A f mf ay x 775 no-extension : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f → ZChain A f mf ay x
767 no-extension ¬sp=x = record { supf = supf1 ; sup = sup ; supf-mono = ? 776 no-extension ¬sp=x = record { supf = supf1 ; sup = sup ; supf-mono = supf-mono
768 ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf 777 ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
769 ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = ptotal1 } where 778 ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = ptotal1 } where
779 supf-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b
780 supf-mono = ?
770 pchain0=1 : pchain ≡ pchain1 781 pchain0=1 : pchain ≡ pchain1
771 pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where 782 pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
772 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z 783 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
773 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 784 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
774 zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = zc12 fc where 785 zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = zc12 fc where
775 zc12 : {z : Ordinal} → FClosure A f (supf0 u1) z → odef pchain1 z 786 zc12 : {z : Ordinal} → FClosure A f (supf0 u1) z → odef pchain1 z
776 zc12 (fsuc x fc) with zc12 fc 787 zc12 (fsuc x fc) with zc12 fc
777 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ 788 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫
778 ... | ⟪ 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₁) ⟫ 789 ... | ⟪ 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₁) ⟫
779 zc12 (init asp refl ) with trio< u1 px | inspect supf1 u1 790 zc12 (init asp refl ) with trio< u1 px | inspect supf1 u1
780 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x ? ) 791 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x (o<→≤ px<x) )
781 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup) } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 ) ⟫ where 792 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup) } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 ) ⟫ where
782 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 ) 793 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
783 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc ) 794 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
784 order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 → 795 order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 →
785 (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1) 796 (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
786 order {s} {z2} s<u1 fc with trio< s px 797 order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
787 ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) 798 ... | tri< a ¬b ¬c | _ = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup (subst₂ (λ j k → j o< k) refl eq1 s<u1) fc )
788 ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) 799 ... | tri≈ ¬a b ¬c | _ = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup (subst₂ (λ j k → j o< k) refl eq1 s<u1) fc )
789 ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s ? )) -- px o< s < u1 < px 800 ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans zc14 a) )) where -- px o< s < u1 < px
790 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x ? ) 801 zc14 : s o< u1
802 zc14 = supf-inject0 supf-mono (subst₂ (λ j k → j o< k ) (sym eq2) refl s<u1 )
803 --- s ≡ sp1, px<s = px o< sp1
804 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x (o<→≤ px<x) )
791 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup) } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 ) ⟫ where 805 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup) } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 ) ⟫ where
792 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 ) 806 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
793 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc ) 807 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
794 order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 → 808 order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 →
795 (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1) 809 (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
796 order {s} {z2} s<u1 fc with trio< s px 810 order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
797 ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) 811 ... | tri< a ¬b ¬c | _ = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup (subst₂ (λ j k → j o< k) refl eq1 s<u1) fc )
798 ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) 812 ... | tri≈ ¬a b ¬c | _ = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup (subst₂ (λ j k → j o< k) refl eq1 s<u1) fc )
799 ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b ? ) )) -- px o< s < u1 = px 813 ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b zc14 ) )) where -- px o< s < u1 = px
814 zc14 : s o< u1
815 zc14 = supf-inject0 supf-mono (subst₂ (λ j k → j o< k ) (sym eq2) refl s<u1 )
800 ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< u1≤x 816 ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< u1≤x
801 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) 817 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 )
802 ... | case2 lt = ⊥-elim ( o<> lt px<u1 ) 818 ... | case2 lt = ⊥-elim ( o<> lt px<u1 )
803 819
804 zc11 : {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z 820 zc11 : {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z