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

comparison src/ODUtil.agda @ 1096:55ab5de1ae02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
recovery
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2022 12:54:05 +0900
parents ef5dde91fa80
children c90eec304cfa
comparison
equal deleted inserted replaced
1095:08b6aa6870d9 1096:55ab5de1ae02
24 open OD O 24 open OD O
25 open OD.OD 25 open OD.OD
26 open ODAxiom odAxiom 26 open ODAxiom odAxiom
27 27
28 open HOD 28 open HOD
29 open _⊆_
30 open _∧_ 29 open _∧_
31 open _==_ 30 open _==_
32 31
33 cseq : HOD → HOD 32 cseq : HOD → HOD
34 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where 33 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
56 lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡) 55 lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
57 lemmab1 : & (x , x) o< next ( odmax (x , x)) 56 lemmab1 : & (x , x) o< next ( odmax (x , x))
58 lemmab1 = ho< 57 lemmab1 = ho<
59 58
60 trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C 59 trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
61 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) } 60 trans-⊆ A⊆B B⊆C ab = B⊆C (A⊆B ab)
62 61
63 refl-⊆ : {A : HOD} → A ⊆ A 62 refl-⊆ : {A : HOD} → A ⊆ A
64 refl-⊆ {A} = record { incl = λ x → x } 63 refl-⊆ x = x
65 64
66 od⊆→o≤ : {x y : HOD } → x ⊆ y → & x o< osuc (& y) 65 od⊆→o≤ : {x y : HOD } → x ⊆ y → & x o< osuc (& y)
67 od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) &iso (incl lt (d→∋ x x>z))) 66 od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) &iso (lt (d→∋ x x>z)))
68 67
69 ⊆→= : {F U : HOD} → F ⊆ U → U ⊆ F → F =h= U 68 ⊆→= : {F U : HOD} → F ⊆ U → U ⊆ F → F =h= U
70 ⊆→= {F} {U} FU UF = record { eq→ = λ {x} lt → subst (λ k → odef U k) &iso (incl FU (subst (λ k → odef F k) (sym &iso) lt) ) 69 ⊆→= {F} {U} FU UF = record { eq→ = λ {x} lt → subst (λ k → odef U k) &iso (FU (subst (λ k → odef F k) (sym &iso) lt) )
71 ; eq← = λ {x} lt → subst (λ k → odef F k) &iso (incl UF (subst (λ k → odef U k) (sym &iso) lt) ) } 70 ; eq← = λ {x} lt → subst (λ k → odef F k) &iso (UF (subst (λ k → odef U k) (sym &iso) lt) ) }
72 71
73 ¬A∋x→A≡od∅ : (A : HOD) → {x : HOD} → A ∋ x → ¬ ( & A ≡ o∅ ) 72 ¬A∋x→A≡od∅ : (A : HOD) → {x : HOD} → A ∋ x → ¬ ( & A ≡ o∅ )
74 ¬A∋x→A≡od∅ A {x} ax a=0 = ¬x<0 ( subst (λ k → & x o< k) a=0 (c<→o< ax )) 73 ¬A∋x→A≡od∅ A {x} ax a=0 = ¬x<0 ( subst (λ k → & x o< k) a=0 (c<→o< ax ))
75 74
76 subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → (A ∩ x ) ∋ y ) ⇔ ( x ⊆ A ) 75 subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → (A ∩ x ) ∋ y ) ⇔ ( x ⊆ A )
77 subset-lemma {A} {x} = record { 76 subset-lemma {A} {x} = record {
78 proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) } 77 proj1 = λ lt x∋z → subst (λ k → odef A k ) &iso ( proj1 (lt (subst (λ k → odef x k) (sym &iso) x∋z ) ))
79 ; proj2 = λ x⊆A lt → ⟪ incl x⊆A lt , lt ⟫ 78 ; proj2 = λ x⊆A lt → ⟪ x⊆A lt , lt ⟫
80 } 79 }
81 80
82 ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅ 81 ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
83 ω<next-o∅ {y} lt = <odmax infinite lt 82 ω<next-o∅ {y} lt = <odmax infinite lt
84 83
107 106
108 single : {x y : HOD } → (x , x ) ∋ y → x ≡ y 107 single : {x y : HOD } → (x , x ) ∋ y → x ≡ y
109 single (case1 eq) = ==→o≡ ( ord→== (sym eq) ) 108 single (case1 eq) = ==→o≡ ( ord→== (sym eq) )
110 single (case2 eq) = ==→o≡ ( ord→== (sym eq) ) 109 single (case2 eq) = ==→o≡ ( ord→== (sym eq) )
111 110
111 single& : {x y : Ordinal } → odef (* x , * x ) y → x ≡ y
112 single& (case1 eq) = sym (trans eq &iso)
113 single& (case2 eq) = sym (trans eq &iso)
114
112 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 115 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
113 -- postulate f-extensionality : { n m : Level} → HE.Extensionality n m 116 -- postulate f-extensionality : { n m : Level} → HE.Extensionality n m
114 117
118 pair=∨ : {a b c : Ordinal } → odef (* a , * b) c → ( a ≡ c ) ∨ ( b ≡ c )
119 pair=∨ {a} {b} {c} (case1 c=a) = case1 ( sym (trans c=a &iso))
120 pair=∨ {a} {b} {c} (case2 c=b) = case2 ( sym (trans c=b &iso))
121
115 ω-prev-eq1 : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y) 122 ω-prev-eq1 : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y)
116 ω-prev-eq1 {x} {y} eq x<y = eq→ (ord→== eq) {& (* y)} (λ not2 → not2 (& (* y , * y)) 123 ω-prev-eq1 {x} {y} eq x<y with eq→ (ord→== eq) record { owner = & (* y , * y) ; ao = case2 refl
117 ⟪ case2 refl , subst (λ k → odef k (& (* y))) (sym *iso) (case1 refl)⟫ ) (λ u → lemma u ) where 124 ; ox = subst (λ k → odef k (& (* y))) (sym *iso) (case1 refl) } -- (* x , (* x , * x)) ∋ * y
118 lemma : (u : Ordinal) → ¬ def (od (* x , (* x , * x))) u ∧ def (od (* u)) (& (* y)) 125 ... | record { owner = u ; ao = xxx∋u ; ox = uy } with xxx∋u
119 lemma u t with proj1 t 126 ... | case1 u=x = ⊥-elim ( o<> x<y (osucprev (begin
120 lemma u t | case1 u=x = o<> (c<→o< {* y} {* u} (proj2 t)) (subst₂ (λ j k → j o< k ) 127 osuc y ≡⟨ sym (cong osuc &iso) ⟩
121 (trans (sym &iso) (trans (sym u=x) (sym &iso)) ) (sym &iso) x<y ) -- x ≡ & (* u) 128 osuc (& (* y)) ≤⟨ osucc (c<→o< {* y} {* u} uy) ⟩ -- * x ≡ * u ∋ * y
122 lemma u t | case2 u=xx = o<¬≡ (lemma1 (subst (λ k → odef k (& (* y)) ) (trans (cong (λ k → * k ) u=xx) *iso ) (proj2 t))) x<y where 129 & (* u) ≡⟨ &iso ⟩
123 lemma1 : {x y : Ordinal } → (* x , * x ) ∋ * y → x ≡ y -- y = x ∈ ( x , x ) = u 130 u ≡⟨ u=x ⟩
124 lemma1 (case1 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq) 131 & (* x) ≡⟨ &iso ⟩
125 lemma1 (case2 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq) 132 x ∎ ))) where open o≤-Reasoning O
133 ... | case2 u=xx = ⊥-elim (o<¬≡ ( begin
134 x ≡⟨ single& (subst₂ (λ j k → odef j k ) (begin
135 * u ≡⟨ cong (*) u=xx ⟩
136 * (& (* x , * x)) ≡⟨ *iso ⟩
137 (* x , * x ) ∎ ) &iso uy ) ⟩ -- (* x , * x ) ∋ * y
138 y ∎ ) x<y) where open ≡-Reasoning
126 139
127 ω-prev-eq : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → x ≡ y 140 ω-prev-eq : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → x ≡ y
128 ω-prev-eq {x} {y} eq with trio< x y 141 ω-prev-eq {x} {y} eq with trio< x y
129 ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a) 142 ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a)
130 ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b 143 ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b
131 ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c) 144 ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)
132 145
133 ω-∈s : (x : HOD) → Union ( x , (x , x)) ∋ x 146 ω-∈s : (x : HOD) → Union ( x , (x , x)) ∋ x
134 ω-∈s x not = not (& (x , x)) ⟪ case2 refl , subst (λ k → odef k (& x) ) (sym *iso) (case1 refl) ⟫ 147 ω-∈s x = record { owner = & ( x , x ) ; ao = case2 refl ; ox = subst₂ (λ j k → odef j k ) (sym *iso) refl (case2 refl) }
135 148
136 ωs≠0 : (x : HOD) → ¬ ( Union ( x , (x , x)) ≡ od∅ ) 149 ωs≠0 : (x : HOD) → ¬ ( Union ( x , (x , x)) ≡ od∅ )
137 ωs≠0 y eq = ⊥-elim ( ¬x<0 (subst (λ k → & y o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) ) 150 ωs≠0 y eq = ⊥-elim ( ¬x<0 (subst (λ k → & y o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) )
138 151
139 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i 152 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
152 ≡⟨ trans ( sym *iso) ox=x ⟩ 165 ≡⟨ trans ( sym *iso) ox=x ⟩
153 x 166 x
154 ∎ where 167 ∎ where
155 open ≡-Reasoning 168 open ≡-Reasoning
156 lemma0 : x ∋ * x₁ 169 lemma0 : x ∋ * x₁
157 lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) (λ not → not 170 lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x)
158 (& (* x₁ , * x₁)) ⟪ pair2 , subst (λ k → odef k (& (* x₁))) (sym *iso) pair1 ⟫ ) 171 record { owner = & ( * x₁ , * x₁ ) ; ao = case2 refl ; ox = subst (λ k → odef k (& (* x₁))) (sym *iso) (case1 refl) }
159 lemma1 : infinite ∋ * x₁ 172 lemma1 : infinite ∋ * x₁
160 lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd 173 lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd
161 lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1 174 lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
162 lemma3 iφ iφ refl = HE.refl 175 lemma3 iφ iφ refl = HE.refl
163 lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) ))) 176 lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) )))