This also removes the double use of the name 'wp_fork' in both
program_logic/weakestpre and heap_lang/lifting.

Add lock interface

@jung looks good?

See merge request !3

NB: these scopes delimiters were already there before Janno's a0067662.

Following the time anology of later, the step-index 0 corresponds does
not correspond to 'now', but rather to the end of time (i.e. 'last').

Make names more consistent with the rest of the development, make
definitions type classes opaque so that the proofmode does not unfold
then, declare timeless, persistent and proper instances.

unfolded logically atomic triple

The definition is a bit funky now to hack together something fast. See demo section for an example of application.

cc @dreyer @jung @robbertkrebbers @jjourdan 

See merge request !7

This is allowed as long as one of the conjuncts is thrown away (i.e. is a
wildcard _ in the introduction pattern). It corresponds to the principle of
"external choice" in linear logic.

Also, since do_head_step no longer has a purpose, I have removed it
and just use a bunch of eauto hints.

This implements issue #3.