Collect all dependencies required for an expression

Stream: metaprogramming / tactics

[Leni Aniva]

Is there a function that collects all fvars that are required for an expression to make sense?

e.g., if I have

b : a
c : b

and the expression is f c, then both b and c would need to exist for this expression to make sense. However, collectFVars only collects c.

[Jannis Limperg]

I'm not aware of such a function.

In case it helps, I believe the specific situation you mention is not possible because f cannot be typed without mentioning b (i.e., @f b c), except if f is itself an fvar. Maybe there's an invariant here that can be exploited. Another corner case is unassigned mvars; there you'll have to assume that any fvar mentioned in the mvar's local context could potentially be used.

[Kyle Miller]

First thing that comes to mind is that you could add e := f c to the local context then use Lean.Meta.collectForwardDeps on every preexisting local variable. The set of local variables that have e as a forward dependency consist of the minimal context for f c. This handles mvars too.

[Leni Aniva]

Jannis Limperg said:

I'm not aware of such a function.

In case it helps, I believe the specific situation you mention is not possible because f cannot be typed without mentioning b (i.e., @f b c), except if f is itself an fvar. Maybe there's an invariant here that can be exploited. Another corner case is unassigned mvars; there you'll have to assume that any fvar mentioned in the mvar's local context could potentially be used.

assume f is a constant

[Aaron Liu]

def foo (n : Nat) : Type := Nat

example (n : Nat) (m : foo n) : Nat.isValidChar m := by
  -- in this context the goal does not mention `n`
  -- but the type of `m` depends on `n`
  -- `Nat.isValidChar` is a constant
  trace_state
  sorry

[Leni Aniva]

I see what you mean. The example I showed I above is a bad one. This would make more sense:

b : a
c : b
d : a = (some function of c)

and the expr is f d. In this case b and c are also dependencies. Or if the expr is just c, in which case b must also be a dependency.

[Aaron Liu]

What is your use case for this function?

[Leni Aniva]

Aaron Liu said:

What is your use case for this function?

determine the minimal context for an expression

[Aaron Liu]

I found docs#Lean.findExprDependsOn

[Aaron Liu]

this would be great if the arguments pf and pm were monadic (but I guess then you wouldn't be able to cache it)

[Leni Aniva]

Aaron Liu said:

I found docs#Lean.findExprDependsOn

This doesn't work for the case where the expr is just c

[Leni Aniva]

It does not signal that b is a dependency

[Aaron Liu]

I found docs#Lean.Expr.getMVarDependencies

[Aaron Liu]

it only works for mvar dependencies

[Aaron Liu]

You could loop through the local context in reverse and docs#Lean.MVarId.tryClear everything

[Kyle Miller]

I'll mention again that you can do Lean.Meta.collectForwardDeps on everything in the local context to figure out the correct dependencies. Adding the expression as a let variable is a trick to then let this computation process all the fvars and metavariables in your expression correctly.

[Kyle Miller]

Or there's the weird mkLambdaFVars (<- getLCtx).getFVars e (usedOnly := true), but you'll lose the connection to which fvar was actually used. It probably also needs a step to clear aux decls from the local context first.