mathlib documentation

core / init.meta.smt.smt_tactic

structure smt_pre_config  :
Type

Configuration for the smt tactic preprocessor. The preprocessor is applied whenever a new hypothesis is introduced.

  • simp_attr: is the attribute name for the simplification lemmas that are used during the preprocessing step.

  • max_steps: it is the maximum number of steps performed by the simplifier.

  • zeta: if tt, then zeta reduction (i.e., unfolding let-expressions) is used during preprocessing.

structure smt_config  :
Type

Configuration for the smt_state object.

  • em_attr: is the attribute name for the hinst_lemmas that are used for ematching
meta constant smt_goal  :
Type
meta def smt_state  :
Type
meta constant smt_state.classical  :

Return tt iff classical excluded middle was enabled at smt_state.mk

meta def smt_tactic (α : Type) :
Type
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
meta constant tactic_to_smt_tactic (α : Type) :
tactic αsmt_tactic α
@[protected, instance]
@[protected, instance]
meta def smt_tactic.has_coe (α : Type) :
@[protected, instance]
meta constant smt_tactic.intron  :
meta constant smt_tactic.close  :

Try to close main goal by using equalities implied by the congruence closure module.

meta constant smt_tactic.ematch_core  :

Produce new facts using heuristic lemma instantiation based on E-matching. This tactic tries to match patterns from lemmas in the main goal with terms in the main goal. The set of lemmas is populated with theorems tagged with the attribute specified at smt_config.em_attr, and lemmas added using tactics such as smt_tactic.add_lemmas. The current set of lemmas can be retrieved using the tactic smt_tactic.get_lemmas.

Remark: the given predicate is applied to every new instance. The instance is only added to the state if the predicate returns tt.

Produce new facts using heuristic lemma instantiation based on E-matching. This tactic tries to match patterns from the given lemmas with terms in the main goal.

meta constant smt_tactic.preprocess  :

Preprocess the given term using the same simplifications rules used when we introduce a new hypothesis. The result is pair containing the resulting term and a proof that it is equal to the given one.

meta def smt_tactic.failed {α : Type} :
meta def smt_tactic.fail {α : Type} {β : Type u} [has_to_format β] (msg : β) :
meta def smt_tactic.try {α : Type} (t : smt_tactic α) :

iterate_at_most n t: repeat the given tactic at most n times or until t fails

iterate_exactly n t : execute t n times

meta def smt_tactic.slift_aux {α : Type} (t : tactic α) (cfg : smt_config) :
meta def smt_tactic.slift {α : Type} (t : tactic α) :

This lift operation will restart the SMT state. It is useful for using tactics that change the set of hypotheses.

meta def smt_tactic.trace {α : Type} [has_to_tactic_format α] (a : α) :
meta def smt_tactic.to_expr (q : pexpr) (allow_mvars : bool := tt) :

Apply the given tactic to all goals.

meta def smt_tactic.seq (tac1 tac2 : smt_tactic unit) :

LCF-style AND_THEN tactic. It applies tac1, and if succeed applies tac2 to each subgoal produced by tac1

meta def smt_tactic.focus1 {α : Type} (tac : smt_tactic α) :
meta def smt_tactic.assert (h : name) (t : expr) :

Add a new goal for t, and the hypothesis (h : t) in the current goal.

meta def smt_tactic.assertv (h : name) (t v : expr) :

Add the hypothesis (h : t) in the current goal if v has type t.

meta def smt_tactic.define (h : name) (t : expr) :

Add a new goal for t, and the hypothesis (h : t := ?M) in the current goal.

meta def smt_tactic.definev (h : name) (t v : expr) :

Add the hypothesis (h : t := v) in the current goal if v has type t.

meta def smt_tactic.pose (h : name) (t : option expr := none) (pr : expr) :

Add (h : t := pr) to the current goal

meta def smt_tactic.note (h : name) (t : option expr := none) (pr : expr) :

Add (h : t) to the current goal, given a proof (pr : t)

Return a proof for e, if 'e' is a known fact in the main goal.

Return a refutation for e (i.e., a proof for (not e)), if 'e' has been refuted in the main goal.

meta def smt_tactic.when (c : Prop) [decidable c] (tac : smt_tactic unit) :
meta def using_smt {α : Type} (t : smt_tactic α) (cfg : smt_config := {cc_cfg := {ignore_instances := tt, ac := tt, ho_fns := none (list name), em := tt}, em_cfg := {max_instances := 10000, max_generation := 10}, pre_cfg := {simp_attr := name.mk_string "pre_smt" name.anonymous, max_steps := 1000000, zeta := ff}, em_attr := name.mk_string "ematch" name.anonymous}) :
meta def using_smt_with {α : Type} (cfg : smt_config) (t : smt_tactic α) :