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.

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

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

This class whose name is horrible and purpose is arbitrary seems to be a
leftover of some experiment with ch2o, a long time a ago.

simplify_equality        => simplify_eq
simplify_equality'       => simplify_eq/=
simplify_map_equality    => simplify_map_eq
simplify_map_equality'   => simplify_map_eq/=
simplify_option_equality => simplify_option_eq
simplify_list_equality   => simplify_list_eq
f_equal'                 => f_equal/=

The /= suffixes (meaning: do simpl) are inspired by ssreflect.

Also, make our redefinition of done more robust under different
orders of Importing modules.

Major changes:
* A data structure to collect locked addresses in memory.
* Operations to lock and unlock addresses.
* Remove [ctree_Forall] and express it using [Forall] and [ctree_flatten]. This
  saves a lot of lines of code.
* Add a [void] value. This value cannot be typed, but will be used as a dummy
  return value for functions with return type [void].

Minor changes:
* Various deciders in preparation of the executable semantics.
* Improve naming and notations.
* Remove obsolete stuff.

The refactoring includes:
* Use infix notations for the various list relations
* More consistent naming
* Put lemmas on one line whenever possible
* Change proofs into one-liners when possible
* Make better use of the "Implicit Types" command
* Improve the order of the list module by placing all definitions at the start,
  then the proofs, and finally the tactics.

Besides, there is some new machinery for proofs by reflection on lists. It is
used for a decision procedure for permutations and list containment.

Both the operational and axiomatic semantics are extended with sequence points
and a permission system based on fractional permissions. In order to achieve
this, the memory model has been completely revised, and is now built on top
of an abstract interface for permissions.

Apart from these changed, the library on lists and sets has been heavily
extended, and minor changed have been made to other parts of the prelude.

The development now corresponds exactly to the FoSSaCS 2013 paper.
Also, the prelude is updated to the one of the master branch.

* Define the standard strict order on pre orders.
* Prove that this strict order is well founded for finite sets and finite maps.
  We also provide some utilities to compute with well founded recursion.
* Improve the "simplify_option_equality" tactic to handle more cases.
* Axiomatize finiteness of finite maps by translation to lists, instead of by
  them having a finite domain.
* Prove many additional properties of finite maps.
* Add many functions and theorems on lists, including: permutations, resize,
  filter, ...

Most interestingly:
* Use [lia] instead of [omega] everywhere
* More many generic lemmas on the memory to the theory on finite maps.
* Many additional list lemmas.
* A new interface for a monad for collections, which is now also used by the
  collection tactics.
* Provide an additional finite collection implementation using unordered lists
  without duplicates removed. This implementation forms a monad (just the list
  monad in disguise).

The following things have been changed in this revision:

* We now give a small step semantics for expressions. The denotational semantics
  only works for side-effect free expressions.
* Dynamically allocated memory through alloc and free is now supported.
* The following expressions are added: assignment, function call, unary
  operators, conditional, alloc, and free.
* Some customary induction schemes for expressions are proven.
* The axiomatic semantics (and its interpretation) have been changed in order
  to deal with non-deterministic expressions.
* We have added inversion schemes based on small inversions for the operational
  semantics. Inversions using these schemes are much faster.
* We improved the statement preservation proof of the operational semantics.
* We now use a variant of SsReflect's [by] and [done], instead of Coq's [now]
  and [easy]. The [done] tactic is much faster as it does not perform
  inversions.
* Add theory, definitions and notations on vectors.
* Separate theory on contexts.
* Change [Arguments] declarations to ensure better unfolding.

improve some definitions, simplify some proofs.

The main changes are:

* Function calls in the operational semantics
* Mutually recursive function calls in the axiomatic semantics
* A general definition of the interpretation of the axiomatic semantics  so as
  to improve reusability (useful for function calls, and also for expressions
  in future versions)
* Type classes for stack independent, memory independent, and memory extensible
  assertions, and a lot of instances to automatically derive these properties.
* Many additional lemmas on the memory and more robust tactics to simplify
  goals involving is_free and mem_disjoint
* Proof of preservation of statements in the smallstep semantics

* Some new tactics: feed, feed destruct, feed inversion, etc...
* More robust tactic scripts using bullets and structured scripts
* Truncate most lines at 80 characters