core / init.meta.backward

meta constant tactic.mk_back_lemmas_core :

tactic.transparency → tactic 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.

source

meta constant tactic.back_lemmas_insert_core :

tactic.transparency → tactic.back_lemmas → expr → tactic tactic.back_lemmas

(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.

source

meta constant tactic.back_lemmas_find :

tactic.back_lemmas → expr → tactic (list expr)

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

source

meta def tactic.mk_back_lemmas :

tactic tactic.back_lemmas

source

meta def tactic.back_lemmas_insert :

tactic.back_lemmas → expr → tactic tactic.back_lemmas

source

meta constant tactic.backward_chaining_core :

tactic.transparency → bool → ℕ → tactic unit → tactic unit → tactic.back_lemmas → tactic unit

(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

source

meta def tactic.back_lemmas_add_extra :

tactic.transparency → tactic.back_lemmas → list expr → tactic tactic.back_lemmas

source

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

tactic unit

source

meta def tactic.back_chaining :

tactic unit

source

meta def tactic.back_chaining_using :

list expr → tactic unit

source

meta def tactic.back_chaining_using_hs :

tactic unit