exfalso puzzle

Stream: batteries

[Kevin Buzzard]

Is it possible to solve a goal with the exfalso tactic?

[Ruben Van de Velde]

I claim yes

[Mario Carneiro]

Solution

example {A} : False → A := by exfalso

[Eric Wieser]

Is this a bug in docs#Std.Tactic.tacticExfalso ? Should it use refine False.elim ?_ instead of apply False.elim?

[Eric Wieser]

std4#540, assuming the answer is yes

[Kevin Buzzard]

Of course this was a student in my class who discovered this (with precisely Mario's example, which is an early problem in my course notes), and then asked me how the proof worked, and initially I was like "..."

[Kim Morrison]

Personally I think that this behaviour is fine. It's no more or less confusing than apply already is (i.e. that it might apply an unexpected number of arguments).

[Eric Wieser]

apply is indeed confusing, but I don't think other tactics should inherit this confusion by leaking implementation details if it's easy to avoid that

[Eric Wieser]

It's certainly a very minor bug, since the only way this can cause confusion is by unexpectedly solving things

[Mario Carneiro]

unexpectedly solving things is bad for tactics that use exfalso as a component and have some expectation of what it does

[Kevin Buzzard]

It certainly confused the undergraduate who had only started using lean a few days before and had been told it would change the goal to False.