Transfer Expr into grind's context

Stream: lean4

[Marcus Rossel]

I'm trying to tack a feature onto grind, but can't implement it without copying and slightly modifying a number of grind's (private) functions. I'm wondering if there's potential for this to be addressed as I think it could be a common issue.

High-Level Problem
Specifically, I'm trying to use an Expr obtained from "outside" of grind in an mvar context produced by grind itself (I've already partially discussed this in #general > Transfer exprs between mvar contexts ). Let's call the outer context o and grind's context g. The problem I'm running into is that the local context of o is not the same as the local context of g. As a result, any expressions containing fvars which were created in o are broken in the context of g.

More Details
The local contexts of o and g are however not unconnected. AFAICT the local context of g is derived from o by first reverting all local variables in o and then reintroducing them (and potentially introducing more fvars which were previously in the goal). This happens once before grind runs by first calling:

private def initCore (mvarId : MVarId) (params : Params) : GrindM Goal := do
  let mvarId ← mvarId.abstractMVars
  let mvarId ← mvarId.clearImplDetails
  let mvarId ← mvarId.revertAll -- RELEVANT LINE
  let mvarId ← mvarId.unfoldReducible
  let mvarId ← mvarId.betaReduce
  appendTagSuffix mvarId `grind
  mkGoal mvarId params

... and subsequently calling:

/--
Introduce new hypotheses (and apply `by_contra`) until goal is of the form `... ⊢ False`
or is inconsistent.
-/
def intros (generation : Nat) : SearchM Unit := withCurrGoalContext do
  ...

... once before grind's main loop:

/--
Try to solve/close the given goal.
Returns `some goal` if this subgoal failed to be closed,
and `none` if all subgoals were closed.
-/
def solve (goal : Goal) : GrindM (Option Goal) := do
  let (failed?, _) ← main.run goal
  return failed?
where
  main : SearchM (Option Goal) := do
    tryCatchRuntimeEx loop ...

  loop : SearchM (Option Goal) := do
    intros 0 -- RELEVANT LINE
    repeat
      ...
    return none

Solution?
Thus, it seems to me that if I want to "transfer" an expression e from the outer context o (in which grind is called) to the context g of grind's Goal, then it would suffice to obtain the list of new fvars introduced by intros and map the fvars in e to those new fvars (as shown in the last post of #general > Transfer exprs between mvar contexts). There is, however, currently no good way of doing that except by copying and slightly modifying a number of functions starting at revertAll and intros to retain the fvars. Does this seem correct, or am I missing something?

Related Efforts
It seems to me that the same problem must be addressed in order to allow for #lean4 > grind with expressions. @Kim Morrison, has there been progress on this, or is it in fact the case that you would need something similar to allow for general expression parameters?
Also, is there perhaps a completely different approach to using Exprs from outside of grind within grind that I'm missing?

[Kim Morrison]

We haven't been moving on passing terms yet, as so far it seems have := foo; grind is sufficing.

[Kim Morrison]

I'm a little hesitant to promise anything that involves GrindM or Goal at all --- this are internal interfaces that we still want to be able to break without telling anyone. :-)

[Kim Morrison]

Maybe you can explain why have doesn't work for your application?

[Marcus Rossel]

Kim Morrison said:

Maybe you can explain why have doesn't work for your application?

What I'm trying to implement is a wrapper around grind which allows one to make progress when grind fails, by extracting the minimal expression (wrt AST size) equivalent to the initial proof goal. For example, if the goal is P 1 2 3 and grind fails to solve this goal, but it does prove that P 1 2 3 = Q along the way, then I want to update the proof goal to be Q:

example (h : P 1 2 3 = Q) : P 1 2 3 := by
  grind extract min_ast
  -- ...
  -- ⊢ Q

That's why I need to translate expressions "into" grind and "out of" grind. Namely, following the example above, I need to translate P 1 2 3 into grind's context, and translate Q out of grind's context.
Translating expressions into grind's context seems like it should be doable, as I think there's a relatively direct translation of the fvars as outlined in my previous message. For the reverse direction I'm not sure, as I don't know if grind can introduce new fvars during its procedure (e.g. as a result of case splits?), which then have no corresponding fvar in the "outer" context.

[Marcus Rossel]

Kim Morrison said:

I'm a little hesitant to promise anything that involves GrindM or Goal at all --- this are internal interfaces that we still want to be able to break without telling anyone. :-)

That makes total sense. I'm just trying to get this to work somehow and would be interested in any sort of metaprogramming functionality to make this possible, even if it may change/break frequently.

As it stands, I'm working around this by defining my own hacky version of docs#Lean.Meta.Grind.main, which just relies on the order of fvars in the local contexts, and will surely break in some cases.