Prove by matching specific natural numbers in Lean

November 18, 2023

I’m trying to prove in Lean 4 that for the naturals: q + q ^ 2 ≠ 7

So far, I have this proof:

example : q + q ^ 2 ≠ 7 := by
  intro h
  have q00 : q = 0 ∨ 0 < q := by exact Nat.eq_zero_or_pos q
  cases q00
  case inl h0 => -- q = 0
    have h' : q + q ^ 2 = 7 := h
    rw [h0] at h'
    norm_num at h'
  case inr hq => -- q ≥ 1 
    have q01 : q = 1 ∨ 2 ≤ q := by exact LE.le.eq_or_gt hq
    cases q01
    case inl q1 => -- q = 1
      have h' : q + q ^ 2 = 7 := h
      rw [q1] at h'
      norm_num at h'
    case inr qge2 => -- q ≥ 2
      have q2or : q = 2 ∨ 3 ≤ q := by exact LE.le.eq_or_gt qge2
      cases q2or
      case inl q2 => -- q = 2
        have h'' : q + q ^ 2 = 7 := h
        rw [q2] at h''
        norm_num at h''
      case inr qge3 => -- q ≥ 3
        have q2ge9 : 9 ≤ q * q := by exact Nat.mul_le_mul qge3 qge3
        rw [← Nat.pow_two] at q2ge9
        linarith only [h, q2ge9]

Two questions:

I’d like to implement a simpler pattern matching proof preserving a similar structure. Something like:

example : q + q ^ 2 ≠ 7 := by
  match q with
  | 0 => norm_num
  | 1 => norm_num
  | 2 => norm_num
  | _ =>
    sorry

Maybe it would need the zero and succ q case patterns?

The statement is very simple, so I’d like ideas for a simpler proof, even if totally distinct.

>Solution :

In Lean 3 the omega tactic would have done this in one line. This tactic is still being ported to Lean 4 and the last I heard was that we could be hoping to see it early next year. Until then, this works:

import Mathlib.Tactic

example (q : ℕ) : q + q ^ 2 ≠ 7 := by
  match q with
  | 0 => norm_num
  | 1 => norm_num
  | 2 => norm_num
  | (n + 3) =>
    ring_nf -- 12 + 7n + n^2 ≠ 7
    apply ne_of_gt -- 7 < 12 + 7n + n^2
    rw [Nat.add_assoc] -- 7 < 12 + blah
    apply Nat.lt_add_right -- 7 < 12
    linarith