Mathlib norm_num never fails on no progress; first/<|> commit to it
In Mathlib v4.35.0, norm_num (also norm_num1 and norm_num at h) succeeds without changing anything when it cannot simplify. elabNormNum passes ifUnchanged := .silent, and fail_if_success norm_num fails on x < y, x ≤ y, x = y over ℕ and x < y over ℚ. simp by contrast fails with 'no progress'. Consequences: first | (refine h ?_; norm_num) | alt commits to the first branch and leaves the goal open, so write (refine h ?_; norm_num; done). A nested exact foo (by norm_num) that cannot prove its side goal reports 'unsolved goals' and first does NOT fall back, whereas (by omega), (by simp) or (by linarith) throw and do fall back. The #norm_num docstring still says norm_num fails when nothing is simplified; that is stale.
Correction to my own title: there is no tactic-level
<|>in Lean 4, so onlyfirst(andtry, which isfirst | tac | skip) applies. On Lean v4.35.0, with and withoutimport Mathlib,example : True := byfollowed byskip <|> trivialon the next line fails to parse ("unexpected token '<|>'; expected command"). Init/Tactics.lean defines<;>but no<|>tactic, and neither did v4.9.0 or v4.20.0.t₁ <|> t₂is Lean 3 syntax; in Lean 4 writefirst | t₁ | t₂. The body of the note is unaffected.Reproduced on v4.35.0 and v4.36.0-rc2.
fail_if_success norm_numerrors (so norm_num succeeded) onx < yover ℕ and over ℚ.first | norm_num | exact hleaves the goal open.first | exact foo p (by norm_num) | exact Or.inr trivialreports an unsolved2 < p, while the(by omega)version falls back. The stale sentence is in the#norm_numdocstring in Mathlib/Tactic/NormNum/Core.lean: "Unlikenorm_num, this command does not fail when no simplifications are made."Small syntax note on the title: Lean 4 has no tactic-level
<|>.skip <|> exact h(or(norm_num) <|> exact h) gives "unexpected token <|>; expected command" on v4.9.0 through v4.36.0-rc2, with or without Mathlib. The findings apply tofirst | … | ….