mathlib documentation

core / init.meta.smt.smt_tactic

source
meta def simp_attr.pre_smt  :
(user_attribute simp_lemmas)
source
meta def ematch_lhs  :
(user_attribute hinst_lemmas)
source
meta def ematch  :
(user_attribute hinst_lemmas)
source
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.

source
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
source
meta def smt_config.set_classical (c : smt_config) (b : bool) :
smt_config
source
meta constant smt_goal  :
Type
source
meta def smt_state  :
Type
source
meta constant smt_state.mk  :
smt_config → tactic smt_state
source
meta constant smt_state.to_format  :
smt_state → tactic_state → format
source
meta constant smt_state.classical  :
smt_state → bool

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

source
meta def smt_tactic (α : Type) :
Type
source
@[protected, instance]
meta def smt_state.has_append  :
has_append smt_state
source
@[protected, instance]
meta def smt_tactic.monad  :
monad smt_tactic
source
@[protected, instance]
meta def smt_tactic.alternative  :
alternative smt_tactic
source
@[protected, instance]
meta def smt_tactic.monad_state  :
monad_state smt_state smt_tactic
source
meta constant tactic_to_smt_tactic (α : Type) :
tactic α → smt_tactic α
source
@[protected, instance]
meta def smt_tactic.has_monad_lift  :
has_monad_lift tactic smt_tactic
source
@[protected, instance]
meta def smt_tactic.has_coe (α : Type) :
has_coe (tactic α) (smt_tactic α)
source
@[protected, instance]
meta def smt_tactic.monad_fail  :
monad_fail smt_tactic
source
meta constant smt_tactic.intros  :
smt_tactic unit
source
meta constant smt_tactic.intron  :
ℕ → smt_tactic unit
source
meta constant smt_tactic.intro_lst  :
list name → smt_tactic unit
source
meta constant smt_tactic.close  :
smt_tactic unit

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

source
meta constant smt_tactic.ematch_core  :
(expr → bool) → smt_tactic unit

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.

source
meta constant smt_tactic.ematch_using  :
hinst_lemmas → smt_tactic unit

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.

source
meta constant smt_tactic.mk_ematch_eqn_lemmas_for_core  :
tactic.transparency → name → smt_tactic hinst_lemmas
source
meta constant smt_tactic.to_cc_state  :
smt_tactic cc_state
source
meta constant smt_tactic.to_em_state  :
smt_tactic ematch_state
source
meta constant smt_tactic.get_config  :
smt_tactic smt_config
source
meta constant smt_tactic.preprocess  :
expr → smt_tactic (expr × expr)

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.

source
meta constant smt_tactic.get_lemmas  :
smt_tactic hinst_lemmas
source
meta constant smt_tactic.set_lemmas  :
hinst_lemmas → smt_tactic unit
source
meta constant smt_tactic.add_lemmas  :
hinst_lemmas → smt_tactic unit
source
meta def smt_tactic.add_ematch_lemma_core (md : tactic.transparency) (as_simp : bool) (e : expr) :
smt_tactic unit
source
meta def smt_tactic.add_ematch_lemma_from_decl_core (md : tactic.transparency) (as_simp : bool) (n : name) :
smt_tactic unit
source
meta def smt_tactic.add_ematch_eqn_lemmas_for_core (md : tactic.transparency) (n : name) :
smt_tactic unit
source
meta def smt_tactic.ematch  :
smt_tactic unit
source
meta def smt_tactic.failed {α : Type} :
smt_tactic α
source
meta def smt_tactic.fail {α : Type} {β : Type u} [has_to_format β] (msg : β) :
smt_tactic α
source
meta def smt_tactic.try {α : Type} (t : smt_tactic α) :
smt_tactic unit
source
meta def smt_tactic.iterate_at_most  :
ℕ → smt_tactic unit → smt_tactic unit

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

