remove classical!

Stream: mathlib4

[Sébastien Gouëzel]

@Kim Morrison, you have removed all the uses of classical! in mathlib. I have a use of classical! in a PR (#12207), so I would like to learn what is recommended. Its use is in the line

     map_add' := by classical!; simp [iteratedFDeriv_aux]

where replacing it with classical doesn't work, for purely syntactic reasons: I can do

      map_add' := by
        classical
        simp [iteratedFDeriv_aux]

but I don't know how to keep it on a single line. Should I just switch to the multiline version?

[Kim Morrison]

I guess so. I'm never particularly concerned about newlines, so it doesn't seem much of a cost to me. Can you write by classical { ... }?

[Mario Carneiro]

the one line version is by classical simp [iteratedFDeriv_aux]

[Sébastien Gouëzel]

In fact I don't care to have it on a single line or several lines. I guess my question is rather: can we fix classical so that it works on single lines, just like most other tactics? It would be good for coherence.

[Mario Carneiro]

the reason it's not by classical; simp is because classical is a block tactic, like try

[Sébastien Gouëzel]

ok, thanks for the explanations. I've switched to by classical simp [iteratedFDeriv_aux]. Still a little bit surprising that by classical!; simp works but by classical; simp doesn't, but I can definitely live with that (although minimizing surprises for newcomers would probably be good, so if there's a way to get by classical; simp to work it might be worth it...)

[Kevin Buzzard]

And would you expect that to turn on classical for the entire proof or just for the simp line? I presume the point of making it a block tactic was precisely to stop it leaking out of an argument.

[Kevin Buzzard]

If that's the argument then shouldn't classical! also be a block tactic?

[Ruben Van de Velde]

No, classical! should get lost :)

[Mario Carneiro]

Kevin Buzzard said:

If that's the argument then shouldn't classical! also be a block tactic?

The operation of classical! is fundamentally leaky, so there was no point in presenting it as a block tactic because it doesn't stop working after the block

[Kyle Miller]

Sébastien Gouëzel said:

if there's a way to get by classical; simp to work it might be worth it...)

I think all we'd need to do is add ";"? like in the following:

elab "classical" ";"? tacs:ppDedent(tacticSeq) : tactic => do
  classical <| Elab.Tactic.evalTactic tacs