by_contra

Summary

The by_contra tactic is a “proof by contradiction” tactic. If your goal is ⊢ P then by_contra h introduces a hypothesis h : ¬P and changes the goal to false.

Example

Here is a proof of ¬ ¬ P → P.

example (P : Prop) : ¬ ¬ P → P :=
begin
  intro hnnP, -- assume ¬ ¬ P
  by_contra hnP, -- goal is now false
  apply hnnP, -- goal is now ¬ P
  exact hnP,
end

Make a new Lean file in a Lean project and cut and paste the above code into it. See if you can understand the logic.

Further notes

The by_contra tactic is strictly stronger than the exfalso tactic in that not only does it change the goal to false but it also throws in an extra hypothesis. However exfalso often terminates in under a millisecond, a speed which by_contra can only dream of.