Zulip Chat Archive

Stream: general

Topic: Antiquoting inside a tactic quotation


view this post on Zulip Nicholas Scheel (Sep 16 2018 at 22:07):

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:

view this post on Zulip Nicholas Scheel (Sep 16 2018 at 22:08):

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

view this post on Zulip Nicholas Scheel (Sep 16 2018 at 22:14):

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

view this post on Zulip Nicholas Scheel (Sep 16 2018 at 22:19):

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

view this post on Zulip Mario Carneiro (Sep 16 2018 at 23:02):

t should have type expr not Type

view this post on Zulip Nicholas Scheel (Sep 17 2018 at 00:05):

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

view this post on Zulip Nicholas Scheel (Sep 17 2018 at 00:09):

I'm using Lean v3.4.1 btw

view this post on Zulip Nicholas Scheel (Sep 17 2018 at 00:10):

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)

view this post on Zulip Nicholas Scheel (Sep 17 2018 at 00:14):

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

view this post on Zulip Simon Hudon (Sep 17 2018 at 03:14):

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

view this post on Zulip Nicholas Scheel (Sep 17 2018 at 04:19):

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

view this post on Zulip Nicholas Scheel (Sep 17 2018 at 04:21):

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

view this post on Zulip Mario Carneiro (Sep 17 2018 at 04:25):

I suggest you use the noninteractive rw tactic outside interactive mode

view this post on Zulip Nicholas Scheel (Sep 17 2018 at 04:25):

that would probably be a good idea :D

view this post on Zulip Nicholas Scheel (Sep 17 2018 at 04:28):

would that be rewrite_target?

view this post on Zulip Simon Hudon (Sep 17 2018 at 15:47):

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


Last updated: May 14 2021 at 13:24 UTC