mathlib documentation

core / init.meta.backward

meta constant tactic.back_lemmas  :

Create a datastructure containing all lemmas tagged as [intro]. Lemmas are indexed using their head-symbol. The head-symbol is computed with respect to the given transparency setting.

(back_lemmas_insert_core m lemmas lemma) adds the given lemma to the set back_lemmas. It infers the type of the lemma, and uses its head-symbol as an index. The head-symbol is computed with respect to the given transparency setting.

Return the lemmas that have the same head symbol of the given expression

(backward_chaining_core t insts max_depth pre_tactic leaf_tactic lemmas): perform backward chaining using the lemmas marked as [intro] and extra_lemmas.

The search maximum depth is \c max_depth.

Before processing each goal, the tactic pre_tactic is invoked. The possible outcomes are: 1) it closes the goal 2) it does nothing, and backward_chaining_core tries applicable lemmas. 3) it fails, and backward_chaining_core backtracks.

Whenever no lemma is applicable, the leaf_tactic is invoked, to try to close the goal. If insts is tt, then type class resolution is used to discharge goals.

Remark pre_tactic may also be used to trace the execution of backward_chaining_core

meta def tactic.back_chaining_core (pre_tactic leaf_tactic : tactic unit) (extra_lemmas : list expr) :