Examples highlighting "unique" capabilities of tactics

Stream: new members

[Isak Colboubrani]

For demonstration purposes, I’m compiling a list of goals that are “uniquely solved” by certain closing tactics (with zero arguments). By “uniquely solved,” I loosely mean that no other tactic can directly solve these goals unless it internally calls the same “primary tactic.”

For instance, consider the following example, which (as far as I can tell) is only solvable by polyrith:

import Mathlib
example (a b c d e f : ℂ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := by polyrith

Some other candidates include:

import Mathlib
example (P : Nat → Prop) (h : {x // P x}) : ∃ x, P x ∧ 0 ≤ x := by aesop
example : Nat.Prime 37 := by decide
example (a b c : ℝ) (h : a ≤ b) : c - Real.exp b ≤ c - Real.exp a := by gcongr
example (h : 1 < 0) : False := by linarith
example : (2 : ℝ) < 5 / 2 ∧ 5 / 2 < 3 := by norm_num
example : 37^2 - 35^2 = 72 * 2 := by omega
example : (-126432 : ZMod 1235412223) ^ 12355342321 = 1001528716 := by reduce_mod_char
example {α : Nat → Type} (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by solve_by_elim
example (p q r : Prop) : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (r ∨ p ∨ r) := by tauto

Do these examples look correct? And do they serve as good representatives for their respective tactics?

And can anyone suggest more examples that highlight the unique capabilities of other tactics?

The preliminary list of tactics I plan to cover: abel aesop aesop_cat assumption bound coherence continuity contradiction decide dsimp ext fun_prop gcongr group infer_instance linarith measurability module noncomm_ring norm_num omega polyrith positivity reduce_mod_char rfl ring rw_search simp simp_all solve_by_elim tauto trivial

Which of these tactics are unlikely to have such an "unique example"? Also, which relevant tactics have I overlooked?

[Kyle Miller]

example : Nat.Prime 37 := by norm_num

[Kyle Miller]

example : 37^2 - 35^2 = 72 * 2 := by rfl -- or norm_num or simp

[Kyle Miller]

omega is meant for linear integer inequalities rather than equations without variables. It can do some case-splitting too to deal with some non-linearities.

[Julian Berman]

Is that rfl example meant to be a counterexample to uniqueness part of this or are you saying it's really a Good Idea™ to use it for that goal? To me I like knowing what kinds of goals make someone say "that's exactly what tactic XYZ is meant for", regardless even of whether a "simpler" tactic can directly solve it -- is rfl really solving that because it should or because it just happens to? (I'd have reached for norm_num seeing all numerals there personally)

[Isak Colboubrani]

@Kyle Miller Thanks for sharing those counterexamples. I’ll remove this example as well:

example (p q r : Prop) : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (r ∨ p ∨ r) := by tauto
example (p q r : Prop) : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (r ∨ p ∨ r) := by aesop

The following examples still stand as presumably “unique examples”:

import Mathlib
example (P : Nat → Prop) (h : {x // P x}) : ∃ x, P x ∧ 0 ≤ x := by aesop
example (a b c : ℝ) (h : a ≤ b) : c - Real.exp b ≤ c - Real.exp a := by gcongr
example (h : 1 < 0) : False := by linarith
example : (2 : ℝ) < 5 / 2 ∧ 5 / 2 < 3 := by norm_num
example (a b c d e f : ℂ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := by polyrith
example : (-126432 : ZMod 1235412223) ^ 12355342321 = 1001528716 := by reduce_mod_char
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by solve_by_elim

[Isak Colboubrani]

Four new presumably unique examples:

import Mathlib
example (a b : α) [AddCommMonoid α] : a + (b + a) = a + a + b := by abel
example (a b c : G) [Group G] : c⁻¹*(b*c⁻¹)*c*(a*b)*(b⁻¹*a⁻¹*b⁻¹)*c = 1 := by group
example (a b : R) [Ring R] : (a + b)^3 = a^3 + a^2*b + a*b*a + a*b^2 + b*a^2 + b*a*b + b^2*a + b^3 := by noncomm_ring
example (a b c : α) [LinearOrderedField α] :  a * (-c / b) * (-c / b) + -c + c = a * (c / b * (c / b)) := by ring

[Julian Berman]

Adding division somewhere to an example will probably give you a field_simp one.

[Kyle Miller]

@Julian Berman For natural number arithmetic with concrete small numbers, I think rfl is best. It gets the kernel to just compute. It gives an efficient proof term.

[Julian Berman]

Wow interesting, TIL. (@Isak Colboubrani I think is a super useful kind of reference to have FWIW so thanks already for putting the list you have together)

[Isak Colboubrani]

@Julian Berman Thanks! Found this one for field_simp:

import Mathlib
example (a b : R) [CommRing R] (u₁ : Rˣ) : a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁ := by field_simp

[Kyle Miller]

(Side note @Julian Berman: You know how people tend to use decide for natural number and integer equalities? That's just doing rfl in the end, but with an extra unnecessary step or two. There's no harm in it, but if decide is ok then rfl is too.)

[Isak Colboubrani]

Found this one for rw_search:

import Mathlib
example (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search

@Kim Morrison, is this a good example for rw_search, or do you have any better suggestion?

[Isak Colboubrani]

Presumably unique examples for fun_prop, measurability and positivity:

import Mathlib
example : Measurable fun x : ℝ => (x * x - 1) / x + (x - x*x) := by fun_prop
example [MeasurableSpace α] [MeasurableSpace β] (F : ℕ → α → β) (hF : ∀ i, Measurable (F i)) : Measurable (F 0) := by measurability
example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by positivity

[Isak Colboubrani]

And coherence:

import Mathlib
open CategoryTheory MonoidalCategory
example (C : Type) [CategoryTheory.Category.{v} C] [CategoryTheory.MonoidalCategory C] (f : 𝟙_ C ⟶ _) : f ≫ (λ_ (𝟙_ C)).hom = f ≫ (ρ_ (𝟙_ C)).hom := by coherence

[Isak Colboubrani]

And assumption_mod_cast:

import Mathlib
example (az bz cz : ℤ) (h : (cz : ℚ) = az / bz) : (cz : ℝ) = az / bz := by assumption_mod_cast

[Aaron Liu]

This one for linarith is not unique, contradiction calls decide on the hypothesis here I think.

example (h : 1 < 0) : False := by contradiction

[Kyle Miller]

linarith is meant for linear inequalities anyway; adding some variables to the example would be better.

[Isak Colboubrani]

And arith_mult:

import Mathlib
open ArithmeticFunction
example {R : Type*} [Field R] (n : ℕ) : IsMultiplicative <| (σ n * pow (n + 3)).ppow 2 := by arith_mult

[Isak Colboubrani]

And compute_degree:

import Mathlib
open Polynomial
example [Semiring R] : natDegree (OfNat.ofNat (OfNat.ofNat 0) : R[X]) ≤ 0 := by compute_degree

[Damiano Testa]

simp does not solve the last one?

[Isak Colboubrani]

Oh, it does. Thanks for catching that!

[Isak Colboubrani]

And tfae_finish:

import Mathlib
example (h₁ : P → Q) (h₂ : Q → P) : List.TFAE [P, Q] := by tfae_finish

[Damiano Testa]

I think that for compute_degree you can use

example : natDegree (X + 1 : Nat[X]) ≤ 1 := by
  compute_degree

[Isak Colboubrani]

And mfld_set_tac:

import Mathlib
example (e : PartialEquiv α β) (e' : PartialEquiv β γ) : (e.trans e').source = e.source ∩ Set.preimage e (e.target ∩ e'.source) := by mfld_set_tac

[Isak Colboubrani]

I believe I’ve found a tauto test case that neither aesop nor any other tactic seems able to solve:

import Mathlib
example (P : Nat → Prop) (n : Nat) : P n → n = 7 ∨ n = 0 ∨ ¬ (n = 7 ∨ n = 0) ∧ P n := by tauto

Does anyone have a counterexample tactic (i.e., a tactic other than tauto that solves this) to prove otherwise?

[Aaron Liu]

grind works, with the warning,

"The grind tactic is experimental and still under development. Avoid using it in production projects"

[Isak Colboubrani]

That's really interesting, @Aaron Liu. Thanks for sharing! I’m excited about grind. I’ll keep track of which “unique” test cases the in-development version of grind can handle. For now, I’ll label this test case as “unique for tauto + not-yet-ready-for-production grind.”

[Isak Colboubrani]

From the original list of tactics, I’m still looking for “unique” test cases for the following:

aesop_cat assumption bound constructor continuity contradiction decide dsimp ext infer_instance linarith module omega rfl simp simp_all trivial

Test case contributions are welcome!

I’ve also compiled another list of additional candidate tactics to cover. Which of these do you think are likely—or unlikely—to have a unique test case?

cancel_denoms dsimp eq_refl finiteness finiteness_nonterminal interval_cases itauto match_scalars native_decide nlinarith nofun norm_cast pure_coherence qify rify simp_arith simp_intro subsingleton whisker_simps

[Aaron Liu]

The one for measurability is also not very good, solve_by_elim and tauto both solve it.

Isak Colboubrani said:

Presumably unique examples for fun_prop, measurability and positivity:

import Mathlib
example : Measurable fun x : ℝ => (x * x - 1) / x + (x - x*x) := by fun_prop
example [MeasurableSpace α] [MeasurableSpace β] (F : ℕ → α → β) (hF : ∀ i, Measurable (F i)) : Measurable (F 0) := by measurability
example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by positivity

[Michael Rothgang]

In general, I'm a bit surprised if fun_prop can solve some measurability goal and measurabilitycannot. (The other way around exists, e.g. around measurable sets or since measurability uses aesop.)

[Michael Rothgang]

Similarly for fun_prop and continuity.

[Michael Rothgang]

gcongr could also be worth including

[Tomas Skrivan]

The main point of fun_prop is speed and that it is much better at applying theorems like Continuous.comp, continuous_apply and continuous_pi. For example this is not solvable by continuity

example (f : ℝ → ℝ → ℝ) (hf : Continuous ↿f) (x : ℝ) : Continuous (f x) := by fun_prop

[Tomas Skrivan]

It also works with bundled morphisms, i.e. you can assume that function (f : ℝ → Path (0:ℝ) (1:ℝ)) is jointly continuous and fun_prop infers that it is component wise continuous

example (f : ℝ → Path (0:ℝ) (1:ℝ)) (hf : Continuous ↿f) (x : ℝ) : Continuous (f x ·) := by fun_prop
example (f : ℝ → Path (0:ℝ) (1:ℝ)) (hf : Continuous ↿f) (y : unitInterval) : Continuous (f · y) := by fun_prop

This all scales to arbitrary number of arguments.

example (f : ℝ → ℝ → ℝ → Path (0:ℝ) (1:ℝ)) (hf : Continuous ↿f) (x y : ℝ) : Continuous (↿(f x · y ·)) := by fun_prop

[Isak Colboubrani]

Michael Rothgang said:

gcongr could also be worth including

gcongr was included in the original list and has the following presumably "unique" test case:

example (a b c : ℝ) (h : a ≤ b) : c - Real.exp b ≤ c - Real.exp a := by gcongr

Let me know if this can be solved using any other tactic.

[Isak Colboubrani]

Two presumably unique test cases for decide and omega:

import Mathlib

example : ∀ m, m < 25 → ∀ n, n < 25 → ∀ c, c < 25 → m ^ 2 + n ^ 2 + c ^ 2 ≠ 7 := by decide
example (a : Nat) : (((a + (2 ^ 64 - 1)) % 2 ^ 64 + 1) * 8 - 1 - (a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + 1) = 8 := by omega

[Isak Colboubrani]

Update -- currently at 23 tactics with unique test cases:

import Mathlib
open ArithmeticFunction CategoryTheory MonoidalCategory Polynomial
set_option autoImplicit false

-- Presumably "unique" test cases for each tactic: no other tactic can directly solve these goals.
example (α : Type) (a b : α) [AddCommMonoid α] : a + (b + a) = a + a + b := by abel
example (P : Nat → Prop) (h : {x // P x}) : ∃ x, P x ∧ 0 ≤ x := by aesop
example (R : Type) [Field R] (n : ℕ) : IsMultiplicative <| (σ n * pow (n + 3)).ppow 2 := by arith_mult
example (a b c : ℤ) (h : (c : ℚ) = a / b) : (c : ℝ) = a / b := by assumption_mod_cast
example (C : Type) [CategoryTheory.Category C] [CategoryTheory.MonoidalCategory C] (f : 𝟙_ C ⟶ _) : f ≫ (λ_ (𝟙_ C)).hom = f ≫ (ρ_ (𝟙_ C)).hom := by coherence
example : natDegree (X + 1 : Nat[X]) ≤ 1 := by compute_degree
example : ∀ m, m < 25 → ∀ n, n < 25 → ∀ c, c < 25 → m ^ 2 + n ^ 2 + c ^ 2 ≠ 7 := by decide
example (R : Type) (a b : R) [CommRing R] (u₁ : Rˣ) : a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁ := by field_simp
example : Measurable fun x : ℝ => (x * x - 1) / x + (x - x*x) := by fun_prop
example (a b c : ℝ) (h : a ≤ b) : c - Real.exp b ≤ c - Real.exp a := by gcongr
example (G : Type) (a b c : G) [Group G] : c⁻¹*(b*c⁻¹)*c*(a*b)*(b⁻¹*a⁻¹*b⁻¹)*c = 1 := by group
example (α β γ : Type) (e : PartialEquiv α β) (e' : PartialEquiv β γ) : (e.trans e').source = e.source ∩ Set.preimage e (e.target ∩ e'.source) := by mfld_set_tac
example (R : Type) (a b : R) [Ring R] : (a + b)^3 = a^3 + a^2*b + a*b*a + a*b^2 + b*a^2 + b*a*b + b^2*a + b^3 := by noncomm_ring
example : (2 : ℝ) < 5 / 2 ∧ 5 / 2 < 3 := by norm_num
example (a : Nat) : (((a + (2 ^ 64 - 1)) % 2 ^ 64 + 1) * 8 - 1 - (a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + 1) = 8 := by omega
example (a b c d e f : ℂ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := by polyrith
example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by positivity
example : (-126432 : ZMod 1235412223) ^ 12355342321 = 1001528716 := by reduce_mod_char
example (α : Type) (a b c : α) [LinearOrderedField α] :  a * (-c / b) * (-c / b) + -c + c = a * (c / b * (c / b)) := by ring
example (α : Type) (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by solve_by_elim
example (P : Nat → Prop) (n : Nat) : P n → n = 7 ∨ n = 0 ∨ ¬ (n = 7 ∨ n = 0) ∧ P n := by tauto
example (P Q : Prop) (h₁ : P → Q) (h₂ : Q → P) : List.TFAE [P, Q] := by tfae_finish

-- The following tactics currently lack unique test cases:
--   aesop_cat assumption bound cancel_denoms constructor continuity contradiction
--   dsimp eq_refl ext finiteness finiteness_nonterminal infer_instance interval_cases
--   itauto linarith match_scalars module native_decide nlinarith nofun norm_cast
--   pure_coherence qify rfl rify simp simp_all simp_arith simp_intro subsingleton
--   trivial whisker_simps

[Daniel Weber]

Example for native_decide:

example : ∀ n < 1000, n.gcd (n + 1) = 1 := by native_decide

[Daniel Weber]

trivial attempts all of assumption,rfl,contradiction,decide, so there's no true example for any of them. Here's an example for trivial:

example (m : Nat) (h : m ≠ 1) : True ∧ m ≠ 1 ∧ ∀ n < 100, n^2 < 10000 := by trivial

[Edward van de Meent]

Daniel Weber said:

Example for native_decide:

example : ∀ n < 1000, n.gcd (n + 1) = 1 := by native_decide

importing mathlib, aesop does this too

[Edward van de Meent]

concretely:

import Mathlib
example : ∀ n < 1000, n.gcd (n + 1) = 1 := by
  aesop? says
    intro n a
    simp_all only [Nat.gcd_self_add_right, Nat.gcd_one_right]

[Daniel Weber]

simp also does

[Daniel Weber]

Fixed example:

example : ∀ a, a < 100 → 0 < a → ∀ b, b < 100 → 0 < b → ∀ c, c < 100 → a^3 + b^3 ≠ c^3 := by native_decide

[Daniel Weber]

Example for module:

example [AddCommGroup V] [CommRing K] [Module K V] {x : V} {a b c d : K} : (c - d) • a • x = (a • c • x + b • d • y) - d • (a • x + b • y) := by module

[Daniel Weber]

I doubt rify/zify/qify would have any example, they aren't finishing tactics

[Daniel Weber]

Example for constructor:

structure True' : Prop
example : True' := by constructor

[Daniel Weber]

Any example for dsimp should also be one for rfl, so I don't expect any

[Edward van de Meent]

never once had i considered constructor to be a closing tactic :rolling_on_the_floor_laughing:

[Daniel Weber]

rfl attempts eq_refl, so eq_refl shouldn't have any example

[Edward van de Meent]

Isak Colboubrani said:

example : ∀ m, m < 25 → ∀ n, n < 25 → ∀ c, c < 25 → m ^ 2 + n ^ 2 + c ^ 2 ≠ 7 := by decide

this is solved by native_decide too

[Edward van de Meent]

(to be expected, i guess, as the docstring says it's an alias for decide +native)

[Daniel Weber]

Example for ext (although it's slightly a stretch :laughing: )

inductive Empty'
example (a b : Set Empty') : a = b := by ext ⟨⟩

[Markus Himmel]

Daniel Weber said:

although it's slightly a stretch

It is useful sometimes if you're too lazy to type by subsingleton :)

[Edward van de Meent]

i wonder if there is a nice one for contradiction

[Daniel Weber]

It's subsumed by trivial, but maybe ignoring that :thinking:

[Daniel Weber]

Example for finiteness:

import Mathlib

example (a : ℝ) : (ENNReal.ofReal (1 + a ^ 2))⁻¹ < ⊤ := by finiteness

[Daniel Weber]

finiteness_nonterminal shouldn't have any example

[Daniel Weber]

Example for infer_instance:

example : Field ℚ := by infer_instance

[Edward van de Meent]

is this a thing?

example {R : Type*} [LinearOrderedRing R] (x:R) (hx : x > 0): 0 < x ^ 9348 := by
  positivity

[Edward van de Meent]

ah nvm we had that one already

[Bryan Gin-ge Chen]

At least for the mathlib tactics, these seem like good examples to add to the tactic docstrings, if they're not already there. (In general I think we still have too few examples in those docstrings.)

[Edward van de Meent]

does anyone know, is assumption subsumed by trivial?

[Daniel Weber]

itauto should be subsumed by tauto if you aren't looking at the axioms used

[Henrik Böving]

Isak Colboubrani said:

Update -- currently at 23 tactics with unique test cases:

import Mathlib
open ArithmeticFunction CategoryTheory MonoidalCategory Polynomial
set_option autoImplicit false

-- Presumably "unique" test cases for each tactic: no other tactic can directly solve these goals.
example (α : Type) (a b : α) [AddCommMonoid α] : a + (b + a) = a + a + b := by abel
example (P : Nat → Prop) (h : {x // P x}) : ∃ x, P x ∧ 0 ≤ x := by aesop
example (R : Type) [Field R] (n : ℕ) : IsMultiplicative <| (σ n * pow (n + 3)).ppow 2 := by arith_mult
example (a b c : ℤ) (h : (c : ℚ) = a / b) : (c : ℝ) = a / b := by assumption_mod_cast
example (C : Type) [CategoryTheory.Category C] [CategoryTheory.MonoidalCategory C] (f : 𝟙_ C ⟶ _) : f ≫ (λ_ (𝟙_ C)).hom = f ≫ (ρ_ (𝟙_ C)).hom := by coherence
example : natDegree (X + 1 : Nat[X]) ≤ 1 := by compute_degree
example : ∀ m, m < 25 → ∀ n, n < 25 → ∀ c, c < 25 → m ^ 2 + n ^ 2 + c ^ 2 ≠ 7 := by decide
example (R : Type) (a b : R) [CommRing R] (u₁ : Rˣ) : a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁ := by field_simp
example : Measurable fun x : ℝ => (x * x - 1) / x + (x - x*x) := by fun_prop
example (a b c : ℝ) (h : a ≤ b) : c - Real.exp b ≤ c - Real.exp a := by gcongr
example (G : Type) (a b c : G) [Group G] : c⁻¹*(b*c⁻¹)*c*(a*b)*(b⁻¹*a⁻¹*b⁻¹)*c = 1 := by group
example (α β γ : Type) (e : PartialEquiv α β) (e' : PartialEquiv β γ) : (e.trans e').source = e.source ∩ Set.preimage e (e.target ∩ e'.source) := by mfld_set_tac
example (R : Type) (a b : R) [Ring R] : (a + b)^3 = a^3 + a^2*b + a*b*a + a*b^2 + b*a^2 + b*a*b + b^2*a + b^3 := by noncomm_ring
example : (2 : ℝ) < 5 / 2 ∧ 5 / 2 < 3 := by norm_num
example (a : Nat) : (((a + (2 ^ 64 - 1)) % 2 ^ 64 + 1) * 8 - 1 - (a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + 1) = 8 := by omega
example (a b c d e f : ℂ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := by polyrith
example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by positivity
example : (-126432 : ZMod 1235412223) ^ 12355342321 = 1001528716 := by reduce_mod_char
example (α : Type) (a b c : α) [LinearOrderedField α] :  a * (-c / b) * (-c / b) + -c + c = a * (c / b * (c / b)) := by ring
example (α : Type) (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by solve_by_elim
example (P : Nat → Prop) (n : Nat) : P n → n = 7 ∨ n = 0 ∨ ¬ (n = 7 ∨ n = 0) ∧ P n := by tauto
example (P Q : Prop) (h₁ : P → Q) (h₂ : Q → P) : List.TFAE [P, Q] := by tfae_finish

-- The following tactics currently lack unique test cases:
--   aesop_cat assumption bound cancel_denoms constructor continuity contradiction
--   dsimp eq_refl ext finiteness finiteness_nonterminal infer_instance interval_cases
--   itauto linarith match_scalars module native_decide nlinarith nofun norm_cast
--   pure_coherence qify rfl rify simp simp_all simp_arith simp_intro subsingleton
--   trivial whisker_simps

If you're interested in less mathematical tactics as well, bv_decide can do some fancy stuff like:

import Std.Tactic.BVDecide

example (x : BitVec 32) :
    x + x.sdiv 8#32 * 4294967288#32 &&& 1#32 = x &&& 1#32 := by
  bv_decide

Which I'm pretty sure no other tactic will solve for you.

[Isak Colboubrani]

@Henrik Böving Every tactic $t$ available after import Mathlib that "uniquely solves" example a : b := by t for some $a$ and $b$ is of interest. Thus, bv_decide is a welcome addition! Thanks!

[Isak Colboubrani]

@Daniel Weber Very nice findings. Thanks a lot! I've added the finiteness, infer_instance, module, native_decide, and trivial examples to the collection.

[Isak Colboubrani]

It seems that all the examples I’ve tested for aesop_cat can also be solved by aesop. Is this expected, and does it hold in general? Or is there a case where aesop_cat succeeds while aesop does not?

#mwe

import Mathlib
open CategoryTheory Limits MonoidalCategory

example (C : Type) [Category C] (X Y : C) (α : X ≅ Y) (f : Aut X) : α.conjAut f = α.symm ≪≫ f ≪≫ α := by aesop
example (C : Type) [Category C] [HasFiniteProducts C] [HasPullbacks C] (X₁ X₂ : Dial C) : (𝟙 X₁ ⊗ 𝟙 X₂ : _ ⟶ _) = 𝟙 (X₁ ⊗ X₂ : Dial C) := by aesop
example (C : Type) [Category C] (D : Type) [Category D] (e : C ≌ D) : e.changeFunctor (Iso.refl _) = e := by aesop

example (C : Type) [Category C] (X Y : C) (α : X ≅ Y) (f : Aut X) : α.conjAut f = α.symm ≪≫ f ≪≫ α := by aesop_cat
example (C : Type) [Category C] [HasFiniteProducts C] [HasPullbacks C] (X₁ X₂ : Dial C) : (𝟙 X₁ ⊗ 𝟙 X₂ : _ ⟶ _) = 𝟙 (X₁ ⊗ X₂ : Dial C) := by aesop_cat
example (C : Type) [Category C] (D : Type) [Category D] (e : C ≌ D) : e.changeFunctor (Iso.refl _) = e := by aesop_cat

[Isak Colboubrani]

The following 16 tactics currently lack unique test cases:

aesop_cat bound cancel_denoms continuity
linarith match_scalars nlinarith nofun norm_cast
pure_coherence simp simp_all simp_arith simp_intro
subsingleton whisker_simps

I'm a bit surprised that I can't construct a unique test case for linarith (or nlinarith). Should I be?

Are any of these 16 tactics particularly unlikely to have a unique example?

Even better—can you come up with a unique example for any of them?

[Isak Colboubrani]

I think this is a unique test case for bound:

import Mathlib

example (a b : ℝ) (h1 : ‖a‖ ≤ ‖b‖) (h2 : 3 ≤ ‖b‖) : ‖b ^ 2 + a‖ ≥ ‖b ^ 2‖ - ‖a‖ ∧  ‖b ^ 2‖ - ‖a‖ ≥ ‖b ^ 2‖ - ‖b‖ ∧ (‖b‖ - 1) * ‖b‖ ≥ 2 * ‖b‖ := by bound

Does anyone have a counterexample tactic (i.e., a tactic other than bound that solves this) to prove otherwise?

[Kyle Miller]

Isak Colboubrani said:

I've added [...] native_decide [...]

(Just note that native_decide is not accepted in mathlib contributions. It uses the docs#Lean.ofReduceBool axiom, which is a way for the kernel to call out to user-defined compiled code via docs#Lean.reduceBool to more efficiently evaluate a boolean value. There are many tricks to get native_decide to prove false things. But, with careful auditing, the risk can be bounded. Just pointing this out so that things it can do don't count against unique capabilities of other tactics.)

[Mario Carneiro]

Do we have a native_decide linter in mathlib?

[Damiano Testa]

I don't think that there is a native_decide linter, but it seems to only be used in MathlibTest/Polynomial.lean.

[Isak Colboubrani]

Update -- currently at 29 tactics with unique test cases:

import Mathlib

set_option autoImplicit false
open ArithmeticFunction CategoryTheory MonoidalCategory Polynomial

-- Presumably "unique" test cases for each tactic: no other tactic can directly solve these goals.
example (α : Type) (a b : α) [AddCommMonoid α] : a + (b + a) = a + a + b := by abel
example (P : Nat → Prop) (h : {x // P x}) : ∃ x, P x ∧ 0 ≤ x := by aesop
example (R : Type) [Field R] (n : ℕ) : IsMultiplicative <| (σ n * pow (n + 3)).ppow 2 := by arith_mult
example (a b c : ℤ) (h : (c : ℚ) = a / b) : (c : ℝ) = a / b := by assumption_mod_cast
example (a b : ℝ) (h1 : ‖a‖ ≤ ‖b‖) (h2 : 3 ≤ ‖b‖) : ‖b ^ 2 + a‖ ≥ ‖b ^ 2‖ - ‖a‖ ∧  ‖b ^ 2‖ - ‖a‖ ≥ ‖b ^ 2‖ - ‖b‖ ∧ (‖b‖ - 1) * ‖b‖ ≥ 2 * ‖b‖ := by bound
example (x : BitVec 32) : x + x.sdiv 8#32 * 4294967288#32 &&& 1#32 = x &&& 1#32 := by bv_decide
example (C : Type) [CategoryTheory.Category C] [CategoryTheory.MonoidalCategory C] (f : 𝟙_ C ⟶ _) : f ≫ (λ_ (𝟙_ C)).hom = f ≫ (ρ_ (𝟙_ C)).hom := by coherence
example : natDegree (X + 1 : Nat[X]) ≤ 1 := by compute_degree
example : ∀ m, m < 25 → ∀ n, n < 25 → ∀ c, c < 25 → m ^ 2 + n ^ 2 + c ^ 2 ≠ 7 := by decide
example (R : Type) (a b : R) [CommRing R] (u₁ : Rˣ) : a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁ := by field_simp
example (a : ℝ) : (ENNReal.ofReal (1 + a ^ 2))⁻¹ < ⊤ := by finiteness
example : Measurable fun x : ℝ => (x * x - 1) / x + (x - x*x) := by fun_prop
example (a b c : ℝ) (h : a ≤ b) : c - Real.exp b ≤ c - Real.exp a := by gcongr
example (G : Type) (a b c : G) [Group G] : c⁻¹*(b*c⁻¹)*c*(a*b)*(b⁻¹*a⁻¹*b⁻¹)*c = 1 := by group
example : Field ℚ := by infer_instance
example (α β γ : Type) (e : PartialEquiv α β) (e' : PartialEquiv β γ) : (e.trans e').source = e.source ∩ Set.preimage e (e.target ∩ e'.source) := by mfld_set_tac
example (V K : Type)[AddCommGroup V] [CommRing K] [Module K V] {x y : V} {a b c d : K} : (c - d) • a • x = (a • c • x + b • d • y) - d • (a • x + b • y) := by module
example (R : Type) (a b : R) [Ring R] : (a + b)^3 = a^3 + a^2*b + a*b*a + a*b^2 + b*a^2 + b*a*b + b^2*a + b^3 := by noncomm_ring
example : (2 : ℝ) < 5 / 2 ∧ 5 / 2 < 3 := by norm_num
example (a : Nat) : (((a + (2 ^ 64 - 1)) % 2 ^ 64 + 1) * 8 - 1 - (a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + 1) = 8 := by omega
example (a b c d e f : ℂ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := by polyrith
example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by positivity
example : (-126432 : ZMod 1235412223) ^ 12355342321 = 1001528716 := by reduce_mod_char
example (α : Type) (a b c : α) [LinearOrderedField α] :  a * (-c / b) * (-c / b) + -c + c = a * (c / b * (c / b)) := by ring
example (α : Type) (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by rw_search
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by solve_by_elim
example (P : Nat → Prop) (n : Nat) : P n → n = 7 ∨ n = 0 ∨ ¬ (n = 7 ∨ n = 0) ∧ P n := by tauto
example (m : Nat) (h : m ≠ 1) : True ∧ m ≠ 1 ∧ ∀ n < 100, n^2 < 10000 := by trivial
example (P Q : Prop) (h₁ : P → Q) (h₂ : Q → P) : List.TFAE [P, Q] := by tfae_finish
-- The following tactics currently lack unique test cases:
--   aesop_cat cancel_denoms continuity interval_cases linarith
--   match_scalars nlinarith nofun norm_cast pure_coherence simp
--   simp_all simp_arith simp_intro subsingleton whisker_simps
--
-- Contributions welcome!

[Aaron Liu]

Your example for fun_prop is also solved (a lot more slowly) by measurability.

import Mathlib

example : Measurable fun x : ℝ => (x * x - 1) / x + (x - x*x) := by measurability

[Damiano Testa]

The solve_by_elim example is also solved by exact? and aesop.

[Rado Kirov]

That's a great list, thanks for compiling it! Some of these look quite non-minimal, would it be worth trying to make them minimal while preserving the uniqueness property? I tried to give it a shot, but to test the uniqueness I need have an automated test that no other tactic solves it. It is easy to script, but a fresh run of lake lean <one_line_generated_file.lean> takes ~2min each on my machine! I thought its due to rechecking Mathlib, but AFAIKT it uses -t=max by default (I have no idea what I am doing)?

[Damiano Testa]

Here is a simple-minded modification of hint that tries out all tactics and reports which goals are solved by exactly one tactic and which ones are solved by more than one.

import Mathlib

/-!
This is a straightforward (and buggy!) modification of `hint`
that tries out several tactics and reports which ones are successful.
-/

-- clear the `hint` cache
run_cmd
  Lean.modifyEnv (Mathlib.Tactic.Hint.hintExtension.setState · [])

-- add the tactics that we want to test for uniqueness
register_hint abel
register_hint aesop
register_hint arith_mult
register_hint assumption_mod_cast
register_hint bound
register_hint bv_decide
register_hint coherence
register_hint compute_degree
register_hint decide
register_hint field_simp
register_hint finiteness
register_hint fun_prop
register_hint gcongr
register_hint infer_instance
register_hint group
register_hint mfld_set_tac
register_hint module
register_hint noncomm_ring
register_hint norm_num
register_hint omega
register_hint polyrith
register_hint positivity
register_hint reduce_mod_char
register_hint ring
register_hint rw_search
register_hint solve_by_elim
register_hint tauto
register_hint trivial
register_hint tfae_finish

open Lean Elab Mathlib Meta Tactic Hint TryThis in
def hint (stx : Syntax) : TacticM Unit := withMainContext do
  let tacs := Nondet.ofList (← getHints)
  let results := tacs.filterMapM fun t : TSyntax `tactic => do
    if let some msgs ← observing? (withMessageLog (withoutInfoTrees ((do evalTactic t; evalTactic (← `(tactic| done))) <|> return))) then
      return some (← getGoals, ← suggestion t msgs)
    else
      return none
  let results ← (results.toMLList).asArray
  let results := results.filter (·.1.1.isEmpty)
  addSuggestions stx (results.map (·.1.2))
  for r in results do
    setMCtx r.2.term.meta.meta.mctx
  if results.size != 1 then
    logWarning "More than one tactic solves the goal!"

/-- Try all the registered tactics and report which ones solve the goal. -/
syntax (name := uniqueTacStx) "unique_tac" : tactic

@[inherit_doc uniqueTacStx]
elab_rules : tactic
  | `(tactic| unique_tac%$tk) => hint tk

set_option autoImplicit false
open ArithmeticFunction CategoryTheory MonoidalCategory Polynomial

-- Presumably "unique" test cases for each tactic: no other tactic can directly solve these goals.
example (α : Type) (a b : α) [AddCommMonoid α] : a + (b + a) = a + a + b := by unique_tac
example (P : Nat → Prop) (h : {x // P x}) : ∃ x, P x ∧ 0 ≤ x := by unique_tac
example (R : Type) [Field R] (n : ℕ) : IsMultiplicative <| (σ n * pow (n + 3)).ppow 2 := by unique_tac
example (a b c : ℤ) (h : (c : ℚ) = a / b) : (c : ℝ) = a / b := by unique_tac
example (a b : ℝ) (h1 : ‖a‖ ≤ ‖b‖) (h2 : 3 ≤ ‖b‖) : ‖b ^ 2 + a‖ ≥ ‖b ^ 2‖ - ‖a‖ ∧  ‖b ^ 2‖ - ‖a‖ ≥ ‖b ^ 2‖ - ‖b‖ ∧ (‖b‖ - 1) * ‖b‖ ≥ 2 * ‖b‖ := by unique_tac
example (x : BitVec 32) : x + x.sdiv 8#32 * 4294967288#32 &&& 1#32 = x &&& 1#32 := by unique_tac
example (C : Type) [CategoryTheory.Category C] [CategoryTheory.MonoidalCategory C] (f : 𝟙_ C ⟶ _) : f ≫ (λ_ (𝟙_ C)).hom = f ≫ (ρ_ (𝟙_ C)).hom := by unique_tac
example : natDegree (X + 1 : Nat[X]) ≤ 1 := by unique_tac
example : ∀ m, m < 25 → ∀ n, n < 25 → ∀ c, c < 25 → m ^ 2 + n ^ 2 + c ^ 2 ≠ 7 := by unique_tac
example (R : Type) (a b : R) [CommRing R] (u₁ : Rˣ) : a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁ := by unique_tac
example (a : ℝ) : (ENNReal.ofReal (1 + a ^ 2))⁻¹ < ⊤ := by unique_tac
example : Measurable fun x : ℝ => (x * x - 1) / x + (x - x*x) := by unique_tac
example (a b c : ℝ) (h : a ≤ b) : c - Real.exp b ≤ c - Real.exp a := by unique_tac
example (G : Type) (a b c : G) [Group G] : c⁻¹*(b*c⁻¹)*c*(a*b)*(b⁻¹*a⁻¹*b⁻¹)*c = 1 := by unique_tac
example : Field ℚ := by unique_tac
example (α β γ : Type) (e : PartialEquiv α β) (e' : PartialEquiv β γ) : (e.trans e').source = e.source ∩ Set.preimage e (e.target ∩ e'.source) := by unique_tac
example (V K : Type)[AddCommGroup V] [CommRing K] [Module K V] {x y : V} {a b c d : K} : (c - d) • a • x = (a • c • x + b • d • y) - d • (a • x + b • y) := by unique_tac
example (R : Type) (a b : R) [Ring R] : (a + b)^3 = a^3 + a^2*b + a*b*a + a*b^2 + b*a^2 + b*a*b + b^2*a + b^3 := by unique_tac
example : (2 : ℝ) < 5 / 2 ∧ 5 / 2 < 3 := by unique_tac
example (a : Nat) : (((a + (2 ^ 64 - 1)) % 2 ^ 64 + 1) * 8 - 1 - (a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + 1) = 8 := by unique_tac
example (a b c d e f : ℂ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := by unique_tac
example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by unique_tac
example : (-126432 : ZMod 1235412223) ^ 12355342321 = 1001528716 := by unique_tac
example (α : Type) (a b c : α) [LinearOrderedField α] :  a * (-c / b) * (-c / b) + -c + c = a * (c / b * (c / b)) := by unique_tac
example (α : Type) (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by unique_tac
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by unique_tac
example (P : Nat → Prop) (n : Nat) : P n → n = 7 ∨ n = 0 ∨ ¬ (n = 7 ∨ n = 0) ∧ P n := by unique_tac
example (m : Nat) (h : m ≠ 1) : True ∧ m ≠ 1 ∧ ∀ n < 100, n^2 < 10000 := by unique_tac
example (P Q : Prop) (h₁ : P → Q) (h₂ : Q → P) : List.TFAE [P, Q] := by unique_tac
-- The following tactics currently lack unique test cases:
--   aesop_cat cancel_denoms continuity interval_cases linarith
--   match_scalars nlinarith nofun norm_cast pure_coherence simp
--   simp_all simp_arith simp_intro subsingleton whisker_simps
--
-- Contributions welcome!

[Damiano Testa]

It is buggy and produces some errors, but, when it does not have errors, it seems to correctly report whether exactly one tactic solves the goal (with a blue squiggle) and when more than one solves the goal (with a yellow squiggle).

[Damiano Testa]

Some of the errors are timeouts/max-depth overflows, others I do not really understand.

[Rado Kirov]

Neat! Starring this as a good example of the power of custom tactics (once I get to learning those).

[Isak Colboubrani]

@Damiano Testa The hint modification is incredibly useful—thank you for your help!

[Damiano Testa]

I am glad that it is helpful! I wish it was more stable...

[Isak Colboubrani]

It appears that several test cases are not unique:

• The abel test case is solved also by module
• The aesop test case is solved also by bound
• The decide test case is solved also by trivial
• The fun_prop test case is solved also by measurability
• The gcongr test case is solved also by bound
• The mfld_set_tac test case is solved also by aesop
• The norm_num test case is solved also by bound
• The positivity test case is solved also by finiteness and field_simp
• The ring test case is solved also by group
• The solve_by_elim test case is solved also by aesop, arith_mult, bound and tauto

[Damiano Testa]

Do not just trust the output of hint1: verify that what it says is actually true! :smile:

[Isak Colboubrani]

I did! :)

[Damiano Testa]

I think that if it exits with no errors it is reliable, but there is a lot of internal hiding/catching of errors that I am not entirely sure of this.

[Isak Colboubrani]

Verification #mwe:

import Mathlib

set_option autoImplicit false
open ArithmeticFunction CategoryTheory MonoidalCategory Polynomial

-- abel test case is not unique
example (α : Type) (a b : α) [AddCommMonoid α] : a + (b + a) = a + a + b := by abel
example (α : Type) (a b : α) [AddCommMonoid α] : a + (b + a) = a + a + b := by module

-- aesop test case is not unique
example (P : Nat → Prop) (h : {x // P x}) : ∃ x, P x ∧ 0 ≤ x := by aesop
example (P : Nat → Prop) (h : {x // P x}) : ∃ x, P x ∧ 0 ≤ x := by bound

-- decide test case is not unique
example : ∀ m, m < 25 → ∀ n, n < 25 → ∀ c, c < 25 → m ^ 2 + n ^ 2 + c ^ 2 ≠ 7 := by decide
example : ∀ m, m < 25 → ∀ n, n < 25 → ∀ c, c < 25 → m ^ 2 + n ^ 2 + c ^ 2 ≠ 7 := by trivial

-- fun_prop test case is not unique
example : Measurable fun x : ℝ => (x * x - 1) / x + (x - x*x) := by fun_prop
example : Measurable fun x : ℝ => (x * x - 1) / x + (x - x*x) := by measurability

-- gcongr test case is not unique
example (a b c : ℝ) (h : a ≤ b) : c - Real.exp b ≤ c - Real.exp a := by gcongr
example (a b c : ℝ) (h : a ≤ b) : c - Real.exp b ≤ c - Real.exp a := by bound

-- mfld_set_tac test case is not unique
example (α β γ : Type) (e : PartialEquiv α β) (e' : PartialEquiv β γ) : (e.trans e').source = e.source ∩ Set.preimage e (e.target ∩ e'.source) := by mfld_set_tac
example (α β γ : Type) (e : PartialEquiv α β) (e' : PartialEquiv β γ) : (e.trans e').source = e.source ∩ Set.preimage e (e.target ∩ e'.source) := by aesop

-- norm_num test case is not unique
example : (2 : ℝ) < 5 / 2 ∧ 5 / 2 < 3 := by norm_num
example : (2 : ℝ) < 5 / 2 ∧ 5 / 2 < 3 := by bound

-- positivity test case is not unique
example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by positivity
example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by finiteness
example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by field_simp

-- solve_by_elim test case is not unique
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by solve_by_elim
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by aesop
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by arith_mult
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by bound
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by tauto

-- ring test case is not unique
example (α : Type) (a b c : α) [LinearOrderedField α] :  a * (-c / b) * (-c / b) + -c + c = a * (c / b * (c / b)) := by ring
example (α : Type) (a b c : α) [LinearOrderedField α] :  a * (-c / b) * (-c / b) + -c + c = a * (c / b * (c / b)) := by group

[Damiano Testa]

By the way, if you can find a goal that is solved by exactly one tactic that is nice. But even goals that are solved by multiple tactics can still be pedagogically useful to know what you should expect a tactic to be able to solve.

[Aaron Liu]

Beware the false-positives! They sneak in.

import Mathlib

set_option autoImplicit false

-- `bound` is build off `aesop`
example (P : Nat → Prop) (h : {x // P x}) : ∃ x, P x ∧ 0 ≤ x := by aesop
example (P : Nat → Prop) (h : {x // P x}) : ∃ x, P x ∧ 0 ≤ x := by bound

-- `trivial` is calling `decide`
example : ∀ m, m < 25 → ∀ n, n < 25 → ∀ c, c < 25 → m ^ 2 + n ^ 2 + c ^ 2 ≠ 7 := by decide
example : ∀ m, m < 25 → ∀ n, n < 25 → ∀ c, c < 25 → m ^ 2 + n ^ 2 + c ^ 2 ≠ 7 := by trivial

-- `bound` calls `norm_num`
example : (2 : ℝ) < 5 / 2 ∧ 5 / 2 < 3 := by norm_num
example : (2 : ℝ) < 5 / 2 ∧ 5 / 2 < 3 := by bound

-- `finiteness` and `field_simp` both call `positivity`
example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by positivity
example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by finiteness
example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by field_simp

-- I strongly suspect all of these are calling `solve_by_elim`
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by solve_by_elim
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by aesop
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by arith_mult
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by bound
example (α : Nat → Type) (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by tauto

-- `group` is calling `ring`
example (α : Type) (a b c : α) [LinearOrderedField α] :  a * (-c / b) * (-c / b) + -c + c = a * (c / b * (c / b)) := by ring
example (α : Type) (a b c : α) [LinearOrderedField α] :  a * (-c / b) * (-c / b) + -c + c = a * (c / b * (c / b)) := by group

[Isak Colboubrani]

Yes, @Aaron Liu , that's an excellent point, and it was exactly my next step—to investigate which of these are "real duplicates" as defined in the first post of this thread: "By ‘uniquely solved,’ I loosely mean that no other tactic can directly solve these goals unless it internally calls the same ‘primary tactic.’"

Thank you for helping me with that investigation!

It seems that the remaining "real duplicates" after this investigation are as follows:

import Mathlib

set_option autoImplicit false
open ArithmeticFunction CategoryTheory MonoidalCategory Polynomial

-- abel test case is not unique
example (α : Type) (a b : α) [AddCommMonoid α] : a + (b + a) = a + a + b := by abel
example (α : Type) (a b : α) [AddCommMonoid α] : a + (b + a) = a + a + b := by module

-- fun_prop test case is not unique
example : Measurable fun x : ℝ => (x * x - 1) / x + (x - x*x) := by fun_prop
example : Measurable fun x : ℝ => (x * x - 1) / x + (x - x*x) := by measurability

-- gcongr test case is not unique
example (a b c : ℝ) (h : a ≤ b) : c - Real.exp b ≤ c - Real.exp a := by gcongr
example (a b c : ℝ) (h : a ≤ b) : c - Real.exp b ≤ c - Real.exp a := by bound

-- mfld_set_tac test case is not unique
example (α β γ : Type) (e : PartialEquiv α β) (e' : PartialEquiv β γ) : (e.trans e').source = e.source ∩ Set.preimage e (e.target ∩ e'.source) := by mfld_set_tac
example (α β γ : Type) (e : PartialEquiv α β) (e' : PartialEquiv β γ) : (e.trans e').source = e.source ∩ Set.preimage e (e.target ∩ e'.source) := by aesop

[Isak Colboubrani]

Generally, test cases that can be solved by gcongr are often also solvable by bound or aesop. However, the following test case is solved exclusively by gcongr:

example (b : ℕ) (hb : 3 ≡ b [ZMOD 5]) : b ^ 2 ≡ 3 ^ 2 [ZMOD 5] := by gcongr

[Isak Colboubrani]

I haven’t been able to create a test case that can be solved by abel but not by module (which makes some sense). Is it possible to create such a test case, or does the module tactic indeed have a strictly broader capability set than the abel tactic?

[Isak Colboubrani]

Generally, the test cases I have tested that can be solved by fun_prop are often also solvable by continuity. However, the following test case is solved exclusively by fun_prop:

example {α} [MeasurableSpace α] (f : α → α → α) (hf : Measurable fun (x,y) => f x y) (a : α) : Measurable (fun x => (f x a, f (f x x) (f (f x x) x))) := by fun_prop

[Isak Colboubrani]

The following test case seems to be exclusively solved by nlinarith:

example (x y : ℚ) : 0 ≤ x*x + y*y := by nlinarith

[Isak Colboubrani]

Turns out the positivity test case was not unique since it could be solved also by nlinarith:

example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by positivity
example (a b : ℚ) (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by nlinarith

Luckily I found this even simpler test case that is solved exclusively by positivity:

example (a : ℤ) : 0 < |a| + 3 := by positivity

[Isak Colboubrani]

I think I found a better omega exclusive test case too:

example (a : ℤ) (hlt : 1 ≤ a) (hne : a ≠ 1) : 1 < a := by omega

... is solved only by omega and is much simpler than the previous omega exclusive test case …

example (a : ℤ) : (((a + (2 ^ 64 - 1)) % 2 ^ 64 + 1) * 8 - 1 - (a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + 1) = 8 := by omega

[Damiano Testa]

I think that exact? solves the new omega example.

[Aaron Liu]

only if you import Mathlib

[Damiano Testa]

I thought that it was with import Mathlib, though.

[Isak Colboubrani]

Thanks @Damiano Testa, you're right! Reverting to the previous omega test case.

#mwe

import Mathlib

example (a : ℤ) (hlt : 1 ≤ a) (hne : a ≠ 1) : 1 < a := by omega
example (a : ℤ) (hlt : 1 ≤ a) (hne : a ≠ 1) : 1 < a := by exact?

example (a : ℤ) : (((a + (2 ^ 64 - 1)) % 2 ^ 64 + 1) * 8 - 1 - (a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + 1) = 8 := by omega

[Isak Colboubrani]

Yes, import Mathlib is assumed. From a previous message:

Every tactic $t$ available after import Mathlib that "uniquely solves" example a : b := by t for some $a$ and $b$ is of interest.

…

For demonstration purposes, I’m compiling a list of goals that are “uniquely solved” by certain closing tactics (with zero arguments). By “uniquely solved,” I loosely mean that no other tactic can directly solve these goals unless it internally calls the same “primary tactic.”

[Isak Colboubrani]

I believe I’ve found a grind test case that no other tactic seems able to solve:

import Mathlib
example (P : Nat → Prop) (hp : P Nat.zero.succ) (h : ∀ n, P n ↔ P n.succ) : P Nat.zero.succ.succ.succ.succ := by grind

[Isak Colboubrani]

Found a few more presumably "unique" grind test cases:

import Mathlib
example {α} (a b c : α) [LE α] : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b := by grind
example (f : Nat → Nat) (a b c d e : Nat) : f (a + 3) = b → f (c + 1) = d → c ≤ a + 2 → a + 1 ≤ e → e < c → b = d := by grind
example (a b : Nat) (f : Nat → Nat) : f 1 = a → b ≤ 1 → b ≥ 1 → f b = a := by grind
example (a b c : Nat)  (f : Nat → Nat) : f 2 = a → b ≤ 1 → b ≥ 1 → c = b + 1 → f c = a := by grind

[Daniel Weber]

tauto can solve the first one

[Isak Colboubrani]

Oh, you're right. Thanks for pointing out that counterexample.

Updated list of presumably "unique" grind test cases:

import Mathlib

example (P : Nat → Prop) (hp : P Nat.zero.succ) (h : ∀ n, P n ↔ P n.succ) : P Nat.zero.succ.succ.succ.succ := by grind
example (f : Nat → Nat) (a b c d e : Nat) : f (a + 3) = b → f (c + 1) = d → c ≤ a + 2 → a + 1 ≤ e → e < c → b = d := by grind
example (a b : Nat) (f : Nat → Nat) : f 1 = a → b ≤ 1 → b ≥ 1 → f b = a := by grind
example (a b c : Nat)  (f : Nat → Nat) : f 2 = a → b ≤ 1 → b ≥ 1 → c = b + 1 → f c = a := by grind

[Isak Colboubrani]

And here's another, perhaps more interesting presumably "unique" grind test case:

import Mathlib
example {α : Type*} {p : α → Prop} {a : α} {s : Set α} (h : ∀ a ∈ s, ∃ b ∈ s, p a ∧ p b) (h' : a ∈ s) : ∃ b ∈ s, p b := by grind

[Isak Colboubrani]

One new and one improved "unique" test case solvable only by positivity:

import Mathlib
open Nat
example (n : ℕ) : 0 < (n)! + (n + 1)! := by positivity
example (n : ℤ) : 0 < |n| + 1 := by positivity

[Isak Colboubrani]

Found a new "unique" test case solvable only by bound, which is a bit simpler than the old test case:

import Mathlib
-- new test case
example (x y : ℝ) (h₁ : 0 ≤ y) (h₂ : x ≤ y) : x / y ≤ 1 := by bound
-- old test case
example (a b : ℝ) (h₁ : ‖a‖ ≤ ‖b‖) (h₂ : 3 ≤ ‖b‖) : ‖b ^ 2 + a‖ ≥ ‖b ^ 2‖ - ‖a‖ ∧ ‖b ^ 2‖ - ‖a‖ ≥ ‖b ^ 2‖ - ‖b‖ ∧ (‖b‖ - 1) * ‖b‖ ≥ 2 * ‖b‖ := by bound

[Isak Colboubrani]

Found one unique test case for continuity and one for fun_prop:

import Mathlib

example {W X Y Z : Type*} [TopologicalSpace W] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
  (f : C(X, Y)) (g : C(W, Z)) : Continuous (Prod.map f g) := by continuity

example {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] {x₀ : α} (f : α → α → β)
  (hf : ContinuousAt (Function.uncurry f) (x₀, x₀)) :
  ContinuousAt (fun x ↦ f x x) x₀ := by fun_prop

[Isak Colboubrani]

Found a pretty nice "unique" test case solvable only by tauto_set:

import Mathlib

example {α : Type*} (s t u : Set α) : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by tauto_set

[Isak Colboubrani]

Found a presumably unique test case solvable only by monicity!:

import Mathlib
open Polynomial
example {R : Type*} [Ring R] : Monic (X ^ 2 + X + 1 : R[X]) := by monicity!

[Isak Colboubrani]

Is there a test case that simp_all can close but aesop cannot?

From what I understand, aesop calls simp_all in at least some situations, but I’m not sure if aesop is a strict superset of simp_all in terms of capabilities.

[Isak Colboubrani]

Adding a "unique" test case solvable only by the exciting and still under development grind tactic:

import Mathlib
example (x y : ℤ) : 27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45 → -10 ≤ 7*x - 9*y → 7*x - 9*y ≤ 4 → False := by grind

[Isak Colboubrani]

Found a presumably unique test case solvable only by abel:

import Mathlib
example {α} [AddCommMonoid α] (a b c d: α) : a + b + c + d + 0 = d + (c + b) + (0 + 0 + a) := by abel

[Isak Colboubrani]

Found a presumably unique test case solvable only by aesop_cat:

import Mathlib
open CategoryTheory MonoidalCategory
example {C} [Category C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X₁ X₂ : Dial C) : (𝟙 X₁ ⊗ 𝟙 X₂ : _ ⟶ _) = 𝟙 (X₁ ⊗ X₂ : Dial C) := by aesop_cat