Design and implement a set of conditions to check before running a tactic

[Russoul]

We don't want to re-elaborate a tactic multiple times, it's inefficient. Moreover, for tactics elaboration to stay order-independent, we need to design a set of constraints to be checked before running elaboration of one. There are a few constraints already but I haven't drawn due attention to whatever it's enough yet. These two wanted properties should form a basis for the conditions we impose pre-elaboration.