How to do TacticM's options in MetaM?

Stream: general

[Zihao Zhang]

import Mathlib
open Lean Meta Elab Tactic Term

def fun1 (i : TacticInfo) : MetaM Unit:= do
  let goalsBefore:=i.goalsBefore
  let goalsAfter:=i.goalsAfter
  for goal1 in goalsBefore do
    for goal2 in goalsAfter do
      let goal2_type ← goal2.getType
      let p ← mkFreshExprMVar goal2_type MetavarKind.syntheticOpaque `h_100
      goal1.withContext do
        let (_, goal1New) ← MVarId.intro1P $ ← goal1.assert `h_100 goal2_type p
        replaceMainGoal [goal1New]

Like this, the replaceMainGoal [goal1New] reported an error. It is just an example, so don't just change TacticM into MetaM.

[Kyle Miller]

replaceMainGoal doesn't make sense from within MetaM. The TacticM monad contains a list of current goals, and it has all of the TermElabM state too. The MetaM monad has neither of these things.

What are you trying to do with fun1? Likely you don't need replaceMainGoal.

[Zihao Zhang]

So it is impossible?

[Zihao Zhang]

@Kyle Miller

import TrainingData.Frontend
import TrainingData.InfoTree.ToJson
import Mathlib.Data.String.Defs
import Mathlib.Lean.CoreM
import Batteries.Data.String.Basic
import Cli

open Lean Elab IO Meta Tactic Term
open Cli System
#check Format
namespace Lean.Elab.TacticInfo

def foo (m : MetaM α) : IO α := CoreM.withImportModules #[`Mathlib] <| m.run'



def verboseTrainingData_1 (module : Name) (i : TacticInfo) (ctx : ContextInfo) : MetaM String := do
  let mut result := "===\n"
  let sourceUpToTactic := Substring.mk (← moduleSource module) 0 (i.stx.getPos?.getD 0)
  let chunks := sourceUpToTactic.splitOn "\n\n"
  let goalstate_before:=← i.goalState ctx
  --for x in goalstate_before do
  --   IO.println ("x:",x)
  let goalsBefore:=i.goalsBefore
  let goalsAfter:=i.goalsAfter
  for goal1 in goalsBefore do
    for goal2 in goalsAfter do
      let goal2_type ← goal2.getType
      let p ← mkFreshExprMVar goal2_type MetavarKind.syntheticOpaque `h_100
      goal1.withContext do
        let (_, goal1New) ← MVarId.intro1P $ ← goal1.assert `h_100 goal2_type p
        replaceMainGoal [goal1New]






    --let goalFmt ← Meta.ppGoal goal
    --IO.println s!"Goal ID: {goal.name}\nType: {goalType}\nContext:\n{goalFmt}\n"

  result := result ++ (Format.joinSep (← i.goalState ctx) "\n").pretty ++ "\n---\n"
  result := result ++ (← i.pp ctx).pretty ++ "\n---\n"
  result := result ++ (Format.joinSep (← i.goalStateAfter ctx) "\n").pretty ++ "\n"
  return result
def verboseTrainingData (module : Name) (i : TacticInfo) (ctx : ContextInfo) : IO String := do
  let s ← foo (verboseTrainingData_1 module i ctx)
  return s

This is my original code, I just want to do some options of TacticM and MetaM, and return a string to verboseTrainingData.

[Zihao Zhang]

More concisely, I want to make goal2 a hyp of goal1.

[Kyle Miller]

Zihao Zhang said:

So it is impossible?

It's not strictly impossible (one can run TacticM from within MetaM and collect a resulting goal list), but it doesn't make sense to use replaceMainGoal in MetaM. There's no goal list in MetaM, and the purpose of replaceMainGoal is to manipulate the goal list.

I don't see in the code any motivation to manipulate a goal list.

Just to check: are you expecting that the for loops are manipulating a global state, and that somehow the i.goalsAfter will be changed? Lean is a functional language, and that's not possible. Instead, you can keep track of the new data you produce yourself.

[Zihao Zhang]

So, I can only manipulate the strings to ugly achieve my goal--making the goal2 a hyp of goal1 and print goal1's tactic state?

[Kyle Miller]

No, I didn't say that at all. I'm just saying that replaceMainGoal is likely not part of your solution.

[Zihao Zhang]

Without replaceMainGoal , I think the goal of goal1 with be No goals,it's not what I want. Like this:

import Mathlib
open Lean Meta Elab Tactic Term

elab "add_goal_to_hyps " : tactic => do
  let mvarId ← getMainGoal
  let t ← mvarId.getType
  let p ← mkFreshExprMVar t MetavarKind.syntheticOpaque `h_1
  mvarId.withContext do
    let (_, mvarIdNew) ← MVarId.intro1P $ ← mvarId.assert `h_1 t p
    --replaceMainGoal [mvarIdNew]
example : 0 + a = a := by
  add_goal_to_hyps

[Kyle Miller]

Are you looking for something like this?

def fun1 (i : TacticInfo) : MetaM Unit:= do
  let goalsBefore:=i.goalsBefore
  let goalsAfter:=i.goalsAfter
  let mut newGoals := #[]
  for goal1 in goalsBefore do
    for goal2 in goalsAfter do
      let goal2_type ← goal2.getType
      let p ← mkFreshExprMVar goal2_type MetavarKind.syntheticOpaque `h_100
      let goal1New ← goal1.withContext do
        let (_, goal1New) ← MVarId.intro1P $ ← goal1.assert `h_100 goal2_type p
        pure goal1New
      newGoals := newGoals.push goal1New
  -- do something with `newGoals` here