mvars left in types after mkForallFVars

Stream: metaprogramming / tactics

[Chris Bailey]

If I have an expression e that contains metavariables ?a, ?b, and ?c, where ?c : f ?a ?b, and I call mkForallFVars #[?a, ?b] ?c, ?a and ?b are handled fine, but I end up with an error that ?c is of type f ?a ?b instead of f a b.

Is there a good way of handling this situation where the type of a metavariable in the expression we're closing around may reference one of the mvars being bound? I wasn't able to figure out how elimMVarDeps works in practice.

[Aaron Liu]

I think in this case you would want to revert ?c

[Chris Bailey]

Aaron Liu said:

I think in this case you would want to revert ?c

I should have mentioned I'm in TermElab and not Tactic, but I'll take a closer look at the implementation of revert to see if there's anything that would be applicable.

[Aaron Liu]

"revert" meaning "abstract it out along with ?a and ?b as well", not in the sense of docs#Lean.MVarId.revert

[Chris Bailey]

I see. I looked at the docs and saw the tactic namespace and "goal", but it's in MetaM. I'm not sure this will work as it only accepts FVarIds. I can potentially take the forall apart, keep track off the mapping from what were the mvarIds to a set of opened fvarIds manually and visit the whole thing looking for ?c, but I feel like I'm messily recreating something that probably already exists.

[Chris Bailey]

The local context for the mvars taken from getMVars (mkForallFVars ..) don't seem to have any changes/additions to their local context.

[Aaron Liu]

What are you trying to do?

[Kyle Miller]

I think mkForallFVars #[?a, ?b] ?c where ?c : f ?a ?b isn't allowed. It's like doing mkForallFVars #[x, y] z where z : f x y is a free variable. When you do mkForallFVars fvars e, the fvars list has to have the property that each fvar that appears in e, if it depends transitively on a variable in fvars, then appears in fvars.

With metavariables the situation is more complicated since you need to worry about dependencies both from fvars and from mvars.

Something that is also tricky here is that mkForallFVars #[?a, ?b] ?c needs to assign to ?c in some way to do the abstraction. If it's a synthetic opaque metavariable, that will be a delayed assignment, but otherwise it will be a true assignment with a freshly created metavariable. It's worth thinking about what you expect here.

[Kyle Miller]

Example if assigning c is ok:

import Lean

open Lean Meta Elab Command

/--
Given metavariables `a`, `b`, and `c`, does "mkForallFVars #[?a, ?b] ?c" correctly.
The type of `b` can depend on `a`.
The type of `c` can depend on `a` and `b`.

Returns this type and a new metavariable `c2`.
If `a : A`, `b : B a`, and `c : C a b` then `c2 : (x : A) → (y : B x) → C x y`.
The metavariable `c` is assigned during this process.
-/
def doIt (a b c : Expr) : MetaM (Expr × Expr) := do
  let cty ← inferType c
  let c2ty ← mkForallFVars #[a, b] cty
  let c2 ← mkFreshExprMVar c2ty
  c.mvarId!.assign <| mkApp2 c2 a b
  let res ← mkForallFVars #[a, b] c
  return (res, c2)

(I say it's "correct" but I didn't test it :-))

[Kyle Miller]

I think even in the synthetic opaque case (e.g. if c is a goal metavariable) you'll have to be ok with assigning some of these metavariables, or otherwise forgetting the relationship between c and the new c in the forall.

Thinking of c as a goal, whose target is C ?a ?b, then for things to continue to make sense ?a and ?b can't remain as metavariables, since implicitly mkForallFVars is declaring that ?a and ?b have been abstracted. The new goal would be a version of c with new local variables a and b. That is, the result of the doIt function and then doing intro.

[Chris Bailey]

Thanks. A mwe for what I'm trying to do boils down to elaborating

p (Fin.mk n ?a (?h : ?a < n)) → r

into this, where the proofs are left as synthetic mvars to be filled in as one would do with refine, but data mvars are forall bound during term elaboration:

∀ (a : Nat), p (Fin.mk n a (?h : a < n)) → r

The complications that prevent just using refine directly (and that are the source of my current problem) are that (1) I want to forall bind the non-prop mvars and only leave the prop mvars as goals, and (2) I have some extra steps that need to be done in the constructor application so I had to write that term elaborator. I'm instantiating the expected types of the arguments with the prior arguments, which I think is doing something wrong because refine basically handles this correctly. I'll try to figure out what's going on differently in refine or the built-in constructor elaborator.