core / init.meta.simp_tactic

source

def simp.default_max_steps :

ℕ

Equations

simp.default_max_steps = 10000000

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 :

simp_lemmas → simp_lemmas → simp_lemmas

Merge the simp_lemma tables.

source

meta constant simp_lemmas.erase :

simp_lemmas → 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 :

simp_lemmas → 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 :

name → tactic bool

source

meta constant is_valid_simp_lemma :

expr → tactic bool

source

meta constant simp_lemmas.pp :

simp_lemmas → tactic format

source

@[protected, 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

md : tactic.transparency
max_steps : ℕ
canonize_instances : bool
single_pass : bool
fail_if_unchanged : bool
eta : bool
zeta : bool
beta : bool
proj : bool
iota : bool
unfold_reducible : bool
memoize : bool

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)) :

expr → tactic expr

source

meta def tactic.get_simp_lemmas_or_default :

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

to_dsimp_config : tactic.dsimp_config

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

to_dsimp_config : tactic.dsimp_config

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

max_steps : ℕ
contextual : bool
lift_eq : bool
canonize_instances : bool
canonize_proofs : bool
use_axioms : bool
zeta : bool
beta : bool
eta : bool
proj : bool
iota : bool
iota_eqn : bool
constructor_eq : bool
single_pass : bool
fail_if_unchanged : bool
memoize : bool
trace_lemmas : bool

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, trace_lemmas := ff}) (r : name := name.mk_string "eq" name.anonymous) (discharger : tactic unit := tactic.failed) :

tactic (expr × expr × name_set)

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, trace_lemmas := ff}) (discharger : tactic unit := tactic.failed) :

tactic name_set

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, trace_lemmas := ff}) (discharger : tactic unit := tactic.failed) :

tactic (expr × name_set)

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) :

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 r e 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.

Note that ext_simplify_core will succeed even if pre and post fail, as failures are used to indicate that the method should move on to the next subterm. If it is desirable to propagate errors from pre, they can be propagated through the "user data". An easy way to do this is to call tactic.capture (do ...) in the parts of pre/post where errors matter, and then use tactic.unwrap a on the result.

Additionally, ext_simplify_core does not propagate changes made to the tactic state by pre and post. If it is desirable to propagate changes to the tactic state in addition to errors, usetactic.resumeinstead oftactic.unwrap`.

source

meta def tactic.collect_ctx_simps :

tactic (list expr)

source

meta def tactic.intro1_aux :

bool → list name → tactic expr

source

structure tactic.simp_intros_config :

Type

to_simp_config : tactic.simp_config
use_hyps : bool

source

meta def tactic.simp_intros_aux (cfg : tactic.simp_config) (use_hyps : bool) (to_unfold : list name) :

simp_lemmas → bool → 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, trace_lemmas := ff}, 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 :

simp_lemmas → 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

```