mathlib documentation

core.init.meta.simp_tactic

source
def simp.default_max_steps  :
ℕ

Equations
source
meta constant mk_simp_attr_decl_name (attr_name : name) :
name

Prefix the given attr_name with "simp_attr".

source
meta constant simp_lemmas  :
Type

Simp lemmas are used by the "simplifier" family of tactics. simp_lemmas is essentially a pair of tables rb_map (expr_type × name) (priority_list simp_lemma). One of the tables is for congruences and one is for everything else. An individual simp lemma is:

  • A kind which can be Refl, Simp or Congr.
  • A pair of exprs l ~> r. The rb map is indexed by the name of get_app_fn(l).
  • A proof that l = r or l ↔ r.
  • A list of the metavariables that must be filled before the proof can be applied.
  • A priority number
source
meta constant simp_lemmas.mk  :
simp_lemmas

Make a new table of simp lemmas

source
meta constant simp_lemmas.join (a a_1 : simp_lemmas) :
simp_lemmas

Merge the simp_lemma tables.

source
meta constant simp_lemmas.erase (a : simp_lemmas) (a_1 : list name) :
simp_lemmas

Remove the given lemmas from the table. Use the names of the lemmas.

source
meta constant simp_lemmas.mk_default  :
tactic simp_lemmas

Makes the default simp_lemmas table which is composed of all lemmas tagged with simp.

source
meta constant simp_lemmas.add (s : simp_lemmas) (e : expr) (symm : bool := to_bool false) :
tactic simp_lemmas

Add a simplification lemma by an expression p. Some conditions on p must hold for it to be added, see list below. If your lemma is not being added, you can see the reasons by setting set_option trace.simp_lemmas true.

  • p must have the type Π (h₁ : _) ... (hₙ : _), LHS ~ RHS for some reflexive, transitive relation (usually =).
  • Any of the hypotheses hᵢ should either be present in LHS or otherwise a Prop or a typeclass instance.
  • LHS should not occur within RHS.
  • LHS should not occur within a hypothesis hᵢ.
source
meta constant simp_lemmas.add_simp (s : simp_lemmas) (id : name) (symm : bool := to_bool false) :
tactic simp_lemmas

Add a simplification lemma by it's declaration name. See simp_lemmas.add for more information.

source
meta constant simp_lemmas.add_congr (a : simp_lemmas) (a_1 : name) :
tactic simp_lemmas

Adds a congruence simp lemma to simp_lemmas. A congruence simp lemma is a lemma that breaks the simplification down into separate problems. For example, to simplify a ∧ b to c ∧ d, we should try to simp a to c and b to d. For examples of congruence simp lemmas look for lemmas with the @[congr] attribute.

lemma if_simp_congr ... (h_c : b ↔ c) (h_t : x = u) (h_e : y = v) : ite b x y = ite c u v := ...
lemma imp_congr_right (h : a → (b ↔ c)) : (a → b) ↔ (a → c) := ...
lemma and_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∧ b) ↔ (c ∧ d) := ...
source
meta def simp_lemmas.append_with_symm (s : simp_lemmas) (hs : list (expr × bool)) :
tactic simp_lemmas

Add expressions to a set of simp lemmas using simp_lemmas.add.

This is the new version of simp_lemmas.append, which also allows you to set the symm flag.

source
meta def simp_lemmas.append (s : simp_lemmas) (hs : list expr) :
tactic simp_lemmas

Add expressions to a set of simp lemmas using simp_lemmas.add.

This is the backwards-compatibility version of simp_lemmas.append_with_symm, and sets all symm flags to ff.

source
meta constant simp_lemmas.rewrite (s : simp_lemmas) (e : expr) (prove : tactic unit := tactic.failed) (r : name := name.mk_string "eq" name.anonymous) (md : tactic.transparency := reducible) :
tactic (expr × expr)

simp_lemmas.rewrite s e prove R apply a simplification lemma from 's'

  • 'e' is the expression to be "simplified"
  • 'prove' is used to discharge proof obligations.
  • 'r' is the equivalence relation being used (e.g., 'eq', 'iff')

  • 'md' is the transparency; how aggresively should the simplifier perform reductions.

    Result (new_e, pr) is the new expression 'new_e' and a proof (pr : e R new_e)

source
meta constant simp_lemmas.rewrites (s : simp_lemmas) (e : expr) (prove : tactic unit := tactic.failed) (r : name := name.mk_string "eq" name.anonymous) (md : tactic.transparency := reducible) :
tactic (list (expr × expr))

