has_to_pexpr (parse ident) error trying to write a tactic

Stream: new members

[Geoffrey Irving]

I'm trying to make a (very simple) tactic that replaces a subexpression with a new variable throughout the context. Here's an example of the tactic logic I want to automate:

lemma test1 (x y : ℕ) : x + y ≥ 0 :=
begin
  let z := x + y,
  let h : x + y = z := rfl,
  rw h,  -- target is now z ≥ 0
  simp
end

At the beginning of the proof, the goal is x + y ≥ 0. The first three lines replace the goal with z ≥ 0, and add z =: x + y as a hypothesis.

Here's an attempt at a tactic to do this, and the hoped-for rewritten proof:

meta def tactic.interactive.label (s : parse ident) (q : parse texpr)
    : tactic unit := do
  e ← tactic.i_to_expr q,
  «have» s none q,
  rw ``(rfl : %%e = %%s)

lemma test2 (x y : ℕ) : x + y ≥ 0 :=
begin
  label z (x + y),
  simp
end

Unfortunately, I'm pretty sure I have the quotation logic wrong in that tactic, as I get an obscure error message

failed to synthesize type class instance for
s : parse ident,
q : parse texpr,
tactic.interactive.label : tactic unit,
e : expr,
_x : unit
⊢ has_to_pexpr (parse ident)

Thanks in advance for any pointers!

[Damiano Testa]

Should you use e instead of q in have?

[Damiano Testa]

On mobile and it's late, so may be nonsense!

[Geoffrey Irving]

Alas, that produces the same error (which is not surprising since it's complaining about parse ident, not parse texpr).

[Geoffrey Irving]

Indeed, here's a simpler version with no texpr and the same error (via hardcoding):

meta def tactic.interactive.label (s : parse ident) --(q : parse texpr)
    : tactic unit := do
  --e ← tactic.i_to_expr q,
  «have» s none ``(`x + `y),
  rw ``(rfl : `x + `y = %%s)

[Eric Wieser]

Can you make a mwe with imports?

[Eric Wieser]

My guess is that you ned to write %%`(s) instead of %%s

[Eric Wieser]

Or maybe you want docs#tactic.get_local to turn the name into an expression

[Damiano Testa]

I do not know how to fix the issue in your initial tactic, but I think that it is caused by the rw, not the have. If you do this:

import tactic.core
open tactic interactive
setup_tactic_parser

meta def tactic.interactive.label (s : parse ident) (q : parse texpr) : tactic unit := do
e ← i_to_expr q,
tactic.interactive.«have» s none q,
read >>= trace,
rw ``(rfl : %%e = %%s)

lemma test2 (x y : ℕ) : x + y ≥ 0 :=
begin
  label z (x + y),
  simp
end

Then you can see that the problem is with the rw. Indeed, from the read command, you can see that you have successfully added z to the local context, but you did not create the expression x + y = z.

Also, I think that instead of rw you may end up using rewrite_target.

[Damiano Testa]

For some strange reason, the first time that I pasted your code in, it was not highlighting the rw as wrong, but only the def. Now, it seems more directly mentioning the rw. I imagine that what I said above is not helpful, then, sorry!

[Geoffrey Irving]

Here's a working example of roughly what I want except for the ident part:

import data.real.basic
import init.meta.rewrite_tactic
open interactive (parse)
open lean.parser (ident)
open interactive.types (texpr)

lemma test1 (x y : ℕ) : x + y ≥ 0 :=
begin
  let z := x + y,
  let h : x + y = z := rfl,
  rw h,  -- target is now z ≥ 0
  simp
end

meta def tactic.interactive.label (s : parse ident) (e : parse texpr)
    : tactic unit := do
  e ← tactic.i_to_expr e,
  tactic.pose s none e,
  t ← tactic.i_to_expr ```(%%e = z), -- Ideally, z would be %%s or similar
  h ← tactic.assert `h t,
  tactic.reflexivity',
  tactic.rewrite_target h,
  tactic.clear h

lemma test2 (x y : ℕ) : x + y ≥ 0 :=
begin
  label z (x + y),
  simp
end

[Geoffrey Irving]

In the end I'm not sure how to use rw, but calling into the noninteractive tactics seems reasonable (though I'd be curious if there are ways to do this in fewer lines). The missing bit is that (%%e = z) hardcodes z rather than using %%s or similar. I'm still not sure how to use s without getting the has_to_pexpr (parse ident) error.

[Geoffrey Irving]

@Damiano Testa Thanks for also proposing rewrite_target instead of rw; that does seem to involve less magic.

[Eric Wieser]

Did you try my suggestion to use get_local?