Re-assembling a TSyntax `tacticSeq

Stream: lean4

[Scott Morrison]

Suppose I've come across a list of TSyntax `tactics (e.g. that my decision procedure has suggested will solve a goal), and I would like to re-assemble these into a TSyntax `tacticSeq. How do I do that?

import Lean

open Lean Syntax

def howDoI? (L : Array (TSyntax `tactic)) : TSyntax `Lean.Parser.Tactic.tacticSeq := by sorry

[Scott Morrison]

To #xy my problem, I'd like to make the following work:

import Lean
import Mathlib.Tactic.PermuteGoals

open Lean Syntax

def Lean.Syntax.TSepArray.ofElems {ks} {sep} (elems : Array (TSyntax ks)) : TSepArray ks sep :=
⟨mkSepArray elems (if sep.isEmpty then mkNullNode else mkAtom sep)⟩

def xy (n : Nat) (L : Array (TSyntax `tactic)) : TSyntax `tactic :=
  let n : TSyntax `num := Syntax.mkNumLit <| toString n
  let s : Syntax.TSepArray `tactic ";" := TSepArray.ofElems L
  `(tactic| on_goal $n => $s) -- fails

This fails with error message

 s has type
  TSepArray `tactic ";" : Type
but is expected to have type
  TSyntax `Lean.Parser.Tactic.tacticSeq : Type

and I'd like to bridge the gap. (Using indenting rather than semicolons is also a fine solution!)

[Scott Morrison]

@Gabriel Ebner, could I ping you on this one?

[Gabriel Ebner]

open Lean

variable (tacs : Array Syntax.Tactic)

#check `(by $tacs*)
#check `(by $tacs;*)
#check `(by $[$tacs]*)
#check `(by $[$tacs];*)

[Gabriel Ebner]

I was just about to collect all the options you have for antiquoting tacticSeqs! :smile:

[Scott Morrison]

Ah, too easy. :-) Is there a description somewhere of the antiquoting mechanism? I failed to discover these by reading the source code, even after thinking to look at antiquotations.

[Scott Morrison]

I guess it's just a matter of knowing examples to look at.

[Scott Morrison]

Gah, and how do I flatten a Array (TSyntax `tactic.seq) to a TSyntax `tactic.seq?

[Scott Morrison]

Or promote a TSyntax `tactic to a singleton TSyntax `tactic.seq?

[Mario Carneiro]

This seems like the wrong question. I pretty much never use tacticSeq except insofar as it appears going in or out of syntax quotations. The main trick is that if $tac is a tacticSeq then ($tac) is a tactic, and $[$tac]* will interpolate an array of tactics as a tacticSeq.

[Scott Morrison]

Perfect. ($tac) was what I was missing.

[Scott Morrison]

Is there a multi-line version of ($tac)? i.e. no parentheses and semicolons.

[Mario Carneiro]

yes, you can do (tac \n tac) too

[Mario Carneiro]

the parentheses are required though

[Scott Morrison]

But I'm starting from a tacticSeq...?

[Mario Carneiro]

I think you need to #xy

[Scott Morrison]

The example I'm fighting with is meant to be

constructor
on_goal 1 =>
  exact 37
exact 37

[Scott Morrison]

But it's coming out as (constructor; on_goal 1 => (exact 37); exact 37) , where the second exact 37 applies also to goal 1

[Mario Carneiro]

don't use semicolons?

[Mario Carneiro]

that seems like a parenthesizer error though

[Scott Morrison]

Let me #xy for a moment. I'm not writing this by hand.

[Gabriel Ebner]

I think it's worth pointing out that simp; assumption is not a tactic. (Although some parts of the system pretend it is by wrapping the two tactics in a mkNullNode, but that's a story for another day..)

[Gabriel Ebner]

You should probably use Array Syntax.Tactic everywhere, and only convert to a tactic on the top-level. (With parens for now.) Then you can store simp; assumption as two tactics. We'll figure something out for the code actions eventually so that we can replace a tactic by a sequence of tactics.

[Scott Morrison]

Okay, sorry for the delay, here's an #xy:

import Lean
import Mathlib.Tactic.PermuteGoals

