tactic with one "input"

Stream: new members

[Heather Macbeth]

I watched some of Rob's videos and decided to try to make a baby tactic, which does the same thing as rw but fails if this doesn't close the goal. I tried

meta def rw1 (a : expr) := `[solve1 { rw %%a }]

and this gave the error "kernel failed to type check declaration 'rw1' this is usually due to a buggy tactic or a bug in the builtin elaborator". What am I doing wrong?

[Logan Murphy]

(deleted)

[Logan Murphy]

albeit not the tactic you're looking for

[Kyle Miller]

I'm not sure how to debug that, but another way is to take the definition for tactic.interactive.rw and replace its innards with running tactic.interactive.rw with the parsed arguments and using what tactic.interactive.solve1 uses:

import tactic

namespace tactic.interactive
open interactive interactive.types tactic

meta def rw1 (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {}) : tactic unit :=
tactic.solve1 $ tactic.interactive.rw q l cfg

end tactic.interactive

example (n m : ℕ) (h : n + 2 = m) : n.succ + 1 = m :=
begin
  rw1 nat.succ_eq_add_one,
  /- solve1 tactic failed, focused goal has not been solved -/
end

example (n m : ℕ) (h : n + 2 = m) : n.succ + 1 = m :=
begin
  rw1 [nat.succ_eq_add_one, h],
end

[Heather Macbeth]

Thank you, Kyle! This is really instructive.

[Ashley Blacquiere]

The following works, but isn't probably very useful for your purposes:

meta def rw1 := `[solve1 { rw h }]

example (n m : ℕ) (h : n + 2 = m) : n.succ + 1 = m :=
by rw1

The `[] notation effectively wraps up solve1 { rw h } in a begin... end block and treats the whole thing as a tactic unit (see Mario's backtick cheatsheet). So rw1 works here by looking for the actual name h in the context it's used in the example. I haven't personally experimented much with the `[] notation, so I don't know if there is a better way to pass in an arbitrary argument, but my sense is that Kyle's approach is better for this particular application.

[Rob Lewis]

I'm honestly not sure how antiquoting (%%a) works in `[...] blocks, so in general I wouldn't try... it'll definitely be less painful to write the tactic directly as Kyle shows

[Rob Lewis]

There's also docs#tactic.rewrite_target and surrounding decls if you need non-interactive versions