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

comparison src/zorn.agda @ 874:852bdf4a2df3

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 Sat, 17 Sep 2022 10:11:54 +0900
parents 27bab3f65064
children 7f03e1d24961
comparison
equal deleted inserted replaced
873:27bab3f65064 874:852bdf4a2df3
371 sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x) 371 sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x)
372 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z 372 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
373 → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b 373 → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b
374 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) ) 374 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
375 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y 375 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y
376 supf-max : {x : Ordinal } → supf x o≤ supf z
376 supf-< : {x y : Ordinal } → supf x o< supf y → supf x << supf y 377 supf-< : {x y : Ordinal } → supf x o< supf y → supf x << supf y
377 csupf : {b : Ordinal } → supf b o≤ z → odef (UnionCF A f mf ay supf z) (supf b) 378 csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b)
378 chain∋init : odef chain y 379 chain∋init : odef chain y
379 chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ 380 chain∋init = ⟪ ay , ch-init (init ay refl) ⟫
380 f-next : {a : Ordinal} → odef chain a → odef chain (f a) 381 f-next : {a : Ordinal} → odef chain a → odef chain (f a)
381 f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫ 382 f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫
382 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 ) ⟫ 383 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 ) ⟫
418 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 419 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
419 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) 420 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)
420 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 421 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫
421 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) )) 422 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) ))
422 ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt ) 423 ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
424
425 csupf1 : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b)
426 csupf1 {b} sb<z = ⟪ ? , ch-is-sup (supf b) ? record { fcy<sup = fcy<sup ? ; order = ? ; supu=u = ? } (init ? ? ) ⟫
423 427
424 -- ordering is not proved here but in ZChain1 428 -- ordering is not proved here but in ZChain1
425 429
426 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 430 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
427 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where 431 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
538 s<b : s o< b 542 s<b : s o< b
539 s<b = ZChain.supf-inject zc ss<sb 543 s<b = ZChain.supf-inject zc ss<sb
540 s≤<z : s o≤ & A 544 s≤<z : s o≤ & A
541 s≤<z = ordtrans s<b b≤z 545 s≤<z = ordtrans s<b b≤z
542 zc04 : odef (UnionCF A f mf ay supf (& A)) (supf s) 546 zc04 : odef (UnionCF A f mf ay supf (& A)) (supf s)
543 zc04 = ZChain.csupf zc (o<→≤ (z09 (ZChain.asupf zc))) 547 zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc))
544 zc05 : odef (UnionCF A f mf ay supf b) (supf s) 548 zc05 : odef (UnionCF A f mf ay supf b) (supf s)
545 zc05 with zc04 549 zc05 with zc04
546 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 550 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫
547 ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 zc08) is-sup fc ⟫ where 551 ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 zc08) is-sup fc ⟫ where
548 zc07 : FClosure A f (supf u) (supf s) -- supf u ≤ supf s → supf u o≤ supf s 552 zc07 : FClosure A f (supf u) (supf s) -- supf u ≤ supf s → supf u o≤ supf s
814 ... | tri> ¬a ¬b c = sp1 818 ... | tri> ¬a ¬b c = sp1
815 819
816 pchainp : HOD 820 pchainp : HOD
817 pchainp = UnionCF A f mf ay supf1 x 821 pchainp = UnionCF A f mf ay supf1 x
818 822
823 zc16 : {z : Ordinal } → z o< px → supf1 z ≡ supf0 z
824 zc16 {z} z<px with trio< z px
825 ... | tri< a ¬b ¬c = refl
826 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<px )
827 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<px )
828
829 supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w
830 supf-mono1 {z} {w} z≤w with trio< w px
831 ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (zc16 (ordtrans≤-< z≤w a))) refl ( supf-mono z≤w )
832 ... | tri≈ ¬a refl ¬c with osuc-≡< z≤w
833 ... | case1 refl = o≤-refl0 zc17 where
834 zc17 : supf1 px ≡ px
835 zc17 with trio< px px
836 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
837 ... | tri≈ ¬a b ¬c = refl
838 ... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl )
839 ... | case2 lt = subst₂ (λ j k → j o≤ k ) (sym (zc16 lt)) (sym sfpx=px) ( supf-mono z≤w )
840 supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
841 ... | tri< a ¬b ¬c = zc19 where
842 zc19 : supf0 z o≤ sp1
843 zc19 = ?
844 ... | tri≈ ¬a b ¬c = zc18 where
845 zc18 : px o≤ sp1
846 zc18 = ?
847 ... | tri> ¬a ¬b c = o≤-refl
848
819 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchainp) z 849 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchainp) z
820 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 850 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
821 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) ? ? ⟫ 851 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) zc15 zc14 ⟫ where
852 zc14 : FClosure A f (supf1 u1) z
853 zc14 = subst (λ k → FClosure A f k z) (sym (zc16 u1<x)) fc
854 zc15 : ChainP A f mf ay supf1 u1
855 zc15 = record { fcy<sup = λ {z} fcy → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (zc16 u1<x)) (ChainP.fcy<sup u1-is-sup fcy)
856 ; order = λ {s} {z1} lt fc1 → subst (λ k → (z1 ≡ k) ∨ ( z1 << k ) ) (sym (zc16 u1<x)) (
857 ChainP.order u1-is-sup (subst₂ (λ j k → j o< k) (zc17 u1<x lt) (zc16 u1<x) lt) (subst (λ k → FClosure A f k z1) (zc17 u1<x lt) fc1) )
858 ; supu=u = trans (zc16 u1<x) (ChainP.supu=u u1-is-sup) } where
859 zc17 : {s u : Ordinal } → u o< px → supf1 s o< supf1 u → supf1 s ≡ supf0 s
860 zc17 u1<x lt = zc16 (ordtrans ( supf-inject0 supf-mono1 lt) u1<x)
822 861
823 zc11 : {z : Ordinal} → z o< px → OD.def (od pchainp) z → OD.def (od pchain) z 862 zc11 : {z : Ordinal} → z o< px → OD.def (od pchainp) z → OD.def (od pchain) z
824 zc11 {z} z<px ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 863 zc11 {z} z<px ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
825 zc11 {z} z<px ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x ?) ? ? ⟫ 864 zc11 {z} z<px ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x ?) ? ? ⟫
826 865
850 supf1 : Ordinal → Ordinal 889 supf1 : Ordinal → Ordinal
851 supf1 z with trio< z px 890 supf1 z with trio< z px
852 ... | tri< a ¬b ¬c = supf0 z 891 ... | tri< a ¬b ¬c = supf0 z
853 ... | tri≈ ¬a b ¬c = supf0 px 892 ... | tri≈ ¬a b ¬c = supf0 px
854 ... | tri> ¬a ¬b c = supf0 px 893 ... | tri> ¬a ¬b c = supf0 px
894
895 zc16 : {z : Ordinal } → z o< px → supf1 z ≡ supf0 z
896 zc16 {z} z<px with trio< z px
897 ... | tri< a ¬b ¬c = refl
898 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<px )
899 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<px )
900
901 zc17 : {z : Ordinal } → supf0 z o≤ supf0 px
902 zc17 = ? -- px o< z, px o< supf0 px
903
904 supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w
905 supf-mono1 {z} {w} z≤w with trio< w px
906 ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (zc16 (ordtrans≤-< z≤w a))) refl ( supf-mono z≤w )
907 ... | tri≈ ¬a refl ¬c with trio< z px
908 ... | tri< a ¬b ¬c = zc17
909 ... | tri≈ ¬a refl ¬c = o≤-refl
910 ... | tri> ¬a ¬b c = o≤-refl
911 supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
912 ... | tri< a ¬b ¬c = zc17
913 ... | tri≈ ¬a b ¬c = o≤-refl
914 ... | tri> ¬a ¬b c = o≤-refl
855 915
856 pchain1 : HOD 916 pchain1 : HOD
857 pchain1 = UnionCF A f mf ay supf1 x 917 pchain1 = UnionCF A f mf ay supf1 x
858 918
859 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z 919 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z