Transfer exprs between mvar contexts

Stream: general

[Marcus Rossel]

I'm having trouble implementing a tactic where a proof is being created in a different mvar context than that of the main proof goal. So the situation is basically the following:

• m : MVarId is the main proof goal
• o : MVarId is some other mvar
• h : Expr is a proof for m.getType which was created in the context of o

When I just assign h to m, I run into problems where h can contain references to fvars which m doesn't know about. What is the correct way to transfer the proof h from o to m?

#xy: the proof term is being extracted from grind by mkEqHeqProof. So o in this case is the mvar (with type False) which grind uses for its work internally.

[Joachim Breitner]

We'll, if h uses assumptions available in o but not in m, then it seems reasonable that this doesn't work. Is there anything about m and o that makes you hope that types can be moved from one to the other?

[Jason Reed]

Are you in some sense asking for a way to take the union of two mvar contexts?

[Marcus Rossel]

@Joachim Breitner Considering the #xy, I feel like it must work somehow, seeing as grind manages to produce proofs just fine. I guess I‘ll have to continue searching for where/how it does that.

[Marcus Rossel]

Jason Reed said:

Are you in some sense asking for a way to take the union of two mvar contexts?

Probably not, because in my concrete project I think there‘s some parity between the fvars in o and m‘s contexts which I want to carry over.

[Sebastian Ullrich]

If some proof step is done in an altered context, there must be something in the final proof term justifying that context change

[Marcus Rossel]

I've looked into grind some more. It obtains goal o by (approximately) calling docs#Lean.MVarId.revertAll and docs#Lean.MVarId.intros on the original proof goal m. Hence, if I know that h was valid in the context of m, there should be a way to transfer that to o.

Here's a #mwe demonstrating the setup. I feel like what I want to do is also revert all the variables in e and then reinstantiate them with the fvars of i. But I don't know how.

elab "test" t:term : tactic => withMainContext do
  let e ← Tactic.elabTerm t none
  logInfo m!"expr e:\n{e}"

  let m ← getMainGoal
  logInfo m!"goal m:\n{m}"

  let r ← m.revertAll
  logInfo m!"goal r:\n{r}"
  r.withContext do logInfo m!"expr e in goal r:\n{e}"

  let (fvars, i) ← r.intros
  logInfo m!"goal i:\n{i}"
  i.withContext do logInfo m!"expr e in goal i:\n{e}"

example (n m : Nat) (h : n > 0) : True → 5 = 6 := by
  test n + m
/-
expr e:
n + m

goal m:
n m : Nat
h : n > 0
⊢ True → 5 = 6

goal r:
⊢ ∀ (n m : Nat), n > 0 → True → 5 = 6

expr e in goal r:
_fvar.2391 + _fvar.2392

goal i:
n✝ m✝ : Nat
h✝ : n✝ > 0
a✝ : True
⊢ 5 = 6

expr e in goal i:
_fvar.2391 + _fvar.2392
-/

[Henrik Böving]

This seems like quite a dangerous path to walk on to me. You're planning to rely on particular implementation details of grind that could break at any moment.

[Marcus Rossel]

I think I don't really have a choice at the moment, as there currently does not exist an API for how I'm trying to interact with grind. I talked to @Leonardo de Moura about this, and I think we agreed that it would be most realistic for use cases such as mine to take this dangerous path first, and then suggest API extensions/improvements for grind based on the experience.

[Marcus Rossel]

In fact, the implementation of grind is probably going to have to address a similar problem to allow for parameters which are not just identifiers but whole terms. @Kim Morrison mentioned this is a planned feature in https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/grind.20with.20expressions/near/537573063.

[Marcus Rossel]

This does it. I just can't really do this in the context of grind, as it does not retain the fvars.

import Lean
open Lean Meta Elab Tactic

def _root_.Lean.MVarId.revertAll' (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := mvarId.withContext do
  mvarId.checkNotAssigned `revertAll
  let mut toRevert := #[]
  for fvarId in (← getLCtx).getFVarIds do
    unless (← fvarId.getDecl).isAuxDecl do
      toRevert := toRevert.push fvarId
  mvarId.setKind .natural
  mvarId.revert toRevert (preserveOrder := true) (clearAuxDeclsInsteadOfRevert := true)

elab "test" t:term : tactic => withMainContext do
  let e ← Tactic.elabTerm t none
  let m ← getMainGoal
  let (oldFVars, r) ← m.revertAll'
  let (newFVars, i) ← r.intros
  let e' := e.replaceFVars (oldFVars.map .fvar) (newFVars.take oldFVars.size |>.map .fvar)
  i.withContext do logInfo m!"expr e' in goal i:\n{e'}"

/--
info: expr e' in goal i:
n✝ + m✝
-/
#guard_msgs(info) in
example (n m : Nat) (h : n > 0) : True → 5 = 6 := by
  test n + m