extract_lets cannot extract syntactically identical lets

Stream: lean4

[Terence Tao]

The extract_lets tactic had an unexpected (for me) behavior when two of the let statements referred to syntactically identical (not just defeq) expressions: only one of the two let statements can be assigned a name. MWE:

import Mathlib

example :
  let a := 42
  let b := 42
  a = b := by
  extract_lets a b  -- linter: b is unused
  rfl

From a purely pragmatic point of view, this does not hinder the ability to complete the proof - one simply uses the one name to refer to both quantities - but from a conceptual or pedagogical point of view it is not always desirable, because the two quantities might play completely different conceptual roles in the proof but are only syntactically equal "by accident". Would it be possible to modify the tactic to allow let statements with syntactically equal values but distinct names be assigned as distinct hypotheses in the proof state?

[Eric Wieser]

This looks like a bug to me, cc @Kyle Miller

[Notification Bot]

This topic was moved here from #mathlib4 > extract_lets cannot extract syntactically identical lets by Eric Wieser.

[Eric Wieser]

(import Mathlib is no longer needed, this is part of lean itself now)

[Kyle Miller]

The -merge option disables this feature:

extract_lets -merge a b

[Kyle Miller]

The behavior on extract_lets a b isn't a bug, but the error message could be more informative. What's going on is that extract_lets a is sufficient due to merging, so b really isn't being used. (In particular, it's the name that's not being used, not that it's an unused variable.)

[Terence Tao]

Perhaps a line could be added to the docstring for extract_lets to mention this flag.

[Kyle Miller]

In the meantime, here are all the options: https://github.com/leanprover/lean4/blob/e2e36087e1ff1c29043ded4949862d5da7a8cf4a/src/Init/MetaTypes.lean#L332

[Eric Wieser]

This behavior is a bit surprising to me:

import Mathlib

example :
    let a := 41 + 1
    let b := letI := @AddSemigroup.toAdd ℕ; 41 + 1
    a = b := by
  extract_lets a b -- not merged, but printed the same in the infoview
  have : a = b := by with_reducible rfl -- but they're the same!
  rfl

I think I'd argue that merge should operate on a coarser relation than "syntactically equal"

[Eric Wieser]

(or not be the default, since the behavior isn't deterministic as a function of the visible state even for non-ambiguous goals)