Using this new definition we can express being contractive using a
Proper. This has the following advantages:

- It makes it easier to state that a function with multiple arguments
  is contractive (in all or some arguments).
- A solve_contractive tactic can be implemented by extending the
  solve_proper tactic.

Use notation N @⊆ E to avoid ambiguity.

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.

See merge request !24

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.

In particular, make sure we always try eassumption before reflexivity.

That range includes tabs and new lines.

Thanks Morten for spotting this problem.

This way we can use set_solver to solve goals involving ∈.

This has bothered me repeatedly in proofs, now I finally got around to fix it at the source

(These instances are not defined for any FinMap to avoid overlapping
instances for EqDecision, which may have awkward consequences for
type class search).

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.