How to reference the goal inside of a tactic?

Stream: general

[Daniel Sainati]

I am trying to do a rewrite as part of the use of a conv tactic. In particular, I am trying to expand out some places where && may have been simplified away. The reasons for this are not worth getting into, but suffice to say I am trying to do some metaprogramming and need to put things in a normal form that my tactics expect, so replacing b with true && b in some circumstances can help me get closer to this normal form.

However, when I try to rewrite with rw [←Bool.and_true] inside of a conv, Lean tells me that it cannot perform the rewrite because the pattern is a metavariable. If I instead supply the whole goal expression to the rewrite, it works just fine. That is, this example works:

example : true := by
  conv => rw [←Bool.and_true true]  /- transforms the goal from true = true to true && true = true && true -/
  /- some more stuff -/

but this one doesn't:

example : true := by
  conv => rw [←Bool.and_true]
  /- some more stuff -/

I would like to be able to do this rewrite without being having to supply the specific goal expression to the rw [←Bool.and_true], so that I can package up this normalization step into a tactic that I can perform on arbitrary goals. Is there either a) a way to get the rewrite to work even in the presence of metavariables? or b) a tactic like goal that I can use to pass the goal expression as the argument to my rewrite, like rw [←Bool.and_true goal] or something?

[Anne Baanen]

To get the goal type inside a tactic what I would use is docs#Lean.Elab.Tactic.getMainGoal followed by docs#Lean.MVarId.getType (or docs#Lean.MVarId.getType' depending on context). But in conv that probably wouldn't work.

[Anne Baanen]

Hoping Cunningham's law comes to your rescue :)

[Patrick Massot]

Note also that your question suggest that in example : true := by … the goal is true. It isn’t, since true is not in Prop but Bool. You may need to think about whether you really really want that kind of goal.

[Patrick Massot]

If you really want with goals coerced from Bool like that, you can recover your Bool by pattern matching, and then play with it. Something like

import Lean

open Lean Elab Tactic Meta Parser Tactic
elab "foo" : tactic => do
  let tgt ← getMainTarget
  if let mkApp3 (.const `Eq [_])  (.const `Bool []) l (.const ``true []) := tgt then
  let s ← PrettyPrinter.delab l
  evalTactic <| Unhygienic.run `(tactic| rewrite [← Bool.and_true $s])

example (b : Bool) : b := by
  foo
  sorry

[Patrick Massot]

where foo turns the goal b = true into (b && true) = true.

[Aaron Liu]

You can run the conv tactic apply to apply the theorem to the goal

[Patrick Massot]

Maybe I oversimplified the question by focusing on “tactic” and “rw [← Bool.and_true] doesn’t work” and ignoring the conv part. You can also do

elab "bar" : conv => do
  let tgt ← getMainTarget
  let s ← PrettyPrinter.delab tgt
  evalTactic <| Unhygienic.run `(conv| rw [← Bool.and_true $s])

example (b : Bool) : b := by
  conv =>
    congr
    bar
  sorry

[Daniel Sainati]

Thank you! This is super helpful. To generalize further, is there a way to take the bar tactic you've written here and allow it to take the specific rewrite tactic as an argument? I.e. if I don't always want to rewrite with Bool.and_true and instead want to pass in a specific lemma, like rw_goal_with (← Bool.and_true) in this case, but maybe a different lemma in other cases?

[Aaron Liu]

This works without any metaprogramming

example (b : Bool) : b := by
  conv =>
    congr
    apply (Bool.and_true ..).symm
  sorry

[Daniel Sainati]

is there a way to not close the goal afterwards? E.g. if i want to follow up the Bool.and_true with a rewrite by Bool.and_comm?

[Aaron Liu]

Just put another conv around it

example (b : Bool) : b := by
  conv =>
    congr
    conv => apply (Bool.and_true ..).symm
    conv => apply (Bool.and_comm ..)
  sorry

[Daniel Sainati]

I see, so you can't do a sequence of tactics within the same conv

[Aaron Liu]

Daniel Sainati said:

I see, so you can't do a sequence of tactics within the same conv

what?

[Robin Arnez]

Daniel Sainati schrieb:

I see, so you can't do a sequence of tactics within the same conv

You can usually but apply terminates a conv sequence.
You can also use trans:

example (b : Bool) : b := by
  conv =>
    congr
    apply (Bool.and_true ..).symm.trans (Bool.and_comm ..)
  sorry

[Daniel Sainati]

Brilliant. This is exactly what I was looking for. Thanks all for the help!