Module 4 - Lesson 3

by_contra and by_cases

by_contra and by_cases are classic proof-structuring tactics. One proves a goal by contradiction; the other splits the goal into two cases.

by_contra: Proof by Contradiction

by_contra h changes a goal Pinto a goal False, while adding h : Not Pto the context. You then derive a contradiction.

lean

1example (P : Prop) (h : Not P -> False) : P := by
2  by_contra hP
3  exact h hP

Key Takeaway

by_contra turns a direct proof into a contradiction proof: assume Not P and derive False.

by_cases: Split on a Proposition

by_cases h : P creates two goals: one withh : P and one with h : Not P. You solve each branch separately.

lean

1example (P : Prop) : Or P (Not P) := by
2  by_cases h : P
3  case pos =>
4    exact Or.inl h
5  case neg =>
6    exact Or.inr h

Case Splits on Equalities

lean

1example (n : Nat) : Or (n = 0) (Not (n = 0)) := by
2  by_cases h : n = 0
3  case pos =>
4    exact Or.inl h
5  case neg =>
6    exact Or.inr h

ℹ

by_contra and by_cases use classical reasoning. If you want constructive proofs, prefer tactics that rely on explicit Decidable instances.

Exercise: Case Split

Prove a disjunction by splitting on a case.

lean

1example (n : Nat) : n = 0 ∨ n ≠ 0 := by
2  by_cases h : n = 0
3  · exact Or.inl h
4  · exact Or.inr h

Deep Dive: Related Tools

For transformations around negation, also see contraposeand push_neg. They help turn goals into a form whereby_contra or by_cases is effective.

conv - Targeted Rewriting Next: Tactic Combinators