tactics that have no effect

Stream: lean4

[Kayla Thomas]

Is Lean 4 different in that, for example, if simp finds no simplifications, it still succeeds? Is the only indication of this that the goal does not change and nothing in the goal is highlighted in green? Is it possible to have the tactic in the .lean file be highlighted in some way?

[Mario Carneiro]

you can wrap the tactic in fail_if_no_progress

[Kayla Thomas]

I see.

[Mario Carneiro]

(that is a workaround, I think we will probably make simp do this automatically at some point)

[Kayla Thomas]

Can the whole tactic proof be wrapped like that, or would it need to be wrapped around each tactic?

[Kayla Thomas]

(I am assuming that simp is not the only tactic that does this)

[Mario Carneiro]

Each tactic would have to be wrapped, or you can (should) make a macro which does the wrapping

[Mario Carneiro]

macro "simp" : tactic => `(tactic| fail_if_no_progress simp)

(untested, might loop)

[Kayla Thomas]

Ok. Thank you.

[Kayla Thomas]

Seems to work.

[Kayla Thomas]

Is there a way to have it also work with simp at?

[Mario Carneiro]

section
open Lean Parser Tactic
syntax (name := simp') "simp" (config)? (discharger)? (&" only")?
  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? (location)? : tactic

macro_rules (kind := simp')
  | stx => `(tactic| fail_if_no_progress $(⟨stx.setKind ``Tactic.simp⟩))
end

[Damiano Testa]

I'm not at a computer right now, but rw and simp_rw have a similar behaviour... :upside_down:

[Kayla Thomas]

Mario Carneiro said:

section
open Lean Parser Tactic
syntax (name := simp') "simp" (config)? (discharger)? (&" only")?
  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? (location)? : tactic

macro_rules (kind := simp')
  | stx => `(tactic| fail_if_no_progress $(⟨stx.setKind ``Tactic.simp⟩))
end

Thank you!

[Mario Carneiro]

I would argue that not erroring is the correct behavior for rw [], and also for rw [show 1 = 1 by rfl] on f 1

[Mario Carneiro]

rw [show 1 = 1 by rfl] on f 2 should error (and does error)

[Damiano Testa]

Mario, sure. However, sometimes (not just with rw) I am confused as to whether not seeing a change in the infoview is a consequence of a tactic having done nothing or of having no pretty-printed effect. It would be nice to have a flag to avoid "useless" tactics.

[Damiano Testa]

Ah, i remembered that congr also does nothing silently!

[Scott Morrison]

On the subject, !4#4774 has been sitting on the review queue for a while: it proposes making casesm fail if it doesn't do anything.

[Mac Malone]

Mario Carneiro said:

macro "simp" : tactic => `(tactic| fail_if_no_progress simp)

Would simp! be a good name for this tactic?

[Mac Malone]

Also, in general would it be reasonable to overload the ! suffix for these kind of actions?

[Scott Morrison]

I'd really prefer if the default behaviour on doing nothing is failure.

It is easier to do flow control in tactics that use these tactics as building blocks, it is more informative to the user, and in particular it gives better information as the behaviour of tactics in a committed proof change due to changes in the simp set, etc.

[Scott Morrison]

No one likes having to inspect the goal state carefully to see if it actually changed after calling simp.

[Damiano Testa]

A recent example where I would have liked this, is the change to push_neg. During the port, right after calls to push_neg there were simp [not_...] calls, to remove the ¬ that were left by the earlier tactic. These simps are now silently doing nothing.

[Damiano Testa]

An example with simp_rw instead of simp is the change in PartitionOfUnity in !4#5132.

[Damiano Testa]

Also, fail_if_no_progress tests isDefEq, whereas maybe actual term equality (or something in-between) might be better.