GitLab

Thanks to Amin Timany for the suggestion.

Add both non-expansive and contractive functors, and bundle them for the general Iris instance as well as the global functor construction

This allows us to move the \later in the user-defined functor to any place we want.
In particular, we can now have "\later (iProp -> iProp)" in the ghost CMRA.

This cleans up some ad-hoc stuff and prepares for a generalization
of saved propositions.

Still need to use it everywhere.

It is doing much more than just dealing with ∈, it solves all kinds
of goals involving set operations (including ≡ and ⊆).

* These type classes bundle an identifier into the global CMRA with a proof
  that the identifier points to the correct CMRA. Bundling allows us to get
  rid of many arguments everywhere.

* I have setup the type classes so that we no longer have to keep track of the
  global CMRA identifiers. These are implicit and resolved automatically.

* For heap I am also bundling the name of the heap RA instance. There always
  should be at most one heap instance so this does not introduce ambiguities.

* We now have a "maps to" notation!

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

Since Coq 8.4 did not backtrack on eauto premises, we used to ensure
that hints like

  Hint Extern 0 (?x ≡{_}≡ ?y) => reflexivity.

were not used for goals involving evars by writing ?x ≡{_}≡ ?y instead
of _ ≡{_}≡ _.

This seems to be a legacy issue that no longer applies to Coq 8.5, so
I have removed these restrictions making these hints thus more powerful.

change statement of inv-open lemmas such that they do not force the invariant, and the 'inner step', to appear right next to each other

Also do some minor clean up.

globalC -> globalF
New notation: iPropG, iFunctorG

It is now slightly below implication. In order to do this, I had to change
the notation from P ={E1,E2}=> Q to P >{E1,E2}=> Q because the prefer ={n
is already used at level 70 for the distance of the metric.

Actual proofs will end up using own and inv, and none of the notions defined in ownership.v

This way we can more easily state lemmas for concrete languages for
arbitrary global functors.