contrapose

1import Mathlib.Tactic.Contrapose
2
3-- contrapose transforms: prove P → Q by proving ¬Q → ¬P
4example (h : P) : Q → P := by
5  intro _
6  exact h
7
8-- Same proof using contrapose
9example : (n = 0 → n * n = 0) := by
10  intro h
11  simp [h]
12
13example : (n * n ≠ 0 → n ≠ 0) := by
14  contrapose  -- Changes goal to: n = 0 → n * n = 0
15  intro h
16  simp [h]

1import Mathlib.Tactic.Contrapose
2import Mathlib.Tactic.PushNeg
3
4-- contrapose! also applies push_neg
5example : (∀ n : Nat, n > 0 → n ≥ 1) := by
6  intro n
7  contrapose!
8  -- Goal changes from: n > 0 → n ≥ 1
9  -- to: n < 1 → n ≤ 0 (with push_neg applied)
10  intro h
11  omega

1import Mathlib.Tactic.Contrapose
2
3-- Sometimes the contrapositive is more natural
4-- "If n² is even, then n is even"
5-- Easier as: "If n is odd, then n² is odd"
6
7example (n : Nat) : (∃ k, n = 2 * k) → ∃ k, n * n = 2 * k := by
8  intro ⟨k, hk⟩
9  use 2 * k * k
10  omega
11
12-- The contrapositive might be easier in some cases
13-- But for this example, direct is fine

1import Mathlib.Tactic.Contrapose
2
3-- contrapose can work on hypotheses too
4example (h : P → Q) (hnq : ¬Q) : ¬P := by
5  exact fun hp => hnq (h hp)
6
7-- Using contrapose directly on hypothesis
8example (h : P → Q) : ¬Q → ¬P := by
9  intro hnq hp
10  exact hnq (h hp)

1import Mathlib.Tactic.Contrapose
2
3-- Proof by contradiction: assume ¬conclusion, derive False
4example (h : P) : ¬¬P := by
5  intro hnp
6  exact hnp h
7
8-- Contraposition: swap hypothesis and conclusion, negate both
9-- To prove P → Q, prove ¬Q → ¬P
10
11-- They're related but different techniques!
12-- Contradiction: assumes negation of what you want
13-- Contraposition: changes the structure of implication

1import Mathlib.Tactic.Contrapose
2
3-- If a divides bc and gcd(a,b) = 1, then a divides c
4-- Contrapositive: If a doesn't divide c, then...
5-- (Sometimes the direct proof is still easier)

1import Mathlib.Tactic.Contrapose
2
3-- f is injective iff f(x) = f(y) → x = y
4-- Contrapositive: x ≠ y → f(x) ≠ f(y)
5
6example (f : Nat → Nat) (hf : ∀ x y, f x = f y → x = y) :
7    ∀ x y, x ≠ y → f x ≠ f y := by
8  intro x y hne hfeq
9  exact hne (hf x y hfeq)

1import Mathlib.Tactic.Contrapose
2
3-- Classic: √2 is irrational
4-- Contrapositive: If √2 = p/q (rational), derive contradiction
5-- This is actually proof by contradiction, but contraposition
6-- can help structure parts of the argument
7
8example (h : ¬(∃ p q : Nat, q ≠ 0 ∧ p * p = 2 * q * q)) :
9    ¬(∃ r : Rat, r * r = 2) := by
10  intro ⟨r, hr⟩
11  sorry  -- Full proof needs more machinery

1import Mathlib.Tactic.Contrapose
2
3-- Pattern: prove implication by contrapositive
4-- When conclusion is "positive" and hypothesis is "negative"
5-- Or when negated forms are simpler
6
7-- Example: If f(x) ≠ 0 for all x > 0, then f has no positive roots
8-- Contrapositive: If f has a positive root, then f(x) = 0 for some x > 0
9example (f : Nat → Int) : 
10    (∃ x, x > 0 ∧ f x = 0) → ¬(∀ x, x > 0 → f x ≠ 0) := by
11  intro ⟨x, hx_pos, hfx⟩
12  push_neg
13  exact ⟨x, hx_pos, hfx⟩

1import Mathlib.Tactic.Contrapose
2import Mathlib.Tactic.ByContra
3
4-- by_contra assumes ¬goal and tries to derive False
5example (h : P) : P := by
6  by_contra hnp
7  exact hnp h
8
9-- contrapose changes the structure of an implication goal
10-- They're complementary techniques!