Changeset 1050 for src/utilities
 Timestamp:
 Jul 4, 2011, 10:43:37 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/HMap.ma
r1049 r1050 170 170 ]. 171 171 172 definition map_single_l_safe ≝ 173 λkey_type. 174 λelt_type. 175 λkey: key_type. 176 λelt: elt_type. 177 λleft: map key_type elt_type. 178 λright: map key_type elt_type. 179 λprf: map_not_nil_p key_type elt_type right. 180 match right return λx. map_not_nil_p key_type elt_type x → map key_type elt_type with 181 [ map_nil ⇒ λright_nil_absrd. ? 182  map_fork r_sz r_key r_elt r_l r_r ⇒ 183 λright_fork_prf. map_binsert ? ? r_key r_elt (map_binsert ? ? key elt left r_l) r_r 184 ] prf. 185 normalize in right_nil_absrd; 186 cases right_nil_absrd 187 qed. 188 172 189 definition map_single_r ≝ 173 190 λkey_type. … … 181 198  map_fork l_sz l_key l_elt l_l l_r ⇒ 182 199 Some ? (map_binsert ? ? l_key l_elt l_l (map_binsert ? ? key elt l_r right)) 200 ]. 201 202 definition map_single_r_safe ≝ 203 λkey_type. 204 λelt_type. 205 λkey: key_type. 206 λelt: elt_type. 207 λleft: map key_type elt_type. 208 λright: map key_type elt_type. 209 λprf: map_not_nil_p key_type elt_type left. 210 match left return λx. map_not_nil_p key_type elt_type x → map key_type elt_type with 211 [ map_nil ⇒ λleft_nil_absrd. ? 212  map_fork l_sz l_key l_elt l_l l_r ⇒ 213 λleft_fork_prf. map_binsert ? ? l_key l_elt l_l (map_binsert ? ? key elt l_r right) 214 ] prf. 215 normalize in left_nil_absrd; 216 cases left_nil_absrd 217 qed. 218 219 definition map_double_r_property_p ≝ 220 λkey_type. 221 λelt_type. 222 λleft: map key_type elt_type. 223 match left with 224 [ map_nil ⇒ False 225  map_fork l_sz l_key l_elt l_l l_r ⇒ 226 match l_r with 227 [ map_nil ⇒ False 228  _ ⇒ True 229 ] 183 230 ]. 184 231 … … 199 246 ] 200 247 ]. 248 249 definition map_double_r_safe ≝ 250 λkey_type. 251 λelt_type. 252 λkey: key_type. 253 λelt: elt_type. 254 λleft: map key_type elt_type. 255 λright: map key_type elt_type. 256 λprf: map_double_r_property_p key_type elt_type left. 257 match left return λx. map_double_r_property_p key_type elt_type x → map key_type elt_type with 258 [ map_nil ⇒ λleft_nil_absrd. ? 259  map_fork l_sz l_key l_elt l_l l_r ⇒ λouter_prf. 260 match l_r return λx. map_double_r_property_p key_type elt_type x → map key_type elt_type with 261 [ map_nil ⇒ λl_r_nil_absrd. ? 262  map_fork lr_sz lr_key lr_elt lr_l lr_r ⇒ 263 λl_r_fork_prf. map_binsert … lr_key lr_elt (map_binsert … l_key l_elt l_l lr_l) (map_binsert … key elt lr_r right) 264 ] ? 265 ] prf. 266 [1: normalize in left_nil_absrd; 267 cases left_nil_absrd; 268 3: normalize in l_r_nil_absrd; 269 cases l_r_nil_absrd; 270 2: normalize in outer_prf; 271 generalize in match outer_prf; 272 cases l_r; 273 [ normalize // 274  #SZ #KEY_TYPE #ELT_TYPE #LEFT #RIGHT 275 normalize 276 #HYP 277 ] 278 qed. 201 279 202 280 definition map_double_l ≝
Note: See TracChangeset
for help on using the changeset viewer.