clear_value

Stream: mathlib4

[Jireh Loreaux]

It seems the clear_value tactic has not been ported. Are there any workarounds?

[Kyle Miller]

Here's a port: mathlib4#2916

[Kyle Miller]

Here's a workaround that does basically what clear_value is doing:

theorem let_of_forall {P : α → Prop} (h : ∀ (x : α), P x) : let x := v; P x := h v

example : let x := 22; 0 ≤ x := by
  intro x
  -- `clear_value x` workaround:
  revert x; apply let_of_forall; intro x
  sorry

example : let x := 22; let y : Fin x := 0; y.1 < x := by
  intro x y
  -- `clear_value y x` workaround:
  revert y; apply let_of_forall; intro y
  revert x; apply let_of_forall; intro x
  sorry

When you do the intro on each line, you have to be sure to intro everything that was reverted.

[Kyle Miller]

I couldn't immediately find let_of_forall in mathlib, but it seems like it's an important relationship between forall and let.

[Jireh Loreaux]

Thanks @Kyle Miller!

[Kyle Miller]

In mathlib4#2916, I'm finding that clear_value isn't interacting well with the unused variables linter.

Here's an example:

example : let x := 22; let y : Nat := x; let z : Fin (y + 1) := 0; z.1 < y + 1 := by
  intro x y z -- claims `z` is unused
  clear_value x
  exact z.2

The implementation of clear_value uses Lean.MVarId.revert, does some processing, then does Lean.MVarId.introNP to undo the revert.

My best guess is that the unused variable linter doesn't notice z is being used because introNP creates fresh fvars, so the z in exact z.2 is a new z.

[Kyle Miller]

If that's the issue, then is this a problem with the unused variables linter? or should the tactic be careful to use the same FVarIds?

[Kyle Miller]

If it's the latter, is there a version of introNP somewhere that takes a list of FVarIds to use, rather than calling mkFreshFVarId?

Or is there a way to "link" two FVarIds together here for the purpose of helping the unused variable linter (and the IDE)? I do get two lists: one of the FVarIds that were reverted, and another of the FVarIds that are introduced.

[Kyle Miller]

(Note that this issue should affect docs4#Lean.MVarId.changeLocalDecl as well since it also does revert/introNP.)

[Kyle Miller]

Kyle Miller said:

My best guess is that the unused variable linter doesn't notice z is being used because introNP creates fresh fvars, so the z in exact z.2 is a new z.

This turns out to be the case. In mathlib4#2937 I have a fix for this, but it involves duplicating a good chunk of the implementation of introNP... Maybe there's another solution?

With this version, neither clear_value nor change ... at cause any spurious unused variable warnings. They also properly handle that variable highlighting feature in VS Code.

[Kyle Miller]

(@Jireh Loreaux clear_value is merged. Let me know if you run into any unused variable linter errors due to it.)

[Jannis Limperg]

I'm very suprised that changeLocalDecl uses the revert-intro pattern. It requires a defeq type, so it should be safe (and faster) to just create a new mvar with a modified lctx. This would also preserve the FVarId.

Wrt your original question, I'm not sure whether it's allowed to change the value of an fvar without generating a new FVarId.

[Kyle Miller]

I think the reason for revert-intro is so it can register a type hint, since Lean doesn't have transitive defeq.

[Jireh Loreaux]

Will do, but it won't be until at least tomorrow until I can check.

[Jannis Limperg]

Kyle Miller said:

I think the reason for revert-intro is so it can register a type hint, since Lean doesn't have transitive defeq.

Possible, though the same file also contains replaceLocalDeclDefEq which implements the method I was alluding to (without a type hint). :shrug:

[Kyle Miller]

Hmm, I had decided not to use replaceLocalDeclDefEq because it didn't register a type hint, but it looks like it's used pervasively in Lean 4, so maybe in practice it's not a problem. I switched change ... at to use it in mathlib4#2937

[Kyle Miller]

Also, @Jannis Limperg, when you said "I'm not sure whether it's allowed to change the value of an fvar without generating a new FVarId" did you mean that as "I'm not sure whether it's possible" or "I'm not sure whether you are meant to"? It's definitely possible (that's what mathlib4#2937 was doing, at least before the commits I just pushed), but I wonder whether re-using FVarIds is breaking any contract.

[Jannis Limperg]

The latter. Like you, I'm not sure what the precise contract for changing LocalDecls is. I know you're allowed to replace the type T of a LocalDecl with a defeq type U. I also know you're not allowed to replace T with a non-defeq type V. (Nothing stops you from doing this, but all kinds of things would probably get messed up.) But I've never seen any documentation on whether changing/removing a value is allowed.