Flexible heuristics for simplification with conditional lemmas by marking formulas as forbidden, mandatory, obligatory, and generous

Due to its practical importance, context-dependent simplification of goals with conditional lemmas has been studied for three decades, mostly under the label of “contextual rewriting”. We present a flexible framework for controlling the recursive relief of conditions by marking formulas in goals and lemmas. Within this framework, by marking goal formulas as forbidden, we can simulate and improve the well-known approaches of contextual rewriting and case rewriting. Furthermore, we develop novel heuristics which may mark goal formulas as mandatory and lemma formulas as obligatory or generous. Our case studies in the field of rewrite-based inductive theorem proving are encouraging.