- Remove the coercion from `Qp` to `Qc`, and remove it into from `Qp_car` into
  `Qp_to_Qc` to be consistent with other conversion functions.
- Use `let '(..) = ...` in the definitions of `Qp_plus`/`Qp_mult`/`Qp_div` to
  avoid Coq tactics (like `injection`) to unfold these definitions eagerly.
- Define orders `Qp_le` and `Qp_lt`, instead of relying on the orders on `Qc`,
  which were obtained through the removed coercion into `Qc`.
- Lift lemmas about the orders from `Qc` to `Qp`.
- Improve variable names and use of notation scopes.

Thanks to @simongregersen for reporting.

Note that prior to 0d7a7f06 we would get this instance automatically,
but that instance would not have the right computational behavior.

This follows iris/iris!387
This closes issue #54.

Use Open/Close Scope without Local (i.e., export the scope opening)
only when the scope corresponds to the main purpose of the module.

Jakob Botsch Nielsen authored 6 years ago and Robbert Krebbers committed 6 years ago

This changes the encoding used for finite lists of values of countable
types to be linear instead of exponential. The encoding works by
duplicating bits of each element so that 0 -> 00 and 1 -> 11, and then
separating each element with 10. The top 1-bits are not kept since we
know a 10 is starting a new element which ends with a 1.

Fix #28

This allows for more control over `Hint Mode`.

This instance leads to exponential failing searches.

These trees are useful to show that other types are countable.

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

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.

Also do some minor clean up.

Also, use a different encoding of lists.

The port makes the following notable changes:

* The carrier types of separation algebras and integer environments are no
  longer in Set. Now they have a type at a fixed type level above Set. This
  both works better in 8.5 and makes the formalization more general.
  I have tried putting them at polymorphic type levels, but that increased the
  compilation time by an order of magnitude.
* I am using a custom f_equal tactic written in Ltac to circumvent bug #4069.
  That bug has been fixed, so this custom tactic can be removed when the next
  beta of 8.5 is out.

Major changes:
* Make void a base type, and include a proper void base value. This is necessary
  because expressions (free, functions without return value) can yield a void.
  We now also allow void casts conforming to the C standard.
* Various missing lemmas about typing, weakening, decidability, ...
* The operations "free" and "alloc" now operate on l-values instead of r-values.
  This removes some duplication.
* Improve notations of expressions and statements. Change the presence of the
  operators conforming to the C standard.

Small changes:
* Use the classes "Typed" and "TypeCheck" for validity of indexes in memory.
  This gives more uniform notations.
* New tactic "typed_inversion" performs inversion on an inductive predicate
  of type "Typed" and folds the premises.
* Remove a horrible hack in the definitions of the classes "FMap", "MBind",
  "OMap", "Alter" that was used to let "simpl" behave better. Instead, we have
  defined a tactic "csimpl" that folds the results after performing an
  ordinary "simpl".
* Fast operation to remove duplicates from lists using hashsets.
* Make various type constructors (mainly finite map implementations) universe
  polymorphic by packing them into an inductive. This way, the whole C syntax
  can live in type, avoiding the need for (slow) universe checks.