isDefEq variant which preserves let-bindings

Stream: metaprogramming / tactics

[Kyle Miller]

Clearing the value could fail if anything depends on the value of the local definition

[Heather Macbeth]

Ah, I start to see why this would be complicated. Nonetheless it seems to me that in many situations there are unambiguously "clearable" lets -- is there any API along these lines?

[Kyle Miller]

You could use clearValue and catch the error (or you could see how clearValue implements it — it reverts the context, making the target be a let expression, and then it turns it into a forall expression and sees if that passes isTypeCorrect — being able to turn a let into a forall or lambda is what I think of as being the definition of a clearable let.)

[Heather Macbeth]

I think I would like something a bit stronger, right? It doesn't matter if the let isn't clearable in the whole goal-plus-hypotheses I am currently working it, I just want to know if the let is clearable in the two expressions I'm checking the defeq on.

[Kyle Miller]

You could form the lambda expression from reverting all the used fvars that depend on the let and then seeing if it's type correct

[Kyle Miller]

(so, compute the list of fvars to revert, then use mkLambdaFVars (usedOnly := true) fvars expressionInQuestion)

[Heather Macbeth]

Ok, I think I understand that strategy, although it's something that would take me some time to learn how to implement. I'll look for other workarounds, and come back to this if I don't find them!

[Heather Macbeth]

Is there a way to compute the "minimal context" of a set of expressions? Something that will clear all the hypotheses and variables which aren't used in the expressions?

[Jovan Gerbscheid]

(deleted)

[Jovan Gerbscheid]

I think you can first find the array of free variables that depend on your given let variable as follows:

Do a for loop through all free variables in the context (which goes in order), starting after your let variable. For every fvar, you loop through its free variables (in its type and its value if it has a value), and if any of those is equal to your let variable, or to any of the variables in your array, then add it to your array.

[Jovan Gerbscheid]

Heather Macbeth said:

Is there a way to compute the "minimal context" of a set of expressions? Something that will clear all the hypotheses and variables which aren't used in the expressions?

To compute the variables that an expression depends on, you do a similar kind of for loop though the local context as I described above, but you have to loop through it in the reverse direction.

If you want to make a local context out of this, you can use LocalContext.erase to modify the local context by erasing all the fvars you don't want anymore.

[Heather Macbeth]

OK, thanks! This too is probably above my pay grade, but I'll come back to it if I can't find a workaround.

[Adam Topaz]

I don't know if this is the most efficient way to do this, but I hacked together something that might work:

import Lean

open Lean

def Lean.Meta.withMinimalLCtx (e : Expr) (go : MetaM α) : MetaM α := do
  let mut unusedFVars := #[]
  for (fvarId, _) in (← getLCtx).fvarIdToDecl do
    if e.containsFVar fvarId then continue
    unusedFVars := unusedFVars.push fvarId
  Meta.withErasedFVars unusedFVars go

Edit: I forgot about Lean.Expr.containsFVar, which makes the code much cleaner.

[Heather Macbeth]

Nice! So maybe I could do something like:

• write a variant of your function which finds the "minimal context" c for two expressions (rather than a single expression)
• recursively clear all the lets in c (and fail if impossible)
• run isDefEqin c

[Jovan Gerbscheid]

This is essentially what I suggested, but forgetting about further dependencies. The problem here is than you could have α : Type and a : α and if your expression contains only a, then you run into problems, because you erased α

[Heather Macbeth]

Ah, that's tricky. So e.containsFVar will not be true for α if the situation is that e contains some a : α?

[Jovan Gerbscheid]

Yes, for example if e is just a. I'm currently trying to write a version that does work.

[Adam Topaz]

Oh yeah, good point! I suppose you could traverse over all subexpressions with Meta.forEachExpr, and collect the fvars used in both the terms and their types.

[Jovan Gerbscheid]

