• Robbert Krebbers's avatar
    Clean up heap_lang and remove some FIXMEs. · 15058014
    Robbert Krebbers authored
    Notable changes:
    * I am now using the same names for the fields of the language record and the
      instances in heap_lang. In order to deal with shadowing, I have put all
      definitions in heap_lang.v in a module.
    * Instead of defining evaluation contexts recursively, these are now defined
      using lists. This way we can easily reuse operations on lists. For example,
      composition of evaluation contexts is just appending lists. Also, it allowed
      me to simplify the rather complicated proof of step_by_val as induction on
      the shape of contexts no longer results in a blow-up of the number of cases.
    * Use better automation to prove all lemmas of heap_lang.
    * I have introduced tactics to invert steps and to do steps. These tactics
      greatly helped simplifying boring parts of lifting lemmas.
    15058014
_CoqProject 1.19 KB