Skip to content
  • Jakob Botsch Nielsen's avatar
    Refactor finite map/finite sets and prove map-list/set-list equality · 5e814944
    Jakob Botsch Nielsen authored
    * Pull the functionality we need into a Containers.v file that takes
      care of including the proper implementations of fmaps and fsets.
      Additionally, this file defines notation/new names.
    * Stop using map/set notation for operations. This conflicts with
      lists/record-set and is generally a head-ache.
    * Switch to lists instead of AVL trees for the sets and maps. This
      allows us to prove (assuming proof irrelevance) what we need:
      FSet.of_list (FSet.elements x) = x. Prove this and the equivalent for
      fin maps.
    * Do not use program instances in Oak.v. We can do with instances which
      generate a lot less bloat.