Lean4
LanguageTactics
Module 6 · Lesson 2

push_neg

Push negations inward through logical connectives and quantifiers.push_neg applies De Morgan's laws and negation rules automatically.

❗
push_neg requires Mathlib. Addimport Mathlib.Tactic.PushNeg orimport Mathlib.Tactic.

Basic Usage

When you have a negation in front of a compound statement, push_negpushes the negation inward, applying De Morgan's laws and quantifier duality. The result is often easier to work with than the original negated form.

lean
1import Mathlib.Tactic.PushNeg
2
3-- push_neg transforms negations
4example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q := by
5  constructor
6  · intro h
7    push_neg at h  -- h becomes: ¬P ∨ ¬Q (not quite, actually P → ¬Q)
8    sorry
9  · intro h
10    push_neg
11    sorry
12
13-- More practically:
14example (h : ¬(∀ x : Nat, x > 0)) : ∃ x : Nat, x ≤ 0 := by
15  push_neg at h
16  -- h is now: ∃ x, x ≤ 0
17  exact h
Key Takeaway
push_neg converts "not forall" to "exists not" and "not exists" to "forall not", and simplifies comparisons.

Negating Quantifiers

The most common use of push_neg is negating quantifiers. "Not for all" becomes "there exists not," and "not exists" becomes "for all not." This transformation often reveals what you actually need to prove or find.

lean
1import Mathlib.Tactic.PushNeg
2
3-- ¬∀ becomes ∃¬
4example (h : ¬∀ n : Nat, n = 0) : ∃ n : Nat, n ≠ 0 := by
5  push_neg at h
6  exact h
7
8-- ¬∃ becomes ∀¬
9example (h : ¬∃ n : Nat, n > 100) : ∀ n : Nat, n ≤ 100 := by
10  push_neg at h
11  exact h

Negating Comparisons

lean
1import Mathlib.Tactic.PushNeg
2
3-- push_neg simplifies negated comparisons
4example (h : ¬(x < y)) : x ≥ y := by
5  push_neg at h
6  exact h
7
8example (h : ¬(x ≤ y)) : x > y := by
9  push_neg at h
10  exact h
11
12example (h : ¬(x = y)) : x ≠ y := by
13  -- Already in simplest form
14  exact h

Negating Implications

lean
1import Mathlib.Tactic.PushNeg
2
3-- ¬(P → Q) becomes P ∧ ¬Q
4example (h : ¬(P → Q)) : P ∧ ¬Q := by
5  push_neg at h
6  exact h
7
8-- Works with quantified implications
9example (h : ¬(∀ x : Nat, x > 0 → x ≥ 1)) : ∃ x : Nat, x > 0 ∧ x < 1 := by
10  push_neg at h
11  exact h
ℹ
push_neg transforms ¬(P → Q)to P ∧ ¬Q, which is logically equivalent in classical logic.

On the Goal

lean
1import Mathlib.Tactic.PushNeg
2
3-- push_neg can also transform the goal
4example : ¬(∀ n : Nat, n < n + 1 → n = 0) := by
5  push_neg
6  -- Goal becomes: ∃ n, n < n + 1 ∧ n ≠ 0
7  use 1
8  simp
9
10-- Useful for proving negations
11example : ¬(∀ f : Nat → Nat, ∃ x, f x = 0) := by
12  push_neg
13  -- Goal: ∃ f, ∀ x, f x ≠ 0
14  use fun _ => 1
15  simp
Deep Dive: push_neg Rules

push_neg applies these transformations:

  • ¬(P ∧ Q) → P → ¬Q
  • ¬(P ∨ Q) → ¬P ∧ ¬Q
  • ¬(P → Q) → P ∧ ¬Q
  • ¬∀ x, P x → ∃ x, ¬P x
  • ¬∃ x, P x → ∀ x, ¬P x
  • ¬(a < b) → a ≥ b
  • ¬(a ≤ b) → a > b

Combined with Other Tactics

lean
1import Mathlib.Tactic.PushNeg
2import Mathlib.Tactic.Cases
3
4-- push_neg then rcases
5example (h : ¬∀ x : Nat, x = 0 ∨ x > 10) : ∃ x : Nat, x ≠ 0 ∧ x ≤ 10 := by
6  push_neg at h
7  -- h : ∃ x, x ≠ 0 ∧ x ≤ 10
8  exact h
9
10-- push_neg in contrapositive proofs
11example (h : ¬Q) (hpq : P → Q) : ¬P := by
12  intro hp
13  exact h (hpq hp)

Real-World Examples

Epsilon-Delta Negation

lean
1import Mathlib.Tactic.PushNeg
2
3-- Negating a limit definition
4-- "f doesn't converge to L" means:
5-- ∃ ε > 0, ∀ δ > 0, ∃ x, |x - a| < δ ∧ |f x - L| ≥ ε
6example (h : ¬∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| < δ → |f x - L| < ε) :
7    ∃ ε > 0, ∀ δ > 0, ∃ x, |x - a| < δ ∧ |f x - L| ≥ ε := by
8  push_neg at h
9  exact h

Counterexample Finding

lean
1import Mathlib.Tactic.PushNeg
2
3-- Show that not all functions have fixed points
4example : ¬∀ f : Nat → Nat, ∃ x, f x = x := by
5  push_neg
6  -- Need: ∃ f, ∀ x, f x ≠ x
7  use (· + 1)  -- successor function
8  intro x
9  omega

Bounds and Suprema

lean
1import Mathlib.Tactic.PushNeg
2
3-- "M is not an upper bound" means some element exceeds it
4example (h : ¬∀ x ∈ S, x ≤ M) : ∃ x ∈ S, x > M := by
5  push_neg at h
6  exact h

Common Patterns

lean
1import Mathlib.Tactic.PushNeg
2
3-- Proving something is not bounded
4example : ¬∃ M : Nat, ∀ n : Nat, n ≤ M := by
5  push_neg
6  -- ∀ M, ∃ n, n > M
7  intro M
8  use M + 1
9  omega
10
11-- Proving functions are different
12example : (fun x : Nat => x + 1) ≠ (fun x => x) := by
13  intro h
14  have : 1 = 0 := congrFun h 0
15  omega
Exercise: Push a Negation

Use push_neg to transform a negated universal.

lean
1import Mathlib.Tactic.PushNeg
2
3example (h : ¬∀ x : Nat, x = 0) : ∃ x : Nat, x ≠ 0 := by
4  push_neg at h
5  exact h
rcases & obtainNext: contrapose