Commit 2023-11-18 03:04 5e4a27b1
View on Github →fix: add some missing whnfR in Linarith/Preprocess (#8310) Fixes this example reported on zulip:
import Mathlib.Tactic.Linarith
--set_option pp.raw true
--set_option trace.linarith true
example (k : ℤ) (h : k < 1) (h₁ : -1 < k)
: k = 0 := by
-- linarith -- works
change -1 < _ at h₁
-- linarith -- fails!
have hk : k = 0 := by
linarith
exact hk
See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linarith.20fails.20in.20a.20simple.20example/near/401267407.
In the failure case, when the strengthenStrictInt preprocessor does inferType on the h₁ : -1 < k hypothesis, it sees it as an mvar, and therefore the match on getAppFnArgs
fails.