Implement more powerful context simplification tactics

[sonmarcho]

We need to have more powerful (and efficient) tactics to simplify the context. For now, I'm relying a lot on simp_all, but it is slow (see this issue for instance) and can't do everything.

A first use case is reasoning about lists. For instance, we have the following lemmas, which are used in particular in the hashmap (note that Nat.not_eq i j is just a clever way of writing i <> j so that it matches many expressions like i < j, j < i, etc.):

@[simp]
theorem index_update_eq
  {α : Type u} [Inhabited α] (l: List α) (i: Nat) (x: α) :
  i < l.length → (l.update i x).index i = x

@[simp]
theorem index_update_neq
  {α : Type u} [Inhabited α] (l: List α) (i: Nat) (j: Nat) (x: α) :
   Nat.not_eq i j → (l.update i x).index j = l.index j

Those lemmas are marked as simp, which means that if, say, we have i < l.length and i < j in the context, then doing simp [*] will manage to apply index_update_neq and discharge its preconditions. Doing this is probably not the best way to go, especially because we have to be aware of those simplification lemmas, meaning we often have to introduce lines of the shape:

have : i < l.length := by scalar_tac

at the beginning of the proofs, in a fashion which is very reminiscent of what we had to do with SMT patterns (by writing assertions in a very specific shape so that we know they will match SMT patterns).

It would be good to have "smarter" simplification tactics (say, a list_simp tactic, or a simp_ctx tactic which would bundle several simplification procedures) which does this kind of simplification. A simple way of implementing such a tactic would be simply to call simp and use scalar_tac as a discharger tactic.

Generally speaking, I believe we will need specialized simplification tactics for various kinds of reasonings, so it would be good to find a generic way of doing so. Something interesting and quite powerful would be for instance to have an attribute like simp, but which would allow indicating which tactic to use to discharge which assumption. Maybe we could simply reuse the notation for default arguments of Lean maybe; it would look like:

@[simp_ctx] -- new attribute
theorem index_update_neq
  {α : Type u} [Inhabited α] (l: List α) (i: Nat) (j: Nat) (x: α)
  (hNotEq : i <> j := by scalar_tac) : -- use scalar_tac to discharge this assumption
  (l.update i x).index j = l.index j