This addresses some concerns in !5.

This way, we will be compabile with Iris's heap_lang, which puts ;;
at level 100.

This allows for more control over `Hint Mode`.

This provides significant robustness against looping type class search.

As a consequence, at many places throughout the library we had to add
additional typing information to lemmas. This was to be expected, since
most of the old lemmas were ambiguous. For example:

  Section fin_collection.
    Context `{FinCollection A C}.

    size_singleton (x : A) : size {[ x ]} = 1.

In this case, the lemma does not tell us which `FinCollection` with
elements `A` we are talking about. So, `{[ x ]}` could not only refer to
the singleton operation of the `FinCollection A C` in the section, but
also to any other `FinCollection` in the development. To make this lemma
unambigious, it should be written as:

  Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.

In similar spirit, lemmas like the one below were also ambiguous:

  Lemma lookup_alter_None {A} (f : A → A) m i j :
    alter f i m !! j = None  m !! j = None.

It is not clear which finite map implementation we are talking about.
To make this lemma unambigious, it should be written as:

  Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
    alter f i m !! j = None  m !! j = None.

That is, we have to specify the type of `m`.

See also Coq bug #5712.

Before, we often had to insert awkward casts when using them. Also,
the generality of also having them on Type, is probably not useful.

For example, instead of:

  Notation "( X ⊆ )"

We now use:

  Notation "( X ⊆)"

We were already doing this for = and ≡.

This solves some conflicts with the notations of MetaCoq.

Some were already maximally implicit, some were not. Now it is consistent.

This approach is originally by Robbert

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

Robbert Krebbers authored 8 years ago and Ralf Jung committed 8 years ago

We do this by introducing a type class UpClose with notation ↑.

The reason for this change is as follows: since `nclose : namespace
→ coPset` is declared as a coercion, the notation `nclose N ⊆ E` was
pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked
because type checking goes from left to right, and as such would look
for an instance `SubsetEq namespace`, which causes the right hand side
to be ill-typed.

Having Is_true as a type class caused problems with rewrite: when the
rewrited lemma has a premise of the shape Is_true, the rewrite tactic
will complain that it cannot find a type class instance, instead
of generating a goal for that premise.

This makes the typeclass mechanism able to use instances like [Is_true X -> Blah], where X reduces to X.

There is still the reals stuff, which is caused by importint Psatz (needed
for lia) and eq_rect_eq which is caused by importint Eqdep_dec.

This reverts commit 20b4ae55bdf00edb751ccdab3eb876cb9b13c99f, which does
not seem to work with Coq 8.5pl2 (I accidentally tested with 8.5pl1).

This makes type checking more directed, and somewhat more predictable.

On the downside, it makes it impossible to declare the singleton on
lists as an instance of SingletonM and the insert and alter operations
on functions as instances of Alter and Insert. However, these were not
used often anyway.

There was not really a need for the lattice type classes, so I removed
these.