leanprover-community / leanprover-community/mathlib4
`wlog` with Unused Declarations
Open
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 4.2k
- Forks
- 1.7k
- PR merge metrics
- No merged PRs in 30d
Description
The following code
import Mathlib.Tactic.WLOG
theorem bugs: ∀ (a : Nat) (f : Nat → Nat), f a = 0 := by
intros a f
let f' : Nat → Nat := λ x ↦ (f x).succ
-- have obv : ∀ x, (f x) + 1 = f' x := by simp [f']
-- clear f'
wlog h : a = 0
sorry
gives an error:
8:2:
tactic 'introN' failed, insufficient number of binders
a : Nat
f : Nat → Nat
h : a = 0
⊢ f a = 0
Uncommenting either of the commented lines fixes the problem so it seems to be related to the fact that the f' declaration is not used before the wlog tactic.
Tested with leanprover/lean4:v4.17.0-rc1 and 96a5ba5ce504f8b8e6acd659015e46e641d7af10.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start by reproducing the example with import Mathlib.Tactic.WLOG, including the unused f' declaration, and inspect the wlog tactic entry point. Compare the behavior when the declaration is referenced or cleared. Done means wlog handles the unused local declaration without the introN failure.
Written by the indexing model from the issue text.
Assessment
- Domain
- tooling
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100