Tactic strength pairs: correctness and completeness

Stream: new members

[Isak Colboubrani]

Are these two claims accurate? Please help me refute them with concrete counterexamples, or let me know if you believe they are unfalsifiable.

Claim 1. In each of the following pairs, the first tactic is strictly stronger than the second. That is, any goal closed by the second tactic is also closed by the first (and not vice versa; additionally, to exclude trivial cases, both tactics in each pair must be capable of closing some goals, and both must be zero-argument).

• (aesop, congr)
• (aesop, simp_all)
• (module, abel)
• (nlinarith, linarith)
• (tauto, itauto)
• (trivial, assumption)
• (trivial, contradition)
• (trivial, decide)
• (trivial, rfl)

Claim 2. The list is complete, meaning that no other tactic pairs exhibit this property.

[Aaron Liu]

Claim 1 is false, because you can poison tactics.

[Aaron Liu]

Here's an example where I poison trivial: #Lean for teaching > Game about finishing tactics @ 💬

[Aaron Liu]

Claim 2 is probably false, I found (solve_by_elim, assumption)

[Aaron Liu]

There's also (norm_num, norm_num1) and other similar pairs.

[Aaron Liu]

Also (sorry, *)

[Isak Colboubrani]

Hehe, I was considering adding a restriction "excluding examples resulting from Aaron's clever 'recursion depth' poisoning trick," but you beat me to it! :) Consider that restriction hereby added.

[Isak Colboubrani]

Another restriction to make it more interesting: "strength" achieved from using the sorryAx axiom is not counted :)

[Isak Colboubrani]

@Aaron Liu (solve_by_elim, assumption) is a nice addition to the list. Nice find—thank you! What pairs, or class of pairs, are you referring to that are similar to (norm_num, norm_num1)?

[Aaron Liu]

Isak Colboubrani said:

What pairs, or class of pairs, are you referring to that are similar to (norm_num, norm_num1)?

(abel, abel1)
(ac_nf, ac_nf0)
(rfl, eq_refl)
(norm_cast, norm_cast0)
(norm_num, norm_num1)
(ring, ring1)
(ring!, ring1!)
etc.

[Aaron Liu]

Now that I have these written down, I think some of these pairs don't close strictly more goals.

[Isak Colboubrani]

@Aaron Liu Thanks! If we omit the ones you're uncertain about, what remains?

[Aaron Liu]

Ok, I just checked and all of these pairs are correct.

[Isak Colboubrani]

Below are the updated claims, revised in light of yesterday's counterexample findings (thanks @Aaron Liu -- you're skilled!).

Are these two claims accurate? Please help me refute them with concrete counterexamples, or let me know if you believe they are unfalsifiable.

Claim 1. In each of the following pairs, the first tactic is strictly stronger than the second. That is, any goal closed by the second tactic is also closed by the first (and not vice versa):

• (abel, abel1)
• (ac_nf, ac_nf0)
• (aesop, congr)
• (aesop, simp_all)
• (module, abel)
• (nlinarith, linarith)
• (norm_cast, norm_cast0)
• (norm_num, norm_num1)
• (rfl, eq_refl)
• (ring, ring1)
• (ring!, ring1!)
• (solve_by_elim, assumption)
• (tauto, itauto)
• (trivial, assumption)
• (trivial, contradition)
• (trivial, decide)
• (trivial, rfl)

(Restrictions to exclude the most trivial cases: 1.) both tactics in each pair must be capable of closing some goals, 2.) both tactics must be zero-argument, 3.) we exclude examples resulting from Aaron's clever "recursion depth" poisoning trick, 4.) we also forbid the use of the sorryAx axiom.)

Claim 2. The list is complete, meaning that no other tactic pairs exhibit this property.

[Aaron Liu]

I will add (aesop, split) and (abel!, abel1!) to that.

[Robin Arnez]

add (rfl, apply_rfl)

[Robin Arnez]

also (norm_num, simp) ideally but non-confluence might get in the way

[Aaron Liu]

Robin Arnez said:

also (norm_num, simp) ideally but non-confluence might get in the way

Is norm_num stronger than simp!?

[Kevin Buzzard]

norm_num is norm_num1 + simp

[Robin Arnez]

well, to be exact, norm_num is simp using norm num extensions which makes this possible which norm_num1; simp can't do:

example : (1 : ℚ) + [2][0] = 3 := by
  norm_num