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

comparison src/zorn.agda @ 849:f1f779930fbf

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 Sun, 04 Sep 2022 14:25:01 +0900
parents 56a150965988
children 2d8ce664ae31
comparison
equal deleted inserted replaced
848:56a150965988 849:f1f779930fbf
772 supf0=1 {z} z≤px with trio< z px 772 supf0=1 {z} z≤px with trio< z px
773 ... | tri< a ¬b ¬c = refl 773 ... | tri< a ¬b ¬c = refl
774 ... | tri≈ ¬a b ¬c = refl 774 ... | tri≈ ¬a b ¬c = refl
775 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c ) 775 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c )
776 776
777 supf1=sp : {z : Ordinal } → x o≤ z → supf1 z ≡ sp1
778 supf1=sp {z} x≤z with trio< z px
779 ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc )))
780 ... | tri≈ ¬a refl ¬c = ⊥-elim ( o≤> x≤z (pxo<x op))
781 ... | tri> ¬a ¬b c = refl
782
777 supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 b) 783 supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 b)
778 supf∈A {b} b≤z = ? 784 supf∈A {b} b≤z = ?
779 785
780 supf1≤sp1 : {a : Ordinal } → supf1 a o≤ sp1 786 supf1≤sp1 : {a : Ordinal } → supf1 a o≤ sp1
781 supf1≤sp1 = ? 787 supf1≤sp1 = ?
961 zcsup : xSUP (UnionCF A f mf ay supf0 px) x 967 zcsup : xSUP (UnionCF A f mf ay supf0 px) x
962 zcsup with zc30 968 zcsup with zc30
963 ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → 969 ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt →
964 IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt) } } 970 IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt) } }
965 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b) 971 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
966 csupf {b} b≤x with osuc-≡< b≤x 972 csupf {b} b≤x = ⟪ zc01 , ch-is-sup u o≤-refl
967 ... | case2 b<x = csupf1 where 973 record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc ⟫ where
968 b≤px : b o≤ px 974 csupf0 : b o≤ px → odef (UnionCF A f mf ay supf0 (supf1 b)) (supf1 b)
969 b≤px = zc-b<x _ b<x 975 csupf0 b≤px = subst (λ k → odef (UnionCF A f mf ay supf0 k) k ) (supf0=1 b≤px) ( ZChain.csupf zc b≤px )
970 csupf0 : odef (UnionCF A f mf ay supf0 (supf1 b)) (supf1 b) 976 zc04 : (b o≤ px ) ∨ (b ≡ x )
971 csupf0 = subst (λ k → odef (UnionCF A f mf ay supf0 k) k ) (supf0=1 b≤px) ( ZChain.csupf zc b≤px ) 977 zc04 with trio< b px
972 csupf1 : odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b) 978 ... | tri< a ¬b ¬c = case1 (o<→≤ a)
973 csupf1 with csupf0 979 ... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b)
974 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 980 ... | tri> ¬a ¬b px<b with osuc-≡< b≤x
975 ... | ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc ⟫ 981 ... | case1 eq = case2 eq
976 with osuc-≡< (subst₂ (λ j k → j o≤ k ) (sym supu=u ) (sym (supf0=1 b≤px)) u≤x) 982 ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
977 ... | case1 eq = ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup1 ; order = order1 ; supu=u = supu=u1 } fc1 ⟫ 983 zc01 : odef A (supf1 b)
978 where 984 zc01 with zc04
979 s0b=s0u : supf0 u ≡ supf0 b -- u ≡ supf0 b 985 ... | case1 le = proj1 ( csupf0 le )
980 s0b=s0u = eq 986 ... | case2 eq = subst (λ k → odef A k ) (sym (supf1=sp (o≤-refl0 (sym eq)))) (SUP.as sup1)
981 u≤sb : u o≤ supf1 b 987 u = supf1 b
982 u≤sb = u≤x 988 supu=u : supf1 u ≡ u
983 supu=u1 : supf1 u ≡ u 989 supu=u with zc04
984 supu=u1 with trio< u px 990 ... | case2 eq = begin
985 ... | tri< a ¬b ¬c = supu=u 991 supf1 u ≡⟨ cong supf1 (supf1=sp ? ) ⟩
986 ... | tri≈ ¬a b ¬c = supu=u 992 supf1 sp1 ≡⟨ supf1=sp ? ⟩
987 ... | tri> ¬a ¬b c = ? -- supf1 b ≡ sp1 , u o≤ sp1, x o≤ u o≤ supf1 b -- u ≡ x → xsup x → ⊥ 993 sp1 ≡⟨ sym (supf1=sp ?) ⟩
988 fc0 : FClosure A f (supf0 u) (supf1 b) 994 u ∎ where open ≡-Reasoning
989 fc0 = fc 995 ... | case1 le = subst (λ k → k ≡ u ) (supf0=1 zc05 ) ( ZChain.sup=u zc zc01 zc05 ? ) where
990 fc1 : FClosure A f (supf1 u) (supf1 b) 996 zc06 : b o≤ px
991 fc1 = ? 997 zc06 = le
992 -- u > x → supf1 u ≡ sp1 → supf1 b o≤ supf1 u 998 zc05 : supf1 b o≤ px
993 -- px o< u o≤ sp1 , spuf1 u o≤ spuf1 sp1 999 zc05 = ?
994 fcy<sup1 : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u) 1000 zc02 : odef A (supf1 u)
995 fcy<sup1 = ? 1001 zc02 = subst (λ k → odef A k ) (sym supu=u) zc01
996 order1 : {s z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1 1002 zc03 : supf1 u ≡ supf1 b
1003 zc03 = ?
1004 fc : FClosure A f (supf1 u) (supf1 b)
1005 fc = init zc02 zc03
1006 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u)
1007 fcy<sup = ?
1008 order : {s z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1
997 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) 1009 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
998 order1 = ?
999 ... | case2 lt = chain-mono f mf ay supf1 b≤sb (UnionCF0⊆1 b≤px zc12 ) where
1000 b≤sb : b o≤ supf1 b -- ≡ supf0 b
1001 b≤sb = ?
1002 lt1 : supf0 u o< supf0 b
1003 lt1 = lt
1004 zc12 : odef (UnionCF A f mf ay supf0 b) (supf1 b)
1005 zc12 = subst (λ k → odef (UnionCF A f mf ay supf0 b) k) &iso ( ZChain.csupf-fc zc b≤px lt fc )
1006 ... | case1 refl = ⟪ supf∈A o≤-refl , ch-is-sup (supf1 x) o≤-refl
1007 record { fcy<sup = fcy<sup ; order = order ; supu=u = zc11 } (init zc10 zc11 ) ⟫ where
1008 zc12 : supf1 x ≡ sp1
1009 zc12 = ?
1010 zc11 : supf1 (supf1 x) ≡ supf1 x
1011 zc11 = ?
1012 zc10 : odef A (supf1 (supf1 x))
1013 zc10 = subst (λ k → odef A k ) (sym zc11) ( supf∈A o≤-refl )
1014 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 (supf1 x)) ∨ (z << supf1 (supf1 x))
1015 fcy<sup = ?
1016 order : {s z1 : Ordinal} → supf1 s o< supf1 (supf1 b) → FClosure A f (supf1 s) z1
1017 → (z1 ≡ supf1 (supf1 b)) ∨ (z1 << supf1 (supf1 b))
1018 order = ? 1010 order = ?
1019 sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x)) 1011 sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x))
1020 sis {z} z≤x = zc40 where 1012 sis {z} z≤x = zc40 where
1021 zc40 : supf1 z ≡ & (SUP.sup (sup z≤x)) -- direct with statment causes error 1013 zc40 : supf1 z ≡ & (SUP.sup (sup z≤x)) -- direct with statment causes error
1022 zc40 with trio< z px | inspect supf1 z | inspect sup z≤x 1014 zc40 with trio< z px | inspect supf1 z | inspect sup z≤x