mathlib3 documentation

tactic.rewrite

Tag for proofs generated by assoc_rewrite.

Equations
meta def tactic.mk_eq_proof (fn : expr) (e₀ e₁ : list expr) (p : expr) :
meta def tactic.assoc_root (fn assoc : expr) :
meta def tactic.assoc_refl' (fn assoc : expr) :
meta def tactic.assoc_refl (fn : expr) :
meta def tactic.flatten (fn assoc e : expr) :
meta def tactic.assoc_rewrite_intl (assoc h e : expr) :
meta def tactic.assoc_rewrite_hyp (h hyp : expr) (opt_assoc : option expr := option.none) :

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

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