PANIC at Mathlib.Tactic.GeneralizeProofs.mkLambdaFVarsUsedOn

Stream: mathlib4

[Boris Alexeev]

I encountered a PANIC deep into a monster Lean file. I believe the following is a minimal "working" example:

[Boris Alexeev]

import Mathlib

noncomputable def def1 (h : true) : ℕ := 0

noncomputable def def2 : ℕ := 0

theorem thm3 (n : ℕ) : true := by
  have h_a :
    let b := def2
    let c := def1 (true)
    true := by
      all_goals generalize_proofs at *;
  generalize_proofs at *;

[Boris Alexeev]

https://live.lean-lang.org/#project=mathlib-v4.24.0&codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQOB2E+AxhOAK4xJboCmcAJrQGaMsCMcAFKnAFxwYUcrQCU/OIFRCfgF44ABjyESZMJWp02rJswBME6XzmKcaWtFohBqEAGZu+A+IFCRsuFgCeOOHFRIAN3pUAH0kfh9fODp4LHcdXUjfGLhieI5uVzEkwWF6Iw9vKKikdHQQgHMIUoBnOArafFooUuAAL1oQsCgICGY6lDgAKgBuSIamlswOrp6+gfhRnCA

[Boris Alexeev]

The error on the "Lean 4 Web" site is:

[Boris Alexeev]

PANIC at Mathlib.Tactic.GeneralizeProofs.mkLambdaFVarsUsedOnly Mathlib.Tactic.GeneralizeProofs:208:11: unreachable code has been reached
backtrace:
PANIC at Mathlib.Tactic.GeneralizeProofs.mkLambdaFVarsUsedOnly Mathlib.Tactic.GeneralizeProofs:208:11: unreachable code has been reached
backtrace:

[Snir Broshi]

This is the unreachable code-
https://github.com/leanprover-community/batteries/blob/2e16f91af2a97975e5d2fac906494cd6c17ba255/Batteries/Tactic/GeneralizeProofs.lean#L210

[Aaron Liu]

I thought generalize proofs was in mathlib

[Aaron Liu]

did they move it to batteries

[Aaron Liu]

so the problem is once again the usedLetOnly option in docs#Lean.Meta.mkLambdaFVars being set to false by default means the result can be something other than a let or a lambda

[Aaron Liu]

this is #14444 which is still awaiting-author after more than a year

[Snir Broshi]

Tried to simplify the repro

import Batteries.Tactic.GeneralizeProofs

example :
    let := true
    let := (fun _ : True ↦ true) True
    True := by
  generalize_proofs

[Snir Broshi]

the type-error in the 2nd let seems necessary

[Boris Alexeev]

The problem did go away when I tried to fix the types. :)

[Snir Broshi]

Aaron Liu said:

so the problem is once again the usedLetOnly option in docs#Lean.Meta.mkLambdaFVars being set to false by default means the result can be something other than a let or a lambda

Do you know what's the type that is returned?

[Aaron Liu]

no idea what you mean by that

[Bryan Gin-ge Chen]

Aaron Liu said:

this is #14444 which is still awaiting-author after more than a year

I'm sure @Mario Carneiro wouldn't mind if someone adopted this!

[Snir Broshi]

Aaron Liu said:

no idea what you mean by that

We know that mkLambdaFVars doesn't return a let, and doesn't return a lambda. So what does it return?

[Aaron Liu]

in this case it returns the body of the let, since the let-variable isn't used in the body

[Aaron Liu]

so since the let is constructed from the argument e, it just returns e unchanged

[Aaron Liu]

in your example depending on how it's used in the implementation I think this would probably be the constant True