you can write for fvarDecl in ← getLCtx do to loop through the LocalContext in order, but doing it in reverse is a bit more awkward. Here's a way I would do it:

  let mut s := collectFVars {} e
  let lctx ← getLCtx
  let mut i := lctx.numIndices
  while i != 0 do
    i := i - 1
    if let some fvarDecl := lctx.getAt? i then
      if s.fvarSet.contains fvarDecl.fvarId then
        s := collectFVars s fvarDecl.type
        if let some value := fvarDecl.value? then
          s := collectFVars s value

[Jovan Gerbscheid]

I am somewhat surprised that (as far as I've seen) there isn't already a funtion that does this.

[Heather Macbeth]

OK, interesting. Do if I understand correctly that, at the end of this logic, the s is the fvars that are "directly or indirectly" used in the expression e?

[Heather Macbeth]

Like you, I'm bit surprised that this isn't well-trodden ground in the metaprogramming API.

[Jovan Gerbscheid]

There does exist collectForwardDeps. The docstring starts with

Given toRevert an array of free variables s.t. lctx contains their declarations,
return a new array of free variables that contains toRevert and all variables
in lctx that may depend on toRevert.

[Jovan Gerbscheid]

On the topic of this collecting (backwards) dependencies, are you sure that collecting these fvars used directly or indirectly in your expression is what you need? I don't know how that would be useful.

[Heather Macbeth]

First, I should say that I'm no longer sure I want this "isDefEq which doesn't look inside lets". In my setting I'm leaning towards using a stricter equivalence relation on expressions, which doesn't look inside lets but also doesn't eta-reduce, beta-reduce, etc. And that's available easily as expr-equality (possibly working inside CanonM).

[Heather Macbeth]

So this is mostly for curiosity now (and also because "isDefEq which doesn't look inside lets" seems like a sensible thing which I or someone else might want in the future).

[Heather Macbeth]

But this is what I had in mind to write the "isDefEq which doesn't look inside lets":
Heather Macbeth said:

maybe I could do something like:

• write a variant of your function which finds the "minimal context" c for two expressions (rather than a single expression)
• recursively clear all the lets in c (and fail if impossible)
• run isDefEqin c

[Heather Macbeth]

Where the first step would be collecting backward dependencies of the two expressions I was comparing (and clearing everything in the context which wasn't a dependency of one of them).

[Jovan Gerbscheid]

I don't see how clearing things from the context that aren't used is helpful here. The goal was to run mkLambdaFVars with the forwards dependencies of the particular let-expression. e.g. if we are trying to remove the value of a : α := b, there is no point in abstracting the backwards dependency α. Instead we are interested in the forwards dependencies, i.e. the fvars that use a.

[Jovan Gerbscheid]

I hadn't seen the canonM before, that seems pretty useful for distinguishing expressions by the criterion that they look different to the user.

[Heather Macbeth]

Suppose I am in a setting like

x y z : ℝ
A : Type := ℝ
a : A := x
b : A := y
T : Type := ℝ
p : T := x
q : T := y
r : T := z
⊢ p ^ 2 + q = r

and I was interested in whether a and id a were defeq-not-unfolding-lets. Then I was thinking I would

(1) clear all the stuff which doesn't appear in a or id a: then I'm left with

x : ℝ
A : Type := ℝ
a : A := x

(2) iteratively clear the values of the lets that remain: first forget that a was defined to be x, then forget that A was defined to be ℝ

(3) check the defeq of a and id A in this new context.

[Heather Macbeth]

My concern was that if I don't perform the step (1), then my code will spuriously object about clearing T or p because they appear in the goal, even though they are irrelevant to the two expressions I want to compare. (Maybe I didn't cook up this example quite right, but perhaps you see what I mean anyway.)

[Jovan Gerbscheid]

Right, but intead of clearing it from the goal, you would only be clearing them from your one or two expressions. And since they don't appear there, clearing T or p won't do anything.

[Jovan Gerbscheid]

So I think what you'd need is to collect the forwards dependencies from all the free variables in your expression, and then run mkLambdaFVars on your expression with these free variables, and check the type of that. For this it doesn't matter what the current goal is. (in fact, MetaM doesn't even know what the current goal is, you need TacticM for that)

[Heather Macbeth]

Jovan Gerbscheid said:

So I think what you'd need is to collect the forwards dependencies from all the free variables in your expression,

I notice that you don't mention let-bindings at all in that sketched approach! Are the let-bindings perhaps somehow a red herring? That is, I just want to treat all free variables the same, whether or not they have a let-binding in the context.

[Jovan Gerbscheid]

When checking dependencies, there is a difference between let variables and normal free variables, because in a let-variable you need to check both the type and the value. Is that what you mean?

[Heather Macbeth]

I'm not sure. I'm pretty confused! Maybe it's not really possible to make progress here without writing down a few examples to discuss concretely.

[Jovan Gerbscheid]

So this is the problematic exmple I have in mind:

a : Nat := 5
b : Fin a
c : Fin 5
h : b = c

Then there is a problem if your expression contains h, and otherwise it is fine to forget the definition of a.

[Jovan Gerbscheid]

Hmm, now that I think of it, if you expressions contains b or h, you would also need to collect backwards dependencies, just to be able to find a .

[Jovan Gerbscheid]

Are you sure that you don't have a given list of let variables that you want to not unfold, instead of just all of them? Because if you want to do this for all free variables, it seems to get pretty messy.

[Heather Macbeth]

I was thinking there ought to be a "best-effort" version of "defeq without looking inside lets" -- on some broad class of examples (which includes most cases in the wild) it would not unfold the lets, but it would have some other behaviour (either looking inside the lets or failing, not sure which) when the expression doesn't make sense without looking inside the lets.

Your example would fall into the latter class (for a, not for the other variables).

[Jovan Gerbscheid]

In principle this wouldn't be a hard change. We already have different transparency settings for unfolding constants (in order: reducible, instance, regular, all). We may as well have 2 transparency settings for let-free variables.

[Jovan Gerbscheid]

By the wayisDefEq sometimes locally changes the transparency setting as appropriate. It could potentially do the same for the let-variable transparency.

[Heather Macbeth]

I think it would be pretty intuitive to have the low transparency settings not unfold lets, and the high transparency settings unfold lets. Not sure to draw the line, but perhaps "default" would be the first level at which lets are unfolded.

[Heather Macbeth]

Honestly, before I started digging into some tactic behaviour yesterday that I didn't expect, I would have assumed that was the case!

[Jovan Gerbscheid]

It sound reasonable, but I would guess that a lot of things would break after such a change.

[Jovan Gerbscheid]

I guess a change that wouldn't break anything would be to have a setting even weaker than reducible which doesn't unfold lets.

[Heather Macbeth]

It might end up being on the scale of lean4#2682 (which made a similar change in simp).

[Heather Macbeth]

Currently any tactic which uses isDefEq anywhere in the implementation may unfold lets ... including in some pretty surprising cases.

[Jovan Gerbscheid]

I see, it makes sense that one would generally want to avoid this unfolding .

But isDefEq itself doesn't return an expression. So then I guess you mean that it gives metavariable assignments in which these variables are unfolded? Or what sort of surprising cases do we get?

[Heather Macbeth]

This seems to happen in non-finishing tactics which have isDefEqs in their implementation: let-unfolding happens sometimes, but not always, as a side effect.

[Heather Macbeth]

For example, ring_nf:

import Mathlib

example (x : ℤ) (R : ℤ → ℤ → Prop) : True := by
  let a : ℤ := x
  have : R (x + a) (a + x) := by
    ring_nf

[Heather Macbeth]

I don't think most users would correctly guess the goal state after that ring_nf: it's

⊢ R (x * 2) (a * 2)

[Jovan Gerbscheid]

I agree, it would make sense in this case to have this weaker transparency setting. We also have ring_nf! which uses default transparency instead of reducible. But we could have ring_nf work in this weaker transparency setting.

[Notification Bot]

54 messages were moved here from #metaprogramming / tactics > whnf variant which preserves let-bindings by Heather Macbeth.