mathlib documentation

tactic.rewrite

meta def tactic.match_fn (fn : expr) :

expr → tactic (expr × expr)

meta def tactic.fill_args :

expr → tactic (expr × list expr)

meta def tactic.mk_assoc_pattern' (fn : expr) :

expr → tactic (dlist expr)

meta def tactic.mk_assoc_pattern (fn e : expr) :

tactic (list expr)

meta def tactic.mk_assoc (fn : expr) :

list expr → tactic expr

meta def tactic.chain_eq_trans :

list expr → tactic expr

meta def tactic.unify_prefix :

list expr → list expr → tactic unit

meta def tactic.match_assoc_pattern' (p : list expr) :

list expr → tactic (list expr × list expr)

meta def tactic.match_assoc_pattern (fn p e : expr) :

tactic (list expr × list expr)

def tactic.id_tag.assoc_proof :

Tag for proofs generated by assoc_rewrite.

Equations

tactic.id_tag.assoc_proof = ()

meta def tactic.mk_eq_proof (fn : expr) (e₀ e₁ : list expr) (p : expr) :

tactic (expr × expr × expr)

meta def tactic.assoc_root (fn assoc : expr) :

expr → tactic (expr × expr)

meta def tactic.assoc_refl' (fn assoc : expr) :

expr → expr → tactic expr

meta def tactic.assoc_refl (fn : expr) :

meta def tactic.flatten (fn assoc e : expr) :

tactic (expr × expr)

meta def tactic.assoc_rewrite_intl (assoc h e : expr) :

tactic (expr × expr)

meta def tactic.enum_assoc_subexpr' (fn : expr) :

expr → tactic (dlist expr)

meta def tactic.enum_assoc_subexpr (fn e : expr) :

tactic (list expr)

meta def tactic.mk_assoc_instance (fn : expr) :

meta def tactic.assoc_rewrite (h e : expr) (opt_assoc : option expr := none) :

tactic (expr × expr × list expr)

meta def tactic.assoc_rewrite_target (h : expr) (opt_assoc : option expr := none) :

meta def tactic.assoc_rewrite_hyp (h hyp : expr) (opt_assoc : option expr := none) :

meta def tactic.interactive.assoc_rewrite (q : interactive.parse tactic.interactive.rw_rules) (l : interactive.parse interactive.types.location) :

assoc_rewrite [h₀,← h₁] at ⊢ h₂ behaves like rewrite [h₀,← h₁] at ⊢ h₂ with the exception that associativity is used implicitly to make rewriting possible.

It works for any function f for which an is_associative f instance can be found.

example {α : Type*} (f : α → α → α) [is_associative α f] (a b c d x : α) :
  let infix `~` := f in
  b ~ c = x → (a ~ b ~ c ~ d) = (a ~ x ~ d) :=
begin
  intro h,
  assoc_rw h,
end

meta def tactic.interactive.assoc_rw (q : interactive.parse tactic.interactive.rw_rules) (l : interactive.parse interactive.types.location) :

synonym for assoc_rewrite