5852865c92
This PR fixes a bug in `propagateBetaEqs` (in `Lean.Meta.Tactic.Grind.Beta`) where new equalities/terms introduced by beta reduction were added to the goal without checking the generation threshold. The generation of the new fact is the maximum generation of the lambda, the function `f`, and its arguments, plus one. Without the threshold check, beta reduction can cascade indefinitely on self-similar lambdas such as `(fun b => f (b + 1)) = fun b => f b`, which kept producing `f n = f (n + 1)` for every `n`. The fix aggregates argument generations before the threshold check and bails out when the resulting generation reaches `maxGeneration`.
27 lines
1.1 KiB
Text
27 lines
1.1 KiB
Text
/-!
|
|
Support for beta-reduction in `grind` must respect generation threshold.
|
|
-/
|
|
set_option warn.sorry false
|
|
|
|
/--
|
|
trace: [grind.beta] f 0 = f 0, using fun b => f b
|
|
[grind.beta] f 0 = f (0 + 1), using fun b => f (b + 1)
|
|
[grind.beta] f 1 = f 1, using fun b => f b
|
|
[grind.beta] f 1 = f (1 + 1), using fun b => f (b + 1)
|
|
[grind.beta] f 2 = f 2, using fun b => f b
|
|
[grind.beta] f 2 = f (2 + 1), using fun b => f (b + 1)
|
|
[grind.beta] f 3 = f 3, using fun b => f b
|
|
[grind.beta] f 3 = f (3 + 1), using fun b => f (b + 1)
|
|
[grind.beta] f 4 = f 4, using fun b => f b
|
|
[grind.beta] f 4 = f (4 + 1), using fun b => f (b + 1)
|
|
[grind.beta] f 5 = f 5, using fun b => f b
|
|
[grind.beta] f 5 = f (5 + 1), using fun b => f (b + 1)
|
|
[grind.beta] f 6 = f 6, using fun b => f b
|
|
[grind.beta] f 6 = f (6 + 1), using fun b => f (b + 1)
|
|
-/
|
|
#guard_msgs (trace) in
|
|
set_option trace.grind.beta true in
|
|
protected theorem Multipliable.tprod_eq_zero_mul' {f : Nat → Nat} (h : (fun b => f (b + 1)) = fun b => f b) (a : Nat)
|
|
(R : Nat → Nat → Prop) : R a (f 0) := by
|
|
fail_if_success grind -ring -linarith -order -lia -ac (splits := 0) -verbose
|
|
sorry
|