Changeset 1050 for src/utilities


Ignore:
Timestamp:
Jul 4, 2011, 10:43:37 AM (9 years ago)
Author:
mulligan
Message:

adding dependent types to map datastructure to remove all option types. some changes to rtlabs to rtl translation pass.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/HMap.ma

    r1049 r1050  
    170170  ].
    171171
     172definition 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
     187qed.
     188
    172189definition map_single_r ≝
    173190  λkey_type.
     
    181198  | map_fork l_sz l_key l_elt l_l l_r ⇒
    182199      Some ? (map_binsert ? ? l_key l_elt l_l (map_binsert ? ? key elt l_r right))
     200  ].
     201
     202definition 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
     217qed.
     218
     219definition 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    ]
    183230  ].
    184231
     
    199246    ]
    200247  ].
     248
     249definition 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  ]
     278qed.
    201279
    202280definition map_double_l ≝
Note: See TracChangeset for help on using the changeset viewer.