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.