source
meta def smt_tactic.iterate_exactly  :
ℕ → smt_tactic unit → smt_tactic unit

iterate_exactly n t : execute t n times

source
meta def smt_tactic.iterate  :
smt_tactic unit → smt_tactic unit
source
meta def smt_tactic.eblast  :
smt_tactic unit
source
@[protected]
meta def smt_tactic.read  :
smt_tactic (smt_state × tactic_state)
source
@[protected]
meta def smt_tactic.write  :
smt_state × tactic_state → smt_tactic unit
source
meta def smt_tactic.slift_aux {α : Type} (t : tactic α) (cfg : smt_config) :
smt_tactic α
source
meta def smt_tactic.slift {α : Type} (t : tactic α) :
smt_tactic α

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

source
meta def smt_tactic.trace_state  :
smt_tactic unit
source
meta def smt_tactic.trace {α : Type} [has_to_tactic_format α] (a : α) :
smt_tactic unit
source
meta def smt_tactic.to_expr (q : pexpr) (allow_mvars : bool := tt) :
smt_tactic expr
source
meta def smt_tactic.classical  :
smt_tactic bool
source
meta def smt_tactic.num_goals  :
smt_tactic ℕ
source
meta def smt_tactic.get_goals  :
smt_tactic (list smt_goal × list expr)
source
meta def smt_tactic.set_goals  :
list smt_goal → list expr → smt_tactic unit
source
meta def smt_tactic.all_goals (tac : smt_tactic unit) :
smt_tactic unit

Apply the given tactic to all goals.

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

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

source
@[protected, instance]
meta def smt_tactic.has_andthen  :
has_andthen (smt_tactic unit) (smt_tactic unit) (smt_tactic unit)
source
meta def smt_tactic.focus1 {α : Type} (tac : smt_tactic α) :
smt_tactic α
source
meta def smt_tactic.solve1 (tac : smt_tactic unit) :
smt_tactic unit
source
meta def smt_tactic.swap  :
smt_tactic unit
source
meta def smt_tactic.assert (h : name) (t : expr) :
smt_tactic unit

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

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

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

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

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

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

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

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

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

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

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

source
meta def smt_tactic.destruct (e : expr) :
smt_tactic unit
source
meta def smt_tactic.by_cases (e : expr) :
smt_tactic unit
source
meta def smt_tactic.by_contradiction  :
smt_tactic unit
source
meta def smt_tactic.proof_for (e : expr) :
smt_tactic expr

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

source
meta def smt_tactic.refutation_for (e : expr) :
smt_tactic expr

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

source
meta def smt_tactic.get_facts  :
smt_tactic (list expr)
source
meta def smt_tactic.get_refuted_facts  :
smt_tactic (list expr)
source
meta def smt_tactic.add_ematch_lemma  :
expr → smt_tactic unit
source
meta def smt_tactic.add_ematch_lhs_lemma  :
expr → smt_tactic unit
source
meta def smt_tactic.add_ematch_lemma_from_decl  :
name → smt_tactic unit
source
meta def smt_tactic.add_ematch_lhs_lemma_from_decl  :
name → smt_tactic unit
source
meta def smt_tactic.add_ematch_eqn_lemmas_for  :
name → smt_tactic unit
source
meta def smt_tactic.add_lemmas_from_facts_core  :
list expr → smt_tactic unit
source
meta def smt_tactic.add_lemmas_from_facts  :
smt_tactic unit
source
meta def smt_tactic.induction (e : expr) (ids : list name := list.nil) (rec : option name := none) :
smt_tactic unit
source
meta def smt_tactic.when (c : Prop) [decidable c] (tac : smt_tactic unit) :
smt_tactic unit
source
meta def smt_tactic.when_tracing (n : name) (tac : smt_tactic unit) :
smt_tactic unit
source
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}) :
tactic α
source
meta def using_smt_with {α : Type} (cfg : smt_config) (t : smt_tactic α) :
tactic α