The general idea is to first import/export modules which are further
than the current one, and then import/export modules which are close
dependencies.

This commit tries to use the same order of imports for every file, and
describes the convention in ProofGuide.md. There is one exception,
where we do not follow said convention: in program_logic/weakestpre.v,
using that order would break printing of texan triples (??).

We already do the same for the goal, this avoids some scope
delimiters being displayed.

The proof mode now explicitly keeps track of anonymous hypotheses (i.e.
hypotheses that are introduced by the introduction pattern `?`). Consider:

  Lemma foo {M} (P Q R : uPred M) : P -∗ (Q ∗ R) -∗ Q ∗ P.
  Proof. iIntros "? [H ?]". iFrame "H". iFrame. Qed.

After the `iIntros`, the goal will be:

  _ : P
  "H" : Q
  _ : R
  --------------------------------------∗
  Q ∗ P

Anonymous hypotheses are displayed in a special way (`_ : P`). An important
property of the new anonymous hypotheses is that it is no longer possible to
refer to them by name, whereas before, anonymous hypotheses were given some
arbitrary fresh name (typically prefixed by `~`).

Note tactics can still operate on these anonymous hypotheses. For example, both
`iFrame` and `iAssumption`, as well as the symbolic execution tactics, will
use them. The only thing that is not possible is to refer to them yourself,
for example, in an introduction, specialization or selection pattern.

Advantages of the new approach:

- Proofs become more robust as one cannot accidentally refer to anonymous
  hypotheses by their fresh name.
- Fresh name generation becomes considerably easier. Since anonymous hypotheses
  are internally represented by natural numbers (of type `N`), we can just fold
  over the hypotheses and take the max plus one. This thus solve issue #101.

This solves issue #100: the proof mode notation is sometimes not printed. As
Ralf discovered, the problem is that there are two overlapping notations:

```coq
Notation "P ⊢ Q" := (uPred_entails P Q).
```

And the "proof mode" notation:

```
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
  (of_envs (Envs Γ Δ) ⊢ Q%I).
```

These two notations overlap, so, when having a "proof mode" goal of the shape
`of_envs (Envs Γ Δ) ⊢ Q%I`, how do we know which notation is Coq going to pick
for pretty printing this goal? As we have seen, this choice depends on the
import order (since both notations appear in different files), and as such, Coq
sometimes (unintendedly) uses the first notation instead of the latter.

The idea of this commit is to wrap `of_envs (Envs Γ Δ) ⊢ Q%I` into a definition
so that there is no ambiguity for the pretty printer anymore.

Fixes #96

After discussing this with Ralf, again, it turned out that using a bar
instead of a turnstyle would be better. When formalizing type systems, one
often wants to use a turnstyle in other notations (the typing judgment),
so having the turnstyle in the proofmode notation is confusing.

Fixes issue #85

Unfortunately, we currently have to keep the unicode-space hack in some places because Coq still complains about the notation otherwise

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

The old choice for ★ was a arbitrary: the precedence of the ASCII asterisk *
was fixed at a wrong level in Coq, so we had to pick another symbol. The ★ was
a random choice from a unicode chart.

The new symbol ∗ (as proposed by David Swasey) corresponds better to
conventional practise and matches the symbol we use on paper.

FDor editors that display 0-width space with more than 0 width, this makes the indentation of assertions more consistent

newline before the first context" and "shuffle 0-width spaces around so
they are distributed more evenly"

This reverts commits e3c56f9e and
7fc1124c, which are workarounds for
Coq bug https://coq.inria.fr/bugs/show_bug.cgi?id=4675

Also, this commit fixes the levels to avoid parantheses.

Pros:
* It does not matter how editors render the 0-width space, everything is always aligned
* In ProofGeneral, there is no more incorrectn indentation of the first line

Cons:
* There is an empty line between the bar ending the Coq context, and the first Iris hypothesis