namespace affects behaviour of `apply_list_expr`

Stream: general

[Heather Macbeth]

In the following example, opening the namespace nat affects the ability of docs#tactic.apply_list_expr to function. Can anyone suggest a fix?

import tactic.core
import data.int.basic

open tactic

@[user_attribute]
meta def foo : user_attribute :=
{ name := `foo,
  descr := "" }

attribute [foo] pow_lt_pow_of_lt_left

meta def minitac : tactic unit := do
  foo_rules ← resolve_attribute_expr_list `foo,
  trace foo_rules.length,
  apply_list_expr {md := reducible} foo_rules

example {x y : ℤ} (n : ℕ) :
  x ^ n < y ^ n :=
begin
  minitac, -- desired behaviour
end

open nat

example {x y : ℤ} (n : ℕ) :
  x ^ n < y ^ n :=
begin
  minitac, -- "no matching rule"
end

[Heather Macbeth]

I'm assuming the problem is in docs#tactic.apply_list_expr rather than docs#tactic.resolve_attribute_expr_list, because of the output of the trace.

[Alex J. Best]

Actually I think the problem is the calls to docs#tactic.resolve_name in docs#tactic.resolve_attribute_expr_list, you get a name clash between docs#pow_lt_pow_of_lt_left and docs#nat.pow_lt_pow_of_lt_left.
The following version has the desired behaviour:

import tactic.core
import data.int.basic

open tactic
.

@[user_attribute]
meta def foo : user_attribute :=
{ name := `foo,
  descr := "" }

attribute [foo] pow_lt_pow_of_lt_left

meta def resolve_attribute_expr_list' (attr_name : name) : tactic (list (tactic expr)) := do
  l ← attribute.get_instances attr_name,
  list.map i_to_expr_for_apply <$> list.reverse <$> l.mmap (λ n, do c ← (mk_const n), return (pexpr.of_expr c))

meta def tactic.interactive.minitac : tactic unit := do
  foo_rules ← resolve_attribute_expr_list' `foo,
  trace foo_rules.length,
  apply_list_expr {md := reducible} foo_rules

example {x y : ℤ} (n : ℕ) :
  x ^ n < y ^ n :=
begin
  minitac, -- desired behaviour
end

open nat

example {x y : ℤ} (n : ℕ) :
  x ^ n < y ^ n :=
begin
  minitac,
end

[Heather Macbeth]

Huh! So should

list.map i_to_expr_for_apply <$> list.reverse <$> l.mmap resolve_name

be replaced by

list.map i_to_expr_for_apply <$> list.reverse <$> l.mmap (λ n, do c ← (mk_const n), return (pexpr.of_expr c))

in tactic#resolve_attribute_expr_list ?

[Alex J. Best]

Looks like resolve_attribute_expr_list is only used in one place, which is apply_rules, which seems more general, so I wouldn't say so without looking a lot deeper

[Alex J. Best]

meta def resolve_attribute_expr_list' (attr_name : name) : tactic (list (tactic expr)) := do
  l ← attribute.get_instances attr_name,
  l.reverse.mmap (λ n, return (mk_const n))

is probably a shorter way

[Heather Macbeth]

Indeed, I am using it for an apply_rules-like function.

[Heather Macbeth]

Well, if I make the change in a branch and it doesn't break anything in mathlib, is that enough evidence to PR it?

[Alex J. Best]

Could be, but I also don't really see an issue with having similar but slightly different tactic internals around if they have slightly different purposes. Of course if you can reproduce the original issue with apply rules then thats a bug that should be fixed
We should also ask @Rob Lewis if he has a particular reason to write it this way, the comments in the source of apply rules make it seem like the setup was carefully chosen, though out of context it does seem a bit odd (e.g. returning a list of tactic exprs)

[Alex J. Best]

Actually the bug does seem to be there for apply rules, or at least the error message is unhelpful

open nat

example {x y : ℤ} (n : ℕ) :
  x ^ n < y ^ n :=
begin
  apply_rules [pow_lt_pow_of_lt_left],
end

[Heather Macbeth]

Indeed, it's exactly the same behaviour for apply_rules.

import tactic.core
import data.int.basic

open tactic

@[user_attribute]
meta def foo : user_attribute :=
{ name := `foo,
  descr := "" }

attribute [foo] pow_lt_pow_of_lt_left

example {x y : ℤ} (n : ℕ) :
  x ^ n < y ^ n :=
begin
  apply_rules with foo, -- desired behaviour
end

open nat

example {x y : ℤ} (n : ℕ) :
  x ^ n < y ^ n :=
begin
  apply_rules with foo, -- "no matching rule"
end

[Alex J. Best]

So that should be fixed, but I'm not sure the fix is the same as in your case, where you know precisely which declaration you want to apply, as its the one given to you by the attribute, so there is never a need to resolve the name

[Heather Macbeth]

Maybe, at least, this should be the behaviour for apply_rules when it is used with an attribute (as here).

[Alex J. Best]

For apply rules what should probably happen is it tells the user, hey you gave me an ambiguous name, please specify this more, rather than "no matching rule"

[Alex J. Best]

Oh I see, yeah thats more similar to your tactic, so maybe there should be different internals

[Heather Macbeth]

Do you mean, different internals for apply_rules with an attribute vs with a user-specified lemma?

[Alex J. Best]

Yeah I think that you make the most sense, after all one has the possibility of ambiguity, that we want to ask the user to fix, but the other should just work

[Heather Macbeth]

Thanks! It's slightly above my pay grade, unfortunately. I'll open an issue.

[Heather Macbeth]

And also ping @Scott Morrison who I think is doing the mathlib4 port.

[Alex J. Best]

Actually looking at it more it seems your original suggestion is fine, resolve_attribute_expr_list is only used for the ones supplied via attribute anyway, so making the change there should be ok

[Heather Macbeth]

Oh, ok! Then I think I can do that myself.

[Alex J. Best]

Sorry for the confusion! Took me a minute to wrap my head around the way it is set up

[Heather Macbeth]

(Or you can if you prefer, it's your line of code)

[Alex J. Best]

Please go ahead (I'm about to log off for the night anyways)! I think the

list.map i_to_expr_for_apply <$> list.reverse <$> l.mmap (λ n, do c ← (mk_const n), return (pexpr.of_expr c))

version is maybe better after looking at this more

[Heather Macbeth]

#16827

[Eric Wieser]

Why does apply_rules take a list of names and not pexprs?

[Eric Wieser]

Then the name resolution would just be automatic like it is for rw

[Notification Bot]

Chris Hughes has marked this topic as resolved.

[Notification Bot]

Chris Hughes has marked this topic as unresolved.