by_contra when goal is an implication

Stream: mathlib4

[Dan Velleman]

It looks to me like by_contra doesn't work if the goal is an implication. Consider this (silly) example:

example (P : Prop) : P → P := by
  by_contra

I get the error message tactic 'apply' failed, failed to unify (¬?p → False) → ?p with P → P.
I assume what's going on here is that by_contra is doing apply Classical.byContradiction, which fails because it tries to unify Classical.byContradiction with P → P and the unification fails. However, apply Classical.byContradiction _ would succeed--the blank gives Lean the clue that it should be applying Classical.byContradiction to something to get P → P. So should by_contra be redefined to use apply Classical.byContradiction _?

[Mario Carneiro]

I think it should be refine Classical.byContradiction ?_ then

[Mario Carneiro]

apply always seems to be problematic in general code because of this issue

[Dan Velleman]

What's the difference between _ and ?_?

[Mario Carneiro]

?_ in refine become new proof goals, _ have to be solved by unification. So refine Classical.byContradiction _ would be an error because it can't infer the rest of the proof

[Dan Velleman]

Thanks.