Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 559:9ba98ecfbe62
fcn-cmp done
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 30 Apr 2022 04:41:06 +0900 |
parents | fed1c67b9a65 |
children | d09f9a1d6c2f |
comparison
equal
deleted
inserted
replaced
558:fed1c67b9a65 | 559:9ba98ecfbe62 |
---|---|
105 ... | case1 eq = fcn s mf p | 105 ... | case1 eq = fcn s mf p |
106 ... | case2 y<fy = suc (fcn s mf p ) | 106 ... | case2 y<fy = suc (fcn s mf p ) |
107 | 107 |
108 fcn-inject : {A : HOD} (s : Ordinal) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) | 108 fcn-inject : {A : HOD} (s : Ordinal) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) |
109 → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx ≡ fcn s mf cy → * x ≡ * y | 109 → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx ≡ fcn s mf cy → * x ≡ * y |
110 fcn-inject {A} s {x} {y} {f} mf cx cy eq = fc00 (fcn s mf cx) cx cy refl eq where | 110 fcn-inject {A} s {x} {y} {f} mf cx cy eq = fc00 (fcn s mf cx) (fcn s mf cy) eq cx cy refl refl where |
111 fc00 : (i : ℕ ) → {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx → i ≡ fcn s mf cy → * x ≡ * y | 111 fc00 : (i j : ℕ ) → i ≡ j → {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx → j ≡ fcn s mf cy → * x ≡ * y |
112 fc00 zero (init _) (init x₁) i=x i=y = refl | 112 fc00 zero zero refl (init _) (init x₁) i=x i=y = refl |
113 fc00 zero (init sa) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) ) | 113 fc00 zero zero refl (init sa) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) ) |
114 ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero (init sa) cy i=x i=y ) | 114 ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero zero refl (init sa) cy i=x i=y ) |
115 fc00 zero (fsuc x cx) (init sa) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | 115 fc00 zero zero refl (fsuc x cx) (init sa) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) |
116 ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero cx (init sa) i=x i=y ) | 116 ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero zero refl cx (init sa) i=x i=y ) |
117 fc00 zero (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) ) | 117 fc00 zero zero refl (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) ) |
118 ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 zero cx cy i=x i=y ) | 118 ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 zero zero refl cx cy i=x i=y ) |
119 fc00 (suc i) {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) ) | 119 fc00 (suc i) (suc j) i=j {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x j=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) ) |
120 ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 (suc i) cx cy i=x i=y ) | 120 ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 (suc i) (suc j) i=j cx cy i=x j=y ) |
121 ... | case1 x=fx | case2 y<fy = {!!} | 121 ... | case1 x=fx | case2 y<fy = subst (λ k → k ≡ * (f y)) x=fx (fc02 x cx i=x) where |
122 ... | case2 x<fx | case1 y=fy = {!!} | 122 fc02 : (x1 : Ordinal) → (cx1 : FClosure A f s x1 ) → suc i ≡ fcn s mf cx1 → * x1 ≡ * (f y) |
123 ... | case2 x₁ | case2 x₂ = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k))) (fc00 i cx cy (cong pred i=x) (cong pred i=y))) | 123 fc02 .(f x1) (fsuc x1 cx1) i=x1 with proj1 (mf x1 (A∋fc s f mf cx1 ) ) |
124 ... | case1 eq = trans (sym eq) ( fc02 x1 cx1 i=x1 ) | |
125 ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc04) where | |
126 fc04 : * x1 ≡ * y | |
127 fc04 = fc00 i j (cong pred i=j) cx1 cy (cong pred i=x1) (cong pred j=y) | |
128 ... | case2 x<fx | case1 y=fy = subst (λ k → * (f x) ≡ k ) y=fy (fc03 y cy j=y) where | |
129 fc03 : (y1 : Ordinal) → (cy1 : FClosure A f s y1 ) → suc j ≡ fcn s mf cy1 → * (f x) ≡ * y1 | |
130 fc03 .(f y1) (fsuc y1 cy1) j=y1 with proj1 (mf y1 (A∋fc s f mf cy1 ) ) | |
131 ... | case1 eq = trans ( fc03 y1 cy1 j=y1 ) eq | |
132 ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc05) where | |
133 fc05 : * x ≡ * y1 | |
134 fc05 = fc00 i j (cong pred i=j) cx cy1 (cong pred i=x) (cong pred j=y1) | |
135 ... | case2 x₁ | case2 x₂ = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k))) (fc00 i j (cong pred i=j) cx cy (cong pred i=x) (cong pred j=y))) | |
124 | 136 |
125 fcn-< : {A : HOD} (s : Ordinal ) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) | 137 fcn-< : {A : HOD} (s : Ordinal ) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) |
126 → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx Data.Nat.< fcn s mf cy → * x < * y | 138 → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx Data.Nat.< fcn s mf cy → * x < * y |
127 fcn-< {A} s {x} {y} {f} mf cx cy x<y = fc01 (fcn s mf cy) cx cy refl x<y where | 139 fcn-< {A} s {x} {y} {f} mf cx cy x<y = fc01 (fcn s mf cy) cx cy refl x<y where |
128 fc01 : (i : ℕ ) → {y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → (i ≡ fcn s mf cy ) → fcn s mf cx Data.Nat.< i → * x < * y | 140 fc01 : (i : ℕ ) → {y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → (i ≡ fcn s mf cy ) → fcn s mf cx Data.Nat.< i → * x < * y |
135 fc03 : suc i ≡ suc (fcn s mf cy) → i ≡ fcn s mf cy | 147 fc03 : suc i ≡ suc (fcn s mf cy) → i ≡ fcn s mf cy |
136 fc03 eq = cong pred eq | 148 fc03 eq = cong pred eq |
137 fc02 : * x < * y1 | 149 fc02 : * x < * y1 |
138 fc02 = fc01 i cx cy (fc03 i=y ) a | 150 fc02 = fc01 i cx cy (fc03 i=y ) a |
139 | 151 |
140 fcn-cmp : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) (imm : immieate-f A f ) | 152 fcn-cmp : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) |
141 → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x ) | 153 → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x ) |
142 fcn-cmp {A} s {.s} {.s} f mf imm (init x) (init x₁) = tri≈ (λ lt → <-irr (case1 refl) lt ) refl (λ lt → <-irr (case1 refl) lt ) | 154 fcn-cmp {A} s {x} {y} f mf cx cy with <-cmp ( fcn s mf cx ) (fcn s mf cy ) |
143 fcn-cmp {A} s f mf imm (init x) (fsuc y cy) with proj1 (mf y (A∋fc s f mf cy ) ) | 155 ... | tri< a ¬b ¬c = tri< fc11 (λ eq → <-irr (case1 (sym eq)) fc11) (λ lt → <-irr (case2 fc11) lt) where |
144 ... | case1 fy=y = subst (λ k → Tri (* s < * k) (* s ≡ * k) (* k < * s ) ) (*≡*→≡ fy=y) ( fcn-cmp {A} s f mf imm (init x) cy ) | 156 fc11 : * x < * y |
145 ... | case2 fy>y = tri< lt (λ eq → <-irr (case1 (sym eq)) lt ) (λ lt1 → <-irr (case2 lt1) lt ) where | 157 fc11 = fcn-< {A} s {x} {y} {f} mf cx cy a |
146 lt : * s < * (f y) | 158 ... | tri≈ ¬a b ¬c = tri≈ (λ lt → <-irr (case1 (sym fc10)) lt) fc10 (λ lt → <-irr (case1 fc10) lt) where |
147 lt with s≤fc s f mf cy | 159 fc10 : * x ≡ * y |
148 ... | case1 s=y = subst (λ k → * k < * (f y) ) (sym (*≡*→≡ s=y)) fy>y | 160 fc10 = fcn-inject {A} s {x} {y} {f} mf cx cy b |
149 ... | case2 s<y = IsStrictPartialOrder.trans PO s<y fy>y | 161 ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 fc12) lt) (λ eq → <-irr (case1 eq) fc12) fc12 where |
150 fcn-cmp {A} s {x} f mf imm cx (init x₁) with s≤fc s f mf cx | 162 fc12 : * y < * x |
151 ... | case1 eq = tri≈ (λ lt → <-irr (case1 eq) lt) (sym eq) (λ lt → <-irr (case1 (sym eq)) lt) | 163 fc12 = fcn-< {A} s {y} {x} {f} mf cy cx c |
152 ... | case2 s<x = tri> (λ lt → <-irr (case2 s<x) lt) (λ eq → <-irr (case1 eq) s<x ) s<x | 164 |
153 fcn-cmp {A} s f mf imm (fsuc x cx) (fsuc y cy) with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) ) | 165 -- fcn-cmp {A} s {.s} {.s} f mf (init x) (init x₁) = tri≈ (λ lt → <-irr (case1 refl) lt ) refl (λ lt → <-irr (case1 refl) lt ) |
154 ... | case1 x=fx | case1 y=fy = {!!} | 166 -- fcn-cmp {A} s f mf imm (init x) (fsuc y cy) with proj1 (mf y (A∋fc s f mf cy ) ) |
155 ... | case1 x=fx | case2 y<fy = {!!} | 167 -- ... | case1 fy=y = subst (λ k → Tri (* s < * k) (* s ≡ * k) (* k < * s ) ) (*≡*→≡ fy=y) ( fcn-cmp {A} s f mf imm (init x) cy ) |
156 ... | case2 x<fx | case1 y=fy = {!!} | 168 -- ... | case2 fy>y = tri< lt (λ eq → <-irr (case1 (sym eq)) lt ) (λ lt1 → <-irr (case2 lt1) lt ) where |
157 ... | case2 x<fx | case2 y<fy = {!!} where | 169 -- lt : * s < * (f y) |
158 fc-mono : {x y : Ordinal } → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → FClosure A f x y ∨ FClosure A f y x | 170 -- lt with s≤fc s f mf cy |
159 fc-mono = {!!} | 171 -- ... | case1 s=y = subst (λ k → * k < * (f y) ) (sym (*≡*→≡ s=y)) fy>y |
160 fc1 : Tri (* (f x) < * (f y)) (* (f x) ≡ * (f y)) (* (f y) < * (f x)) | 172 -- ... | case2 s<y = IsStrictPartialOrder.trans PO s<y fy>y |
161 fc1 with fcn-cmp s f mf imm cx cy | 173 -- fcn-cmp {A} s {x} f mf imm cx (init x₁) with s≤fc s f mf cx |
162 ... | tri< a ¬b ¬c = {!!} | 174 -- ... | case1 eq = tri≈ (λ lt → <-irr (case1 eq) lt) (sym eq) (λ lt → <-irr (case1 (sym eq)) lt) |
163 ... | tri≈ ¬a b ¬c = {!!} | 175 -- ... | case2 s<x = tri> (λ lt → <-irr (case2 s<x) lt) (λ eq → <-irr (case1 eq) s<x ) s<x |
164 ... | tri> ¬a ¬b c = {!!} | 176 -- fcn-cmp {A} s f mf imm (fsuc x cx) (fsuc y cy) with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) ) |
177 -- ... | case1 x=fx | case1 y=fy = {!!} | |
178 -- ... | case1 x=fx | case2 y<fy = {!!} | |
179 -- ... | case2 x<fx | case1 y=fy = {!!} | |
180 -- ... | case2 x<fx | case2 y<fy = {!!} where | |
181 -- fc-mono : {x y : Ordinal } → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → FClosure A f x y ∨ FClosure A f y x | |
182 -- fc-mono = {!!} | |
183 -- fc1 : Tri (* (f x) < * (f y)) (* (f x) ≡ * (f y)) (* (f y) < * (f x)) | |
184 -- fc1 with fcn-cmp s f mf imm cx cy | |
185 -- ... | tri< a ¬b ¬c = {!!} | |
186 -- ... | tri≈ ¬a b ¬c = {!!} | |
187 -- ... | tri> ¬a ¬b c = {!!} | |
165 | 188 |
166 record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x) ( f : Ordinal → Ordinal ) : Set n where | 189 record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x) ( f : Ordinal → Ordinal ) : Set n where |
167 field | 190 field |
168 y : Ordinal | 191 y : Ordinal |
169 ay : odef B y | 192 ay : odef B y |