source
meta constant simp_lemmas.drewrite (s : simp_lemmas) (e : expr) (md : tactic.transparency := reducible) :
tactic expr

simp_lemmas.drewrite s e tries to rewrite 'e' using only refl lemmas in 's'

source
meta constant is_valid_simp_lemma_cnst (a : name) :
tactic bool

source
meta constant is_valid_simp_lemma (a : expr) :
tactic bool

source
meta constant simp_lemmas.pp (a : simp_lemmas) :
tactic format

source
@[instance]
meta def simp_lemmas.has_to_tactic_format  :
has_to_tactic_format simp_lemmas

source
meta def tactic.revert_and_transform (transform : expr → tactic expr) (h : expr) :
tactic unit

Revert a local constant, change its type using transform.

source
meta def tactic.get_eqn_lemmas_for (deps : bool) (d : name) :
tactic (list name)

get_eqn_lemmas_for deps d returns the automatically generated equational lemmas for definition d. If deps is tt, then lemmas for automatically generated auxiliary declarations used to define d are also included.

source
structure tactic.dsimp_config  :
Type

source
meta constant simp_lemmas.dsimplify (s : simp_lemmas) (u : list name := list.nil) (e : expr) (cfg : tactic.dsimp_config := {md := reducible, max_steps := simp.default_max_steps, canonize_instances := tt, single_pass := ff, fail_if_unchanged := tt, eta := tt, zeta := tt, beta := tt, proj := tt, iota := tt, unfold_reducible := ff, memoize := tt}) :
tactic expr

(Definitional) Simplify the given expression using only reflexivity equality lemmas from the given set of lemmas. The resulting expression is definitionally equal to the input.

The list u contains defintions to be delta-reduced, and projections to be reduced.

source
meta constant tactic.dsimplify_core {α : Type} (a : α) (pre post : α → expr → tactic (α × expr × bool)) (e : expr) (cfg : tactic.dsimp_config := {md := reducible, max_steps := simp.default_max_steps, canonize_instances := tt, single_pass := ff, fail_if_unchanged := tt, eta := tt, zeta := tt, beta := tt, proj := tt, iota := tt, unfold_reducible := ff, memoize := tt}) :
tactic (α × expr)

source
meta def tactic.dsimplify (pre post : expr → tactic (expr × bool)) (a : expr) :
tactic expr

source
meta def tactic.get_simp_lemmas_or_default (a : option simp_lemmas) :
tactic simp_lemmas

source
meta def tactic.dsimp_target (s : option simp_lemmas := none) (u : list name := list.nil) (cfg : tactic.dsimp_config := {md := reducible, max_steps := simp.default_max_steps, canonize_instances := tt, single_pass := ff, fail_if_unchanged := tt, eta := tt, zeta := tt, beta := tt, proj := tt, iota := tt, unfold_reducible := ff, memoize := tt}) :
tactic unit

source
meta def tactic.dsimp_hyp (h : expr) (s : option simp_lemmas := none) (u : list name := list.nil) (cfg : tactic.dsimp_config := {md := reducible, max_steps := simp.default_max_steps, canonize_instances := tt, single_pass := ff, fail_if_unchanged := tt, eta := tt, zeta := tt, beta := tt, proj := tt, iota := tt, unfold_reducible := ff, memoize := tt}) :
tactic unit

source
meta constant tactic.dunfold_head (e : expr) (md : tactic.transparency := tactic.transparency.instances) :
tactic expr

Tries to unfold e if it is a constant or a constant application. Remark: this is not a recursive procedure.

source
structure tactic.dunfold_config  :
Type

source
meta constant tactic.dunfold (cs : list name) (e : expr) (cfg : tactic.dunfold_config := {to_dsimp_config := {md := tactic.transparency.instances, max_steps := simp.default_max_steps, canonize_instances := tt, single_pass := ff, fail_if_unchanged := tt, eta := tt, zeta := tt, beta := tt, proj := tt, iota := tt, unfold_reducible := ff, memoize := tt}}) :
tactic expr

source
meta def tactic.dunfold_target (cs : list name) (cfg : tactic.dunfold_config := {to_dsimp_config := {md := tactic.transparency.instances, max_steps := simp.default_max_steps, canonize_instances := tt, single_pass := ff, fail_if_unchanged := tt, eta := tt, zeta := tt, beta := tt, proj := tt, iota := tt, unfold_reducible := ff, memoize := tt}}) :
tactic unit

