Improve the `saturate` tactic for `scalar_tac`

[sonmarcho]

trafficstars

Use Aesop

We should use Aesop's saturate tactic to saturate the context forward, as it would allow quite expressive patterns in scalar_tac like:

@[scalar_tac a < b, c < d]
theorem ... (a b c d : Nat)  (h0 : a < b) (h1 : c < d) : a * c < b * d

Degenerate Patterns

Several theorems use "degenerate" patterns which are simply made of a variable, whenever we want to instantiate a theorem for all the expressions of a given type we find in the context. For instance:

@[scalar_tac x]
theorem UScalar.bounds {ty : UScalarTy} (x : UScalar ty) :
  x.val ≤ UScalar.max ty :=
  x.hBounds

The problem is that we the current implementation of saturate, which uses a discrimination tree, the pattern x ignores the type of x meaning this theorem gets matched against all the expressions in the context. This is expensive, and my understanding is that Aesop does the same.

Worse, because of this many expressions which use big integer constants (such as 2^32) get matched. The issue is that when matching a constant like 1000 with another expression, it often gets reduced to succ (succ ...) (1000 times) leading to a "maximum recursion depth reached" exception.

For now, the solution is for saturate to first check if the types of the expressions are definitionally equal, so that we don't compare, e.g., 1000 : Nat with ?x : UScalar ?ty, then compare the expressions themselves. It would be good to implement better support for degenerate patterns, for instance by looking up theorems based on the type rather than the expression itself.