Tactic hierarchies in Lean/Mathlib

Stream: new members

[Isak Colboubrani]

For educational purposes, I am exploring the relationships between various tactics in Lean/Mathlib, particularly looking at situations where certain tactics can be considered as encompassing the functionalities of others. This involves identifying scenarios where one tactic may act as a "superset" in terms of its capabilities relative to another tactic.

A trivial yet possibly far-fetched example to illustrate this point (assuming my understanding of these tactics is correct):

If a single remaining goal can be successfully closed by employing any tactic from the following list, then it's guaranteed that all tactics listed above it can also close the goal:

• aesop (Mathlib)
• …
• simp_all (Lean)
• …
• simp (Lean)
• …
• rfl (Lean)

Put differently, if a comprehensive tactic like aesop, considered the most encompassing in this hierarchy, fails to resolve a single remaining goal, it's unnecessary to attempt using the tactics that rank lower in this list (to close the goal in one go). (This is based on the understanding that aesop incorporates strategies equivalent to simp_all, among other more sophisticated methods of course.)

Is this correct?

Are there other similar tactic hierarchies?

[Bolton Bailey]

Interesting initiative. Another tactic hierarchy I might think of for this would involve apply/convert and maybe some other tactics, though those tactics take arguments.

[Damiano Testa]

A small correction: simp does not "imply" rfl.

def myZero : Nat := 0

-- fails
example : myZero = 0 := by simp

-- works
example : myZero = 0 := by rfl

[Damiano Testa]

In fact, you can also trick simp_all into not working, when simp does work:

import Mathlib.Data.Nat.Basic
import Mathlib.Algebra.GroupWithZero.Basic

@[simp]
theorem ohNo (m n : Nat) : m = n ↔ 2 * m = 2 * n := by
  simp only [mul_eq_mul_left_iff, Nat.succ_ne_zero, or_false]

example (n : Nat) (h : n = 2 * n) : True := by
  simp_all  -- times out, while `simp` works.

Although this seems a little contrived and #lint complains that ohNo is not great as a simp lemma!

[Isak Colboubrani]

Thanks!

It might be more accurate to represent the relationships between these tactics using a tree structure, where each parent node represents a tactic that is more comprehensive or powerful (in the sense outlined above) than its child nodes (descendants).

In this structure:

  aesop
  ├─ simp_all
  ├─ trivial
     ├─ apply True.intro
     ├─ apply And.intro <;> trivial
     ├─ assumption
     ├─ contradiction
     ├─ decide
     ├─ rfl
        ├─ eq_refl
     ├─ simp

Is this representation more accurate, or are there counterexamples that challenge it?

[Yaël Dillies]

Again, there are some cases that aesop can't do which rfl can

[Damiano Testa]

While I agree that for pedagogical purposes this is a good place to start, in any "real-word" situation, unless a tactic is essentially defined as "try one tactic first and then do something else" it is almost never true that one tactic is strictly more powerful than another.

[Martin Dvořák]

I am always a bit surprised when rfl closes a goal that simp cannot.

[Isak Colboubrani]

Yaël Dillies said:

Again, there are some cases that aesop can't do which rfl can

This is quite unexpected to me (possibly due to my novice status in this field!). Would anyone be able to illustrate such a case, especially one a student might realistically encounter?"

[Damiano Testa]

Here is a simple example:

import Mathlib.Tactic

@[irreducible]
def m : Nat := 0

example : m = 0 := by aesop  -- fails
example : m = 0 := by rfl  -- works

[Damiano Testa]

Here is a small tour over the transparencies:

import Mathlib.Tactic

def noSimp : Nat := 0
example : noSimp = 0 := by aesop
example : noSimp = 0 := by simp -- fails
example : noSimp = 0 := by rfl

@[irreducible] def onlyRfl : Nat := 0
example : onlyRfl = 0 := by aesop -- fails
example : onlyRfl = 0 := by simp -- fails
example : onlyRfl = 0 := by rfl

abbrev allWork : Nat := 0
example : allWork = 0 := by aesop
example : allWork = 0 := by simp
example : allWork = 0 := by rfl

[Isak Colboubrani]

@Damiano Testa Thank you! Your examples have been enlightening, and they've guided me towards further reading.

Based on what I've learned today, here's my revised representation of the "tactic hierarchy" introduced above:

  aesop
  ├─ trivial
     ├─ apply True.intro
     ├─ apply And.intro <;> trivial
     ├─ assumption
     ├─ contradiction
     ├─ decide
  simp
  simp_all
  rfl
  ├─ eq_refl

Is this structure accurate, or are there still counterexamples that could potentially challenge this arrangement?

[Damiano Testa]

I do not think that aesop uses decide:

import Mathlib.Tactic
example : ∀ n, n ≤ 0 → Nat.divisors n ≠ {n} := by
  --aesop -- fails to close goal
  decide  -- works, as does `trivial`

[Damiano Testa]

Maybe I can say here something that I tell my students.

Having a rough mental picture of a partial ordering of the tactics is certainly very useful and also close to how my intuition works. However, "proving theorems" is undecidable, so no algorithm can consistently close all goals. And in particular, no algorithm can do everything that all algorithms can do. So, pushing too far this partial order is not too useful and I would even say it is undesirable: having many different algorithms, means having more theorems they will prove collectively!

So, having tactics that do not supersede each other is a goal to try to achieve, in my opinion!

[Damiano Testa]

Here is another example showing that you can "trick" even the tactics that are defined in terms of each other from really being "stronger":

import Mathlib.Tactic

example (h : ∀ n, n ≤ 160 → ¬ 161 ∣ n) : ∀ n, n ≤ 160 → ¬ 161 ∣ n := by
  --trivial -- max recursion
  --decide  -- max recursion
  assumption -- works

[Damiano Testa]

In fact, in this last example, if you reduce the imports to just import Mathlib.Data.Nat.Basic, then trivial works!

I'll leave you to figure out why this is the case! :wink:

[Yaël Dillies]

I think it's much better to emphasize what kinds of goals each tactic can close