feature wish : goal- or more generally task-oriented proof strategies
This issue suggests a more general form of strategies, which are not blind with respect to the current goal. The idea would be to mimick the current function Controller_itp.run_strategy on goal
, but instead of passing a quite limited parameter Strategy.t
, would accept a function of type task -> strat
. The type strat could be
something like
type strat = Do_nothing | Run_prover of prover * time * ... | Apply_trans of Trans.t * strat list
In the case Apply_trans
, it is supposed to apply the given transformation, that should return the same number of subgoals as the given sublist of strat
, and then each of these sub strat should be in turn applied to the corresponding subtask.
Such a general mechanism should permit to write complex, dedicated proof strategies that operate differently in function of the shape of the goal: e.g., decide to compute things in the goal, apply specific known lemmas for the topmost predicate symbol. A mechanism similar to Frama-C Qed
should be doable with that mechanism.