Update scalar_tac to use the aesop tactic

[sonmarcho]

This PR is a first step towards relying on Aesop for some class of automation. As such it is very basic, but opens up quite interesting possibilities.

For now, I simply replaced the part of scalar_tac which automatically introduces assumptions in the goal, for instance to introduce information about the bounds of the machine integers in the context. As I needed this system to be extensible I originally used typeclasses, but it was a bit ad-hoc. By using the forward reasoning abilities of aesop, and in particular its "patterns", I was able to make the implementation simpler and more flexible. In practice, it works as follows.

Whenever we want scalar_tac to automatically introduce a lemma in the context during its preprocessing step, we simply mark the lemma with the scalar_tac attribute, together with a pattern which will guide the application.
For instance (comes from here) to introduce bounds for all x : Scalar ty in the context:

@[scalar_tac x]
theorem Scalar.bounds {ty : ScalarTy} (x : Scalar ty) :
  Scalar.min ty ≤ x.val ∧ x.val ≤ Scalar.max ty :=
  And.intro x.hmin x.hmax

It is possible to make the rules local (to a section/file) with the local keyword (this comes for free). I use this in the proof of the hashmap, for instance (see here - I pasted the code below) to use the fact that some arithmetic facts can be deduced from the invariant. The idea is to have automation, but local to the file (it wouldn't make sense for this rule to escape to client code). If we think in terms of SMT automation (for instance, with Dafny), this is tantamount to declaring the invariant as transparent, except here we reveal only the facts we need, and when reasoning about arithmetic (with scalar_tac).

@[local scalar_tac h]
theorem inv_imp_eqs_ineqs {hm : HashMap α} (h : hm.inv) :
  0 < hm.slots.length ∧ hm.num_entries = hm.al_v.len := by
  simp_all [inv]

Because I expect this to be frequently used, I defined a rule set for some non-linear arithmetic rules, which can be activated via the option scalarTac.nonLin. They provide rules to reason about the modulo operation (I use it in the hashmap) or the fact that the multiplication of two positive numbers is positive. For instance (comes from here):

@[nonlin_scalar_tac n % m]
theorem Int.emod_of_pos_disj (n m : Int) : m ≤ 0 ∨ (0 ≤ n % m ∧ n % m < m)

I also provide a generic way of specifying the sets of rules to use (see here).

[sonmarcho]

@JLimperg I think this is of interest to you :)