Improve `scalar_tac`

[sonmarcho]

trafficstars

The scalar_tac tactic is heavily used as there are a lot of arithmetic proof obligations in the proofs. It can be dramatically improved, both in terms of performance and features.

For instance:

• scalar_tac splits all the "cases" (the if ... then ... else ..., the match ... with but not the \/- maybe it should for the latter ones; for now it is handled afterwards by the omega tactic which scalar_tac delegates the end of the proof to) which appear in the context before calling simp_all. To be more precise and because it is expensive: it first attempts the proof without splitting, then retries after splitting. As progress tries scalar_tac on all arithmetic preconditions, the cost of failing on goals for which we split can be expensive. We should add an option to deactivate this behavior globally (and have some syntax to reactivate it on a per-case basis, like scalar_tac split).
• scalar_tac applies some simplification lemmas during its preprocessing phase. For now, those lemmas are hardcoded in the tactic, but they should not: we should introduce attributes to add such lemmas in an extensible manner. Also, there are two simplification phases: one before the "saturation" phase, and one after, so we should have two sets of lemmas. For some context: the saturation phase introduces useful facts in the context, and the system is extensible (see this PR - note that since then we reimplemented our own saturation mechanism which doesn't use aesop: see here). For instance, if we have the lemma:

@[simp, scalar_tac replicate l x]
theorem replicate_length {α : Type u} (l : Nat) (x : α) :
  (replicate l x).length = l := by
  induction l <;> simp_all

Then whenever scalar_tac sees something of the shape replicate l x in the context, it will introduce the assumption (replicate l x).length = l in the preprocessing phase. The two simplification phases (before saturation/after saturation) can be found here and there.

• the lemmas introduced during the saturation phase can be improved. For instance, whenever scalar_tac sees Scalar.toNat x it introduces the fact (x.toNat : Int) = x.val \/ (x.toNat : Int) = - x.val. If the scalar is an unsigned scalar it is always positive, so the second case can not happen (omega performs a case split on all the disjunctions, so this has a cost). We could fix the issue if we added lemmas of the shape : (x.toNat : Int) = x.val \/ (x.toNat : Int) = - x.val <-> (x.toNat : Int) = x.val in the simplification lemmas (for after the saturation phase) for all the unsigned scalar types.