Changeset 1052 for src/utilities


Ignore:
Timestamp:
Jul 4, 2011, 3:31:18 PM (9 years ago)
Author:
mulligan
Message:

removed offsets after reading cerco mailing list

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/HMap.ma

    r1050 r1052  
    230230  ].
    231231
     232lemma map_double_r_property_p_exists:
     233  ∀key_type.
     234  ∀elt_type.
     235  ∀left: map key_type elt_type.
     236    map_double_r_property_p key_type elt_type left →
     237      ∃l_sz, l_key, l_elt, l_l, l_r.
     238        left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r.
     239  #KEY_TYPE #ELT_TYPE #LEFT
     240  cases LEFT
     241  [ normalize #HYP cases HYP
     242  | #L_SZ #L_KEY #L_ELT #L_LEFT #L_RIGHT
     243    #HYP
     244    @ex_intro
     245    [1: @L_SZ
     246    |2: @ex_intro
     247        [1: @L_KEY
     248        |2: @ex_intro
     249            [1: @L_ELT
     250            |2: @ex_intro
     251                [1: @L_LEFT
     252                |2: @ex_intro
     253                    [1: @L_RIGHT
     254                    |2: %
     255                    ]
     256                ]
     257            ]
     258        ]
     259    ]
     260  ]
     261qed.
     262
     263lemma map_double_r_property_p_exists_l_r_not_nil_p:
     264  ∀key_type.
     265  ∀elt_type.
     266  ∀left: map key_type elt_type.
     267    map_double_r_property_p key_type elt_type left →
     268      ∃l_sz, l_key, l_elt, l_l, l_r.
     269        (left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r) ∧
     270        map_not_nil_p key_type elt_type l_r.
     271  #KEY_TYPE #ELT_TYPE #LEFT
     272  cases LEFT
     273  [ normalize #HYP cases HYP
     274  | #L_SZ #L_KEY #L_ELT #L_LEFT #L_RIGHT
     275    #HYP
     276    @ex_intro
     277    [1: @L_SZ
     278    |2: @ex_intro
     279        [1: @L_KEY
     280        |2: @ex_intro
     281            [1: @L_ELT
     282            |2: @ex_intro
     283                [1: @L_LEFT
     284                |2: @ex_intro
     285                    [1: @L_RIGHT
     286                    |2: @conj
     287                        [1: %
     288                        |2: generalize in match HYP
     289                            cases L_RIGHT
     290                            [1: normalize //
     291                            |2: #NEW_SZ #NEW_KEY #NEW_ELT #NEW_L #NEW_R
     292                                normalize //
     293                            ]
     294                        ]
     295                    ]
     296                ]
     297            ]
     298        ]
     299    ]
     300  ]
     301qed.
     302
    232303definition map_double_r ≝
    233304  λkey_type.
     
    246317    ]
    247318  ].
    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.
    279319
    280320definition map_double_l ≝
Note: See TracChangeset for help on using the changeset viewer.