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.

Estimated changes