making a TacticM

Stream: mathlib4

[Heather Macbeth]

I hope we can consider the #mathlib4 stream an acceptable location for simple mathematically-inspired tactic questions.

Question: How can I make a TacticM which performs simp only [one_mul, neg_mul]?

[Mario Carneiro]

evalTactic `(simp only [one_mul, neg_mul]) is the easy way

[Heather Macbeth]

I've also encountered evalTactic (←`(tactic| ring)) in mathlib4:
https://github.com/leanprover-community/mathlib4/blob/3fbdae49475528e1e4014189f98d217e67ece6da/Mathlib/Tactic/Linarith/Datatypes.lean#L322
That's similar, right?

[Mario Carneiro]

that's what I meant (making MWEs takes a while)

[Mario Carneiro]

import Mathlib.Algebra.Ring.Defs

open Lean Elab Tactic

elab "foo" : tactic => do
  evalTactic (← `(tactic| simp only [one_mul, neg_mul]))

example [Ring α] (x : α) : -1 * x = -x := by foo

[Heather Macbeth]

Ah :-)

[Heather Macbeth]

Isn't there usually a TacticM version of a tactic, though? I had the impression that it was considered good style to separate out the frontend/syntax from the rest, and that in a situation like this there was some prewritten TacticM simp which I would use.

[Mario Carneiro]

Every tactic is a TacticM. The good style is to make a MetaM version of the tactic, but support for that depends on the tactic and for a lot of things from core you still basically need a syntax on hand unless you want to bypass / redo a lot of the front end work

[Mario Carneiro]

calling simp-the-TacticM looks almost the same:

elab "foo" : tactic => do
  evalSimp (← `(tactic| simp only [one_mul, neg_mul]))

example [Ring α] (x : α) : -1 * x = -x := by foo

[Mario Carneiro]

you still need to pass it a syntax in this form

[Heather Macbeth]

It seems a bit wordy. Am I working against intended use in some way? Would it be more compact if there were a simp-the-MetaM for this?

[Mario Carneiro]

oh if you think this is wordy you don't want to see what calling simp the MetaM looks like

[Heather Macbeth]

Ok, I'll run with this. If I want a tactic which chains several things together (something I would have written in Lean 3 as

`[try { tac1 }, try { tac2 }, tac3, try { tac4 }]

) would it be better style to write it as

evalTactic (← `(tactic| try { tac1 } ; try { tac2 } ; tac3 ; try { tac4 })

or

do
evalTactic (← `(tactic| try { tac1 })
evalTactic (← `(tactic| try { tac2 })
evalTactic (← `(tactic| tac3)
evalTactic (← `(tactic| try { tac4 })

[Heather Macbeth]

And if I need to split it across multiple lines where do I put the linebreaks?

[Mario Carneiro]

Here's the no-stx version of calling simp:

elab "foo" : tactic => withMainContext do
  let simpTheorems ← (simpOnlyBuiltins ++ [``one_mul, ``neg_mul])
    |>.foldlM (·.addConst ·) ({} : SimpTheorems)
  let ctx := { simpTheorems := #[simpTheorems], congrTheorems := ← getSimpCongrTheorems }
  _ ← simpLocation ctx none (.targets #[] true)

example [Ring α] (x : α) : -1 * x = -x := by foo

[Heather Macbeth]

what's a stx?

[Mario Carneiro]

it's actually not as bad as I thought it would be, this is obtained by inlining evalSimp, mkSimpContext, elabSimpArgs with your particular invocation arguments

[Mario Carneiro]

stx short for Syntax meaning the part where we construct the expression `(tactic| simp only [one_mul, neg_mul]) only to parse it for the actual arguments to pass to the backend

[Mario Carneiro]

Heather Macbeth said:

Ok, I'll run with this. If I want a tactic which chains several things together (something I would have written in Lean 3 as

`[try { tac1 }, try { tac2 }, tac3, try { tac4 }]

) would it be better style to write it as

evalTactic (← `(tactic| try { tac1 } ; try { tac2 } ; tac3 ; try { tac4 })

or

do
evalTactic (← `(tactic| try { tac1 })
evalTactic (← `(tactic| try { tac2 })
evalTactic (← `(tactic| tac3)
evalTactic (← `(tactic| try { tac4 })

Personally I like to do as much control flow stuff as possible in the do block rather than in the syntax, so I would write it like

do
  try evalTactic (← `(tactic| tac1)) catch _ => pure ()
  try evalTactic (← `(tactic| tac2)) catch _ => pure ()
  evalTactic (← `(tactic| tac3))
  try evalTactic (← `(tactic| tac4)) catch _ => pure ()

(assuming I didn't have any better way to call tac1-4)

[Mario Carneiro]

but either way works

[Mario Carneiro]

The main thing to keep in mind is that tac1; tac2 is not actually a tactic (it is a sequence of tactics), so I don't think `(tactic| tac1; tac2) will parse, you have to write `(tactic| (tac1; tac2))

[Heather Macbeth]

In this case tac2 is abel_nf. I found abelNFTarget which is nearly a TacticM except it needs an AbelNF.Config argument. Is there a quick way to make an empty one on the fly?

[Mario Carneiro]

{} probably

[Heather Macbeth]

Yup! Thanks!

[Thomas Murrills]

similar question along these lines: let's say I'm in TacticM and want to use `(tactic| ...) syntax to construct a term of a known type (which is not the main goal). What's the "best" pattern for that? evalTactic doesn't seem to easily let me assign a metavariable without some mvar-shuffling via run.

Is there a version (or a standard workflow) for evaluating tactics to construct a term? (I tried elabTermEnsuringType, but I ran into issues—I'm guessing because it couldn't see the tactic state? I wasn't sure, though.)

[Jannis Limperg]

elabTermEnsuringType is definitely the idiomatic solution. Turning a Syntax into an Expr is exactly what elaboration does.

[Dan Velleman]

It's a minor point, but I believe `(tactic| tac1; tac2) does parse. For example, a tactic I wrote includes this line:

evalTactic (← `(tactic| refine $hid ?_; clear $hid))

And it works fine.