Tracking Issue: Tactic wishlist

There has been some discussion of what tactics we would like in a few threads on Zulip. I am making this tracking issue to try to organize these ideas and put them in a visible place. Anyone with repo permission should feel free to edit or add to the list.

TODO: Integrate suggestions from this thread.

New Tactics

• Tendsto
  • Should find limits in "simple" cases (e.g., no 0/0 etc).
  • Simplest version is Continuous.tendsto' (by continuity) _ _ (by simp).
  • More advanced version should know that exp(-1/x) tends to 𝓝[>] 0 as x tends to atTop.
    *Should know that 1/x tends to cobounded as x tends to 𝓝[≠] 0 and vice versa (for any normed field, not only reals)
• Exists positive from limit
  • Prove statements like (δ : Real) (h : 0 < δ) ⊢ ∃ ε > 0, ε ^ 2 + 5 * ε + sin ε < δ ∧ 3 * ε < δ by proving Tendsto (fun ε ↦ ε ^ 2 + 5 * ε + sin ε) (nhds 0) (nhds 0), similarly for 3 * ε, then using this fact to get a witness
• Nonzero A tactic that proves expr ≠ 0.
  • at least as powerful as whatever field_simp currently uses (it tries several tactics);
  • knows lemmas like a ≠ 0 → -a ≠ 0, a ≠ 0 → b ≠ 0 → a * b ≠ 0 and a ≠ 0 → a ^ n ≠ 0;
  • fallbacks to positivity if it can't deal with the head symbol (e.g., +) and there is a PartialOrder instance
• Tactic that can compute things about polynomials
  • Polynomial equality
  • Polynomial disequality
  • n-th coefficient, leading coefficient
  • degree (compute_degree)
  • monicity (is that the word for the property of being monic?)
• ring in characteristic n
• More tactics resolving statements in decidable first-order theories
  • Such as:
    • Presburger arithmetic. (Is this just omega?)
    • Reals.
    • Lists.
  • Often these are hard to write fast tactics for.
    • Nevertheless, I think they could often be helpful.
    • Maybe the best version of these tactics is to use a look-up table for common instances.
• Tactic to decide the order on logarithmico-exponential functions
• Tactic to provide approximations of real-valued expressions (i.e prove 3.83 < ln(2) + pi < 3.84)
  • See (https://github.com/Timeroot/ComputableReal/tree/main) which does this, albeit with some feature yet-to-be-added:
    • pi
    • exp
    • log
    • ... see the link for more
• #21841
  • Pushes any instance of the def it is fed to the leaves of the syntax tree. For example, push Real.log would apply log_mul.
• field #4837
• module_nf
• recommend
• #25302
  • Preferably in order of typical completion time, though we could also use exponential backoff to avoid spending too much time on expensive tactics.
  • Have a ? version that gives a Try This on success.
• a tactic that rewrites modulo associativity and commutativity:#general > "Missing Tactics" list @ 💬

Enhancements of existing Tactics

• Improved positivity
  • more extensions
    • docs#Int.fract_nonneg,
    • docs#Int.floor_nonneg,
    • docs#Int.ceil_pos,
    • docs#Int.ceil_nonneg,
    • docs#Nat.ceil_pos
    • docs#neg_ne_zero
  • an attribute that automatically produces correct positivity extension in a simple case (e.g., we only know how to prove 0 ≤ f a, never 0 < f a, or we always can prove 0 < f a)
  • support for goals expr < 0, so that it can prove -3 * ε - δ < 0
  • Ability to supply terms
• zify! #7450
• rify
  • #25303
• There should be a by_contra! similar to contrapose!
• A preprocessor for linarith which identifies calls to natural division/modulo and introduces the facts
  • 0 ≤ n%d
  • n%d < d
  • d * n/d + n%d = n
  • Potential problem: if d = 0 these do not all hold.
• Make abel work for multiplicative monoids/groups.
  • #13233
  • #13442
• Make linear_combination work for groups.
• Reimplement polyrith in pure Lean, removing the dependence on sage and an internet connection.
• Boost omega into a full decision procedure for Presburger arithmetic.
• clear_unneeded:
  • #25319
  • If (a : α) is a hypothesis and α is Nonempty, but a is never used elsewhere, delete a.
  • If (h : a = ...) if a hypothesis and a is never used elsewhere, delete h.
• a version of simp_rw that can create new goals for side-conditions
• a version of field_simp that collects non-zeroness as side conditions.
• More ? versions of tactics
  • unfold? to list possible unfold applications. (https://github.com/leanprover-community/mathlib4/pull/12016)
  • assumption?/rwa? (replaces with call to exact)
  • field_simp?
  • #25320
    • (replaces by linarith only)
    • Or even better, by a call to linear_combination
• Let norm_cast use Fin.cast_val_eq_self, so Nat.cast (Fin.val n) simplifies to n.
• cases (r:ℚ) should replace r with _ / _ instead of an application of Rat.mk'
• push_neg should be aware of Infinite, Finite, Set.Infinite and Set.Finite, Nat.Odd, Nat.Even
• a ring_nf option to normalize a ring equality a = b to a - b = 0
• Let linear_combination be used nonterminally.
• suffices should work with incremental elaboration
• in conv mode, simp, unfold, etc should throw errors when doing nothing (like they usually do)
• Version of plausible that produces a counterexample demonstration.
• A option for the simp? tactic that, instead of outputting a simp only call, outputs a simp_rw call.
  • This would make it easier to step through the transformations of simp call when debugging it.
• Make norm_num convert Gaussian rationals to the form a_n / a_d + b_n / b_d * I
• A variant of extract_goal called extract_mwe that provides the same things, but with additional import and opened namespace information.
• ext at #general > "Missing Tactics" list @ 💬
• observe! #general > "Missing Tactics" list @ 💬

simprocs

• A simproc that simplifies expressions of the form ∃ a', ... ∧ a' = a ∧ ... (Zulip). (https://github.com/leanprover-community/mathlib4/pull/22273)
• TODO: The contents of #mathlib4 > potential simp_procs @ 💬

As-Yet Unported mathlib3 Tactics

• TODO identify these

This is a broad tracking list rather than a single implementation task, and it names no repository files, tests, or entry points. Start by choosing one unchecked tactic and reading its linked Zulip discussion and related existing tactics; completion criteria must be defined for that specific item before work begins.