Access parent goal

Stream: new members

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Suppose my tactic myTac is running in the position below. Is there some way it can access the parent MVarId, i.e., the thing with expected type P?

example : P := by
  have : Q := by myTac
  ...

[Kyle Miller]

A trick I know is to start off with refine (?_ : ?goal), and then you can refer to ?goal inside the have

[Daniel Weber]

This seems to work, but it's hacky

import Lean

open Lean Elab Tactic

example (test : O → Q) : P := by
  have : Q := by
    apply test
    run_tac do
      withMainContext do
        let mg ← getMainGoal
        for (a, a') in (← getMCtx).eAssignment do
          if a == mg then continue
          let some (_, t, v, b) := a'.letFun? | continue
          let v ← instantiateMVars v
          if (v.findMVar? (· == mg)).isSome then
            logInfo m!"{a} ({a'})"
        return
    sorry
  sorry

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Kyle Miller said:

A trick I know is to start off with refine (?_ : ?goal), and then you can refer to ?goal inside the have

Indeed! I was wondering if it's possible to do programmatically without adjusting the proof script, though.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Daniel Weber said:

This seems to work, but it's hacky

import Lean

open Lean Elab Tactic

example (test : O → Q) : P := by
  have : Q := by
    apply test
    run_tac do
      withMainContext do
        let mg ← getMainGoal
        for (a, a') in (← getMCtx).eAssignment do
          if a == mg then continue
          let some (_, t, v, b) := a'.letFun? | continue
          let v ← instantiateMVars v
          if (v.findMVar? (· == mg)).isSome then
            logInfo m!"{a} ({a'})"
        return
    sorry
  sorry

Thanks! This does work, but relies on the by myTac appearing inside have, and the have elaborating to a let_fun. I guess the answer to the question of 'is there a mapping from mvars to 'parent mvars' in the MVarCtx is 'no'.

[Daniel Weber]

You can find the mvar with the maximal index which is assigned and contains the current goal, but then the parent would be the goal before apply, not the goal before the have. I assumed you were asking about have specifically

[Daniel Weber]

@Michael Bucko may I ask why you're randomly reacting to messages?

[Michael Bucko]

Daniel Weber schrieb:

Michael Bucko may I ask why you're randomly reacting to messages?

I'm not a bot :) I react after I read and find something interesting. And I read and code a lot.