monotonicity.attr with apply_rules

Stream: general

[Heather Macbeth]

The tactic apply_rules works with sets of lemmas defined by a user attribute. The example given in the documentation of apply_rules is that you could make a custom monotonicity attribute and then use apply_rules with it, and that indeed works just fine.

import algebra.order.group

variables {α : Type*} [linear_ordered_add_comm_group α]

@[user_attribute]
meta def mono_rules : user_attribute :=
{ name := `mono_rules,
  descr := "lemmas usable to prove monotonicity" }

local attribute [mono_rules] add_le_add

example (a b c d : α) : a + b ≤ c + d :=
begin
  apply_rules mono_rules, -- takes action
end

So I figured, we already have an attribute mono from the monotonicity tactic for this use case, why not use that? But when I tried the experiment it didn't work. Any ideas?

import tactic.monotonicity

variables {α : Type*} [linear_ordered_add_comm_group α]

example (a b c d : α) : a + b ≤ c + d :=
begin
  apply_rules tactic.interactive.monotonicity.attr, -- `no matching rule`
end

[Heather Macbeth]

I wanted to :ping_pong: this question about getting a user attribute to work. Maybe @Gabriel Ebner or @Rob Lewis knows the answer?

[Rob Lewis]

It looks like a bug in apply_rules. It should work based on the name field of the user attribute, so apply_rules mono should work. But it seems to fail unless the name of the user attribute and the name field are the same. I've starred this message but won't have time to try to fix this week.