Tactic wishlist

[BoltonBailey]

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
• push tactic that generalizes push_neg from neg to any def. #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 field tactic #4837
• module_nf
• recommend
• finish/terminal: It would be nice if tactics that were capable of finishing a proof were tagged with some kind of finishing or terminal attribute, so that they could be collected into a single tactic that would try them all.
  • 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.

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! zify! tactic #7450
• rify should work for NNreal.
• 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.
  • feat: abel for multiplicative Groups/Monoids #13233
  • feat: mabel tactic for multiplicative abelian groups #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.
• cleanup: A tactic to identify and remove redundant terms/hypotheses from the context, doing the work of clear but automatically.
• 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. ([Merged by Bors] - feat: interactive unfold? tactic #12016)
  • assumption? (replaces by exact)
  • linarith?/nlinarith?
    • (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
• 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)

As-Yet Unported mathlib3 Tactics

• TODO identify these