Add bag and tweak lock

This MR adds example 7.38 from the Iris lecture notes. That is, a course grained back implemented based on a lock developed earlier in the lecture notes.

The MR also tweaks lock.v slightly. I've made it better match the lecture notes where the is_lock predicate takes a value and not a location. I.e. it hides that the lock is implemented as a location. Besides that I've changed the names of the lemmas in the specification such that they match what those are typically called in Iris for a lock.

Note, that I did not write the bag from scratch. I merely cleaned it up and adapted it to the current version of Iris.