Zulip Chat Archive

Stream: general

Topic: monotonicity.attr with apply_rules

Heather Macbeth (Mar 28 2022 at 01:29):

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 α]

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 :=
  apply_rules mono_rules, -- takes action

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 :=
  apply_rules tactic.interactive.monotonicity.attr, -- `no matching rule`

Heather Macbeth (Mar 29 2022 at 21:20):

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 (Mar 30 2022 at 02:36):

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.

Last updated: Aug 03 2023 at 10:10 UTC