open Lean Meta Elab Tactic Syntax

/-- A representation of a semi-structured
(i.e. only uses `on_goal` for structuring) tactic script. -/
inductive Script : Type
| single : Syntax.Tactic → Script
| step : Syntax.Tactic → Script → Script
| on_goal : Nat → Script → Script → Script

def Script.compile : Script → MetaM Syntax.Tactic
| .single s => `(tactic| $s)
| .step s S => do
  let S ← S.compile
  `(tactic| ($s; $S))
| .on_goal n a b => do
  let n := Syntax.mkNumLit <| toString (n+1)
  let a ← a.compile
  let b ← b.compile
  `(tactic| (on_goal $n => $a); $b) -- fails, a is not a TSyntax `tactic.seq

def test : MetaM Script := do
  pure (.step (← `(tactic| constructor)) (.on_goal 0 (.single (← `(tactic| exact 42))) (.single (← `(tactic| exact 37)))))

elab "test" : tactic => do
  let script ← test
  let tac ← script.compile
  evalTactic tac

def f : Nat × Nat := by test

example : f = (42, 37) := rfl

[Scott Morrison]

But I will in any case go and rethink this having seen @Gabriel Ebner's suggestion.

[Mario Carneiro]

One approach might be to take a page from the infoTree implementation and have a monad which stores a Array Syntax.Tactic in the state, and then you have the following operations:

• pushTactic : Syntax.Tactic -> M Unit: insert a new tactic node in the state
• withOnGoal : Nat -> M Unit -> M Unit: First stash the state in tacs and clear it, then run the continuation. Retrieve the new state tacs', and construct (on_goal $n => $tacs') and push it to tacs and restore the state.

[Scott Morrison]

I guess I'm not sure what problem a monad is solving here. It sounds like you want to do something intertwined with the tactic discovery process? That seems like unnecessary complication. I'm happy with some intermediate representation describing the structure of the proof, and am just looking for a way to synthesize the Array Syntax.Tactic from it.

[Mario Carneiro]

Well, all of your tactics need to do some proof recording as well, right? The manual version of what I just said would be to pass an Array Syntax.Tactic in and out of all the augmented tactics (or just out and append everything together). It will be a lot of common bookkeeping compared to having the monad handle it

[Mario Carneiro]

anyway, I agree with Gabriel that the "intermediate representation describing the structure of the proof" can be Array Syntax.Tactic; the monad is just a way to put stuff together transparently.

[Scott Morrison]

Okay. I appreciate the point about the monad, and I'll try that later, but it's orthogonal to my immediate problem. However I think I've got it now.

[Mario Carneiro]

Here's a working version of your example BTW:

import Lean
open Lean
syntax "on_goal " num " => " tacticSeq : tactic

/-- A representation of a semi-structured
(i.e. only uses `on_goal` for structuring) tactic script. -/
inductive Script : Type
| single : Syntax.Tactic → Script
| step : Syntax.Tactic → Script → Script
| on_goal : Nat → Script → Script → Script

def Script.compile : Script → Array Syntax.Tactic → MetaM (Array Syntax.Tactic)
| .single s, acc => return acc.push s
| .step s S, acc => S.compile (acc.push s)
| .on_goal n a b, acc => do
  let n := Syntax.mkNumLit <| toString (n+1)
  let a ← a.compile #[]
  b.compile (acc.push (← `(tactic| on_goal $n => $a))

[Scott Morrison]

I had come up with

/-- A representation of a semi-structured
(i.e. only uses `on_goal` for structuring) tactic script. -/
inductive Script : Type
| step : Syntax.Tactic → Script
| array : Array Script → Script
| on_goal : Nat → Script → Script

partial def Script.compile : Script → MetaM (Array (Syntax.Tactic))
| .step s => do pure #[← `(tactic| $s)]
| .array a => do
  pure (← a.mapM compile).flatten
| .on_goal n a => do
  let n := Syntax.mkNumLit <| toString (n+1)
  let a ← a.compile
  pure #[← `(tactic| on_goal $n => $[$a]*)]

(so with a different definition of Script, but whatever). Thanks for this, I will be able to use some combination of these.