Cancelable elements are a new way of proving local updates, by
removing some cancellable element of the global state, provided that
we own it and we are willing to lose this ownership.

Identity-free elements are an auxiliary that is necessary to prove that
[Some x] is cancelable.

For technical reasons, these two notions are not defined exactly like
what one might expect, but also take into account validity. Otherwise,
an exclusive element would not be cancelable or idfree, which is
rather confusing.

Also add "Local" to some Default Proof Using to keep them more contained

by Janno

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

Use COFEs only for the recursive domain equation solver

This is more consistent with the definition of the extension order, which
is also defined in terms of an existential.

Also, remove some unused lemmas about agree.

This may save the need to seal off some stuff.

be the same as .

This is a fairly intrusive change, but at least makes notations more
consistent, and often shorter because fewer parentheses are needed. Note
that viewshifts already had the same precedence as →.

Based on an idea and WIP commits of J-H. Jourdan: the core of a CMRA
A is now a partial function A → option A.

TODO: define sum CMRA
TODO: remove one shot CMRA and define it in terms of sum

- Make the carrier argument of the constructors for the canonical structures
  cofeT and cmraT explicit. This way we make sure the carrier is properly
  exposed, instead of some alias of the carrier.
- Make derived constructions (such as discreteC and discreteR) notations
  instead of definitions. This is yet again to make sure that the carrier is
  properly exposed.
- Turn DRA into a canonical structure (it used to be a type class).

This fixes some issues, notably it fixes some broken rewrites in algebra/sts
and it makes canonical structures work properly with dec_agree.

The only drawback is that we have to restrict iprod to finite types,
but that is fine.

Thanks to Amin Timany for the suggestion.

So, only use the type class for contractive functors.

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.

Since functor instances are just used as combinators, there is really
no need for functors that are not contractive.

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

It now also contains a non-expansiveness proof.

I have simplified the following CMRA axioms:

  cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y;
  cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y;

By dropping off the step-index, so into:

  cmra_unit_preservingN x y : x ≼ y → unit x ≼ unit y;
  cmra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y;

The old axioms can be derived.

The performance gain seems neglectable, unfortunatelly...

This way it behaves better for discrete CMRAs.

This better seals off their definition. Although it did not give
much of a speedup, I think it is conceptually nicer.