Basic question about writing a custom tactic

Stream: general

[Hongseok Yang]

I am trying to write a custom tactic that runs the rw tactic on a list of equalities generated by this custom tactic. But I am struggling to make `(tactic|rw ARRAY_OF_GENERATED_FACTS), where ARRAY_OF_GENERATED_FACTS refer to a list of lemmas that my custom tactic proved already and added to the hypothesis of the current goal state. Would some of you help me how to fix this? A baby version of this problem can be seen in the Lean code below:

import Lean

open Lean Elab Tactic Meta

elab "my_custom_rewrite_h0" : tactic =>
  withMainContext do
    let rwRule : TSyntax `Lean.Parser.Tactic.rwRule := TSyntax.mk (mkIdent `h0)
    let tacticSyntax ← `(tactic| rw [$rwRule])
    evalTactic tacticSyntax

theorem example_with_hyps (a b c d : Nat)
    (h0 : a = 100)
    (h1 : b = c)
    (h2 : c = d)
    (h_final : d = 100) : a = 100 := by
  my_custom_rewrite_h0

Although the assumption h0 is in the hypothesis, the my_custom_rewrite_h0 tactic fails to use it. Lean complains and says that the argument of rw in the implementation of my_custom_rewrite_h0 does not refer to the proof of some equality or iff statement. How should I change the argument part of rw in the above code?

Thank you very much for your help.
Hongseok

[Paul Reichert]

I'm on my mobile right now so I can't investigate deeper, but I think Lean's macro hygiene ensures that identifiers built in a macro won't refer to variables in the caller's environment. The h0 in your macro probably refers to a different name than your lemma hypothesis.

I don't know how to circumvent macro hygiene. I'm sure there is a way, but I wonder whether there's a more idiomatic solution to your problem. What are you trying to achieve with your tactic?

[Tomas Skrivan]

I also think you are being hit by hygiene. I do not understand why not to pass h0 as an argument to your tactic but I`m guessing that is not what you want. Can you show a more complicated example of the tactic you want to write?

[Robin Arnez]

This is not type-correct: let rwRule : TSyntax `Lean.Parser.Tactic.rwRule := TSyntax.mk (mkIdent `h0)
rwRule is its own node, so you'd really need to do mkNode ``rwRule #[mkNullNode #[], mkIdent `h0, mkNullNode #[]]
But don't do that because you can do

let tacticSyntax ← `(tactic| rw [$(mkIdent `h0):ident])

(in general avoid using TSyntax.mk)
I'm assuming the original problem was that it didn't infer ident correctly as the type and instead assumed rwRule. Because parsing happens first it can't know what the type you want at that point and it's often better to just specify using the colon.

[Hongseok Yang]

Thank you very much, Robin, Tomas, and Paul. Robin, your suggestion works, but what I need is actually a slightly more complex. I have an array of identifiers hs = #[mkIdenth0, mkIdent h1, ..., mkIdenthn], and want to convert this as an argument to rw, and have something like (tactic| rw hs). What I should do? Here is a modified version of my first example that illustrates this challenge.

elab "my_custom_rewrite_h0" : tactic =>
  withMainContext do
    -- let rwRule : TSyntax `Lean.Parser.Tactic.rwRule := TSyntax.mk (mkIdent `h0)
    -- let tacticSyntax ← `(tactic| rw [$rwRule])
    let h := #[mkIdent `h0, mkIdent `h1]
    let tacticSyntax ← `(tactic| rw [$h,*: ident])
    evalTactic tacticSyntax

theorem example_with_hyps (a b c d : Nat)
    (h0 : a = 100)
    (h1 : b = a)
    (h2 : c = d)
    (h_final : d = 100) : b = 100 := by
  my_custom_rewrite_h0

What follows explains the background of my question. Feel free to ignore it. I also tried to attach the current implementation of my tactic, but it is too long and Zulip refuses me to add the implementation at the end of this message.

Regarding what I want to do ultimately, I would like to implement a tactic that proves the equality between the products of combinations (i.e., e1.choose e2), using a simple proof strategy of expanding combinations to factorials and cancelling the same factors on both sides. I am doing this in multiple stages. First, I go through all the combinations (e1.choose e2) of both sides of the equality, and creates the product of the denominators of their factorial representations (e2.factorial * (e1 - e2).factorial). This product gets multiplied to both sides of the equality. Next, I rearrange the factors in both sides and group them such that each group has the form (e1.choose e2 * e2.factorial * (e1-e2).factorial). Third, I rewrite each such group to e1.factorial, using the generated equalities (e1.choose e2 * e2.factorial * (e1-e2).factorial = e1.factorial) that I generate using some lemma in Mathlib. Finally, I call an existing tactic (such as ring or ring_nf) to prove that the rewritten equalities hold.

The issue in my post comes from my failed attempt to implement the third step.

[Robin Arnez]

The correct syntax is let tacticSyntax ← `(tactic| rw [$[$h:ident],*])

[Robin Arnez]

If you want to read about some of the details of quotations, Metaprogramming in Lean 4 has a section about them.