Antiquoting inside a tactic quotation

Stream: general

[Nicholas Scheel]

Hi!! So I'm trying to write my first tactic and I have something that looks like this:

meta def naturally (t : Type) : tactic unit :=
  iterate `[ rw [← @nat.cast_zero %%t] ]

but I get this error:

kernel failed to type check declaration 'naturally' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  Type → tactic unit
elaborated value:
  λ (t : Type),
     .....................

I can write it without the antiquotation, but I realized I then have to have t in scope when I run naturally to get it to work that way :sweat_smile:

[Nicholas Scheel]

Do you know what the issue is and how I could write it properly? :)

[Nicholas Scheel]

Background: I'm basically trying to write a tactic that converts statements about \N embedded in \R into statements about \N, like the following:

example : ∀ n : ℕ, (0 : ℕ) < 2 + n := by intro n; simpa [nat.zero_lt_succ]

example : ∀ n : ℕ, (0 : ℝ) < 2 + n :=
  begin
  intro n,
  let t := ℝ,
  naturally ℝ,
  rw [add_comm _ n],
  apply nat.zero_lt_succ
  end

[Nicholas Scheel]

Why I’m trying to restrict it to a certain type is to prevent infinite recursion (e.g. 0 with lots of coercions from nat to nat); it would be cool if there was a better way to do this but I have not explored tactics much

[Mario Carneiro]

t should have type expr not Type

[Nicholas Scheel]

Hm ... I believe you, but it still doesn't seem to compile:

meta def naturally' (t : expr) : tactic unit :=
  tactic.interactive.iterate none `[ rw [← @nat.cast_zero %%t] ]

[Nicholas Scheel]

I'm using Lean v3.4.1 btw

[Nicholas Scheel]

it looks like this term is failing: rule := expr.subst (to_pexpr t) (it's missing the second argument)
without the antiquotation it is: rule := ``(@nat.cast_zero t)

[Nicholas Scheel]

I think it should be rule := expr.subst ``(λ (_x_1 : _), @nat.cast_zero _x_1) (to_pexpr t)

[Simon Hudon]

rw is tricky to use this way. Try not quoting it. You'll see its argument list is not a list of expr (in which case your attempt should work); it's a list of rw_rules

[Nicholas Scheel]

yeah, this is what I ended up with (forgive the messy code): https://github.com/MonoidMusician/MATH361/blob/56b6b5df40598bddade40e973a400a67cb79d184/src/hw/hw2.lean#L380-L407

[Nicholas Scheel]

I wasn’t able to get it to parse an expression in interactive mode, so I just made an alias for applying it to reals haha

[Mario Carneiro]

I suggest you use the noninteractive rw tactic outside interactive mode

[Nicholas Scheel]

that would probably be a good idea :D

[Nicholas Scheel]

would that be rewrite_target?

[Simon Hudon]

I was about to suggest rewrite_target but it requires that you encode <- by hand