GitLab

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 (_)`.

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

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 /=]`.

This fixes issue #67.

It now copies the hypothesis when: 1.) it is persistent 2.) when destructing
it requires a universal quantifier to be instantiated. The new behavior is
implemented using a type class (called CopyDestruct) so that it can easily be
extended.

This fixes issue #51.

This fixes issue #62.

The error message accidentally got removed in e0789039.

This fixes issue #61.

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing

For iApply and iRewrite we want that, but for iDestruct and iMod we do not.

This fixes issue #52.

I also renamed `iProof` into `iStartProof`, as it is supposed to be
something internal, and not a substitute of Coq's `Proof` command (as
originally intended).

This fixes issue #44.

    The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.