Speed up the cf tactics

[xrchz]

This issue is about reviewing the implementation of the tactics in characteristic and taking any quick wins on efficiency. A good benchmark would be examples/pseudo_bool/array.

[tanyongkiam]

The specific slowdowns are due to xlet_auto and xmatch

[ordinarymath]

The internal simplifier calls in cf tactics are slow because traversing terms is slower than it currently slower than it needs to be. And the terms are really big because strings are really big terms

[tanyongkiam]

Do you have some evidence or pointers specifically to show that this is causing significant slowdown overall in CF?

[dnezam]

The profiler was made for exactly this purpose. A good first step is to use it to measure and locate heavy hitters by looking at the flamegraphs/flamecharts.

In my last attempt it turned out a lot of time was spent in simp calls which became much better by replacing some of those calls with simpler tactics (in particular those that don't make use of the arithmetic decision procedure).

For experimenting I can also recommend commenting out the :> ... in the tactic libs so one has access to helpers and can instrument those as well.