source
meta def tactic.dunfold_hyp (cs : list name) (h : expr) (cfg : tactic.dunfold_config := {to_dsimp_config := {md := tactic.transparency.instances, max_steps := simp.default_max_steps, canonize_instances := tt, single_pass := ff, fail_if_unchanged := tt, eta := tt, zeta := tt, beta := tt, proj := tt, iota := tt, unfold_reducible := ff, memoize := tt}}) :
tactic unit

source
structure tactic.delta_config  :
Type
  • max_steps : ℕ
  • visit_instances : bool

source
meta def tactic.delta (cs : list name) (e : expr) (cfg : tactic.delta_config := {max_steps := simp.default_max_steps, visit_instances := tt}) :
tactic expr

Delta reduce the given constant names

source
meta def tactic.delta_target (cs : list name) (cfg : tactic.delta_config := {max_steps := simp.default_max_steps, visit_instances := tt}) :
tactic unit

source
meta def tactic.delta_hyp (cs : list name) (h : expr) (cfg : tactic.delta_config := {max_steps := simp.default_max_steps, visit_instances := tt}) :
tactic unit

source
structure tactic.unfold_proj_config  :
Type

source
meta constant tactic.unfold_proj (e : expr) (md : tactic.transparency := tactic.transparency.instances) :
tactic expr

If e is a projection application, try to unfold it, otherwise fail.

source
meta def tactic.unfold_projs (e : expr) (cfg : tactic.unfold_proj_config := {to_dsimp_config := {md := tactic.transparency.instances, max_steps := simp.default_max_steps, canonize_instances := tt, single_pass := ff, fail_if_unchanged := tt, eta := tt, zeta := tt, beta := tt, proj := tt, iota := tt, unfold_reducible := ff, memoize := tt}}) :
tactic expr

source
meta def tactic.unfold_projs_target (cfg : tactic.unfold_proj_config := {to_dsimp_config := {md := tactic.transparency.instances, max_steps := simp.default_max_steps, canonize_instances := tt, single_pass := ff, fail_if_unchanged := tt, eta := tt, zeta := tt, beta := tt, proj := tt, iota := tt, unfold_reducible := ff, memoize := tt}}) :
tactic unit

source
meta def tactic.unfold_projs_hyp (h : expr) (cfg : tactic.unfold_proj_config := {to_dsimp_config := {md := tactic.transparency.instances, max_steps := simp.default_max_steps, canonize_instances := tt, single_pass := ff, fail_if_unchanged := tt, eta := tt, zeta := tt, beta := tt, proj := tt, iota := tt, unfold_reducible := ff, memoize := tt}}) :
tactic unit

source
structure tactic.simp_config  :
Type

source
meta constant tactic.simplify (s : simp_lemmas) (to_unfold : list name := list.nil) (e : expr) (cfg : tactic.simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, iota_eqn := ff, constructor_eq := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}) (r : name := name.mk_string "eq" name.anonymous) (discharger : tactic unit := tactic.failed) :
tactic (expr × expr)

simplify s e cfg r prove simplify e using s using bottom-up traversal. discharger is a tactic for dischaging new subgoals created by the simplifier. If it fails, the simplifier tries to discharge the subgoal by simplifying it to true.

The parameter to_unfold specifies definitions that should be delta-reduced, and projection applications that should be unfolded.

source
meta def tactic.simp_target (s : simp_lemmas) (to_unfold : list name := list.nil) (cfg : tactic.simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, iota_eqn := ff, constructor_eq := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}) (discharger : tactic unit := tactic.failed) :
tactic unit

source
meta def tactic.simp_hyp (s : simp_lemmas) (to_unfold : list name := list.nil) (h : expr) (cfg : tactic.simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, iota_eqn := ff, constructor_eq := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}) (discharger : tactic unit := tactic.failed) :
tactic expr

source
meta constant tactic.ext_simplify_core {α : Type} (a : α) (c : tactic.simp_config) (s : simp_lemmas) (discharger : α → tactic α) (pre post : α → simp_lemmas → name → option expr → expr → tactic (α × expr × option expr × bool)) (r : name) (a_1 : expr) :
tactic (α × expr × expr)

ext_simplify_core a c s discharger pre post r e:

  • a : α - initial user data
  • c : simp_config - simp configuration options
  • s : simp_lemmas - the set of simp_lemmas to use. Remark: the simplification lemmas are not applied automatically like in the simplify tactic. The caller must use them at pre/post.
  • discharger : α → tactic α - tactic for dischaging hypothesis in conditional rewriting rules. The argument 'α' is the current user data.
  • pre a s r p e is invoked before visiting the children of subterm 'e'.
    • arguments:
    • a is the current user data
    • s is the updated set of lemmas if 'contextual' is tt,
    • r is the simplification relation being used,
    • p is the "parent" expression (if there is one).
    • e is the current subexpression in question.
    • if it succeeds the result is (new_a, new_e, new_pr, flag) where
    • new_a is the new value for the user data
    • new_e is a new expression s.t. r e new_e
    • new_pr is a proof for e r new_e, If it is none, the proof is assumed to be by reflexivity
    • flag if tt new_e children should be visited, and post invoked.
  • (post a s r p e) is invoked after visiting the children of subterm e, The output is similar to (pre a r s p e), but the 'flag' indicates whether the new expression should be revisited or not.
  • r is the simplification relation. Usually = or ↔.
  • e is the input expression to be simplified.

The method returns (a,e,pr) where

  • a is the final user data
  • e is the new expression
  • pr is the proof that the given expression equals the input expression.
source
meta def tactic.collect_ctx_simps  :
tactic (list expr)

source
meta def tactic.intro1_aux (a : bool) (a_1 : list name) :
tactic expr

source
structure tactic.simp_intros_config  :
Type

source
meta def tactic.simp_intros_aux (cfg : tactic.simp_config) (use_hyps : bool) (to_unfold : list name) (a : simp_lemmas) (a_1 : bool) (a_2 : list name) :
tactic simp_lemmas

source
meta def tactic.simp_intros (s : simp_lemmas) (to_unfold ids : list name := list.nil) (cfg : tactic.simp_intros_config := {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, iota_eqn := ff, constructor_eq := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, use_hyps := ff}) :
tactic unit

source
meta def tactic.mk_eq_simp_ext (simp_ext : expr → tactic (expr × expr)) :
tactic unit

source
meta def tactic.to_simp_lemmas (a : simp_lemmas) (a_1 : list name) :
tactic simp_lemmas

source
meta def tactic.mk_simp_attr (attr_name : name) (attr_deps : list name := list.nil) :
tactic unit

source
meta def tactic.get_user_simp_lemmas (attr_name : name) :
tactic simp_lemmas

Example usage:

-- make a new simp attribute called "my_reduction"
run_cmd mk_simp_attr `my_reduction
-- Add "my_reduction" attributes to these if-reductions
attribute [my_reduction] if_pos if_neg dif_pos dif_neg

-- will return the simp_lemmas with the `my_reduction` attribute.
#eval get_user_simp_lemmas `my_reduction
source
meta def tactic.join_user_simp_lemmas_core (a : simp_lemmas) (a_1 : list name) :
tactic simp_lemmas

source
meta def tactic.join_user_simp_lemmas (no_dflt : bool) (attrs : list name) :
tactic simp_lemmas

source
meta def tactic.simplify_top_down {α : Type} (a : α) (pre : α → expr → tactic (α × expr × expr)) (e : expr) (cfg : tactic.simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, iota_eqn := ff, constructor_eq := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}) :
tactic (α × expr × expr)

source
meta def tactic.simp_top_down (pre : expr → tactic (expr × expr)) (cfg : tactic.simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, iota_eqn := ff, constructor_eq := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}) :
tactic unit

source
meta def tactic.simplify_bottom_up {α : Type} (a : α) (post : α → expr → tactic (α × expr × expr)) (e : expr) (cfg : tactic.simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, iota_eqn := ff, constructor_eq := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}) :
tactic (α × expr × expr)

source
meta def tactic.simp_bottom_up (post : expr → tactic (expr × expr)) (cfg : tactic.simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, iota_eqn := ff, constructor_eq := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}) :
tactic unit

source
meta def tactic.non_dep_prop_hyps  :
tactic (list expr)

source
meta structure tactic.simp_all_entry  :
Type

source
meta def tactic.simp_all (s : simp_lemmas) (to_unfold : list name) (cfg : tactic.simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, iota_eqn := ff, constructor_eq := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}) (discharger : tactic unit := tactic.failed) :
tactic unit

source
meta constant tactic.trace_algebra_info (a : expr) :
tactic unit

source
meta def simp_attr.norm  :
(user_attribute simp_lemmas)