clear_value fails unexpectedly #25053
Description
Prerequisites
- Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues - Reduce the issue to a minimal, self-contained, reproducible test case.
Avoid dependencies to Mathlib or Batteries. - Test your test case against the latest nightly release, for example on
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
The tactic clear_value fails in a specific context with unreasonable trace.
Context
This snippet is generated by our coding agent.
Steps to Reproduce
The following is a working example followed by the bug example.
example : True := by
let x := 1
have x_def : x = 1 := by rfl
have : x + 1 = 2 := by
clear_value x
rw [x_def]
sorryimport Mathlib
set_option trace.Meta.check true
open Rat
variable (m : ℚ) (h₀ : 0 < m) (h₁ : ∑ k in Finset.Icc (1 : ℕ) 35, Real.sin (5 * ↑k * Real.pi / 180) = Real.tan (↑m * Real.pi / 180)) (h₂ : (↑m.num / ↑m.den : ℝ) < 90) in
example : True := by
letI deg_to_rad := fun (x : ℝ) => x * Real.pi / 180
letI S_val := ∑ k in Finset.Icc (1 : ℕ) 35, Real.sin (deg_to_rad (5 * ↑k))
letI f_cos := fun (j : ℝ) => Real.cos (deg_to_rad (5 * j))
letI telescoped_sum_val := f_cos 0 + f_cos 1 - f_cos 35 - f_cos 36
have telescoped_sum_val_def : telescoped_sum_val = f_cos (0 : ℝ) + f_cos (1 : ℝ) - f_cos (35 : ℝ) - f_cos (36 : ℝ) := by funext; rfl
have subprob_S_val_eq_h1_lhs_proof : S_val = ∑ k in Finset.Icc (1 : ℕ) 35, Real.sin (5 * ↑k * Real.pi / 180) := by
clear_value telescoped_sum_val
sorry
sorryExpected behavior: No error.
Actual behavior: Failed and log with head Meta.check.
Versions
- 4.20.0-rc5
- 4.12.0-rc1
- 4.9.0
Additional Information
The log is as the following.
[Meta.check] ❌️ ∀ (telescoped_sum_val : ℝ),
telescoped_sum_val = f_cos 0 + f_cos 1 - f_cos 35 - f_cos 36 →
S_val = ∑ k ∈ Finset.Icc 1 35, Real.sin (5 * ↑k * Real.pi / 180) ▼
[] application type mismatch
?m.2653 telescoped_sum_val telescoped_sum_val_def
argument
telescoped_sum_val_def
has type
telescoped_sum_val = f_cos 0 + f_cos 1 - f_cos 35 - f_cos 36 : Prop
but is expected to have type
f_cos 0 + f_cos 1 - f_cos 35 - f_cos 36 = f_cos 0 + f_cos 1 - f_cos 35 - f_cos 36 : Prop
Impact
Our coding agent heavily depends on clear_value. This bug breaks many snippets it generates.