Stream: general

Topic: Antiquoting inside a tactic quotation

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:

Nicholas Scheel (Sep 16 2018 at 22:08):

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

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 ℝ,
apply nat.zero_lt_succ
end


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

Mario Carneiro (Sep 16 2018 at 23:02):

t should have type expr not Type

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


Nicholas Scheel (Sep 17 2018 at 00:09):

I'm using Lean v3.4.1 btw

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)

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)

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

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

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

Mario Carneiro (Sep 17 2018 at 04:25):

I suggest you use the noninteractive rw tactic outside interactive mode

Nicholas Scheel (Sep 17 2018 at 04:25):

that would probably be a good idea :D

Nicholas Scheel (Sep 17 2018 at 04:28):

would that be rewrite_target?

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