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
def
tactic.interactive.assoc_rw
(q : interactive.parse tactic.interactive.rw_rules)
(l : interactive.parse interactive.types.location) :
synonym for assoc_rewrite