Add a contributor's guide

See merge request !47

When using [iAssert ... with ">[]"], we should not use [tac_assert_persistent], and eliminate the modality instead.

This patch is still not ideal, because some modalities (e.g., later) preserve persistence.

For example, when having `"H" : ∀ x : Z, P x`, using
`iSpecialize ("H" $! (0:nat))` now works. We do this by first
resolving the `IntoForall` type class, and then instantiating
the quantifier.

Instead of doing all the instantiations by invoking a single type
class search, it now performs the instantiations by invoking
individual type class searches. This a.) gives better error messages
and b.) works when `xj` depends on `xi`.

In the following ways:
- When having `P → Q` it will now also work when the spatial context
  is non-empty.
- When having `∀ x : A, Q` it will now do an `iIntros (_)`.

Make it possible to apply the observational view shift lemmas.

See merge request !40

In this case, we cannot use all the hypotheses for proving the premises as well
as for the remaining goal.

use coq-stdpp

See merge request !46

It no longer requires the functions on both sides of the relation
to be syntactically the same.

Cancelable elements are a new way of proving local updates, by
removing some cancellable element of the global state, provided that
we own it and we are willing to lose this ownership.

Identity-free elements are an auxiliary that is necessary to prove that
[Some x] is cancelable.

For technical reasons, these two notions are not defined exactly like
what one might expect, but also take into account validity. Otherwise,
an exclusive element would not be cancelable or idfree, which is
rather confusing.

This fixes issue #57.

I considered supporting these introduction patterns also in a nested fashion --
for example allowing `iDestruct foo as [H1 [{H1} H1 /= H2|H2]` -- but that
turned out to be quite difficult.

Where should we allow `/=`, `{H}` and `{$H}` exactly. Clearly something like
`>/=` makes no sense, unless we adopt to some kind of 'stack like' semantics
for introduction patterns as in ssreflect. Alternatively, we could only allow
these patterns in the branches of the destructing introduction pattern
`[... | ... | ...]` but that brings other complications, e.g.:

- What to do with `(H1 & /= & H3)`?
- How to distinguish the introduction patterns `[H _]` and `[_ H]` for
  destructing a spatial conjunction? We cannot simply match on the shape of the
  introduction pattern anymore, because one could also write `[_ H /=]`.