trouble starting a simple proof (n^2+n is even)

Stream: new members

[rzeta0]

I've been following The Mechanics of Proof and am about 1/4 way through.

I wanted to challenge myself and think of a simple theorem to prove - without referring to the course, most of whose exercises are about completing a starter set of code.

I wanted to prove that $n^2+n$ is always even, for integer $n$.

Here is my formulation using quantifiers (which I'm new to):

$$(\forall n \in \mathbb{N}) \, [\exists k \in \mathbb{N} : n^2+n = 2k]$$

I think this is a correct formulation, but do tell me if I'm wrong.

The lean proof header should then start as:

example {n : ℕ} : ∃ k: ℕ, n^2 + n = 2*k := by

I think this correctly translates the theorem with quantifiers.

I then want to prove by cases, $n$ odd, and $n$ even.

This is where I have trouble getting started:

example {n : ℕ} : ∃ k: ℕ, n^2 + n = 2*k := by
  apply Nat.even_or_odd n
  · -- even n case
    -- show n=2*m leads to n^2 + n = 4*m^2 + 2*m = 2*k
  · -- off n case
    -- show n=2*m+1 leads to n^2 + n = 4*m^2 +4*m + 1 + 2*m + 1 = 2*k

The first problem I find is that `apply Nat.even_or_odd n" doesn't replace the proof goal with a disjunction with even and odd cases. Perhaps this lemma isn't meant to be applied to a goal?

If I think work forwards, not backwards from the proof goal, and construct an intermediate hypothesis:

example {n : ℕ} : ∃ k: ℕ, n^2 + n = 2*k := by
  have h: Nat.even_or_odd n
  obtain ha | hb := h
  · -- even n case
    -- show n=2*m leads to n^2 + n = 4*m^2 + 2*m = 2*k
  · -- off n case
    -- show n=2*m+1 leads to n^2 + n = 4*m^2 +4*m + 1 + 2*m + 1 = 2*k

This gives me an error which I don't understand.

type expected, got
  (Nat.even_or_odd n : Even n ∨ Odd n)

I'd appreciate help suitable for a beginner like me.

To be clear: I want to avoid using the Odd and Even definitions and see if I can do this just algebraically.

[Daniel Weber]

You can't apply Nat.even_or_odd n, as the goal isn't Even n ∨ Odd n. The problem in your forwards reasoning is that the syntax for have is have h : <type> := <value>, and in your case Nat.even_or_odd n is the value. You can do

have h : Even n ∨ Odd n := Nat.even_or_odd n
obtain ha | hb := h

or directly

obtain ha | hb := Nat.even_or_odd n

[rzeta0]

thank you - this is helpful.

[rzeta0]

actually i'm getting a tactic failed error:

import Mathlib.Tactic

example {n : ℕ} : ∃ k: ℕ, n^2 + n = 2*k := by
  have h := Nat.even_or_odd' n -- < -- errors relate to this line
  obtain ha | hb := h

errors

12_using_lemmas.lean:7:9
rcases tactic failed: x✝ : ?m.405 is not an inductive datatype
12_using_lemmas.lean:7:20
function expected at
  h
term has type
  ∃ k, n = 2 * k ∨ n = 2 * k + 1

I can see that h has a quantifier before the disjunction - how should this be handled?

Normally i'd use use for the goal, not a hypothesis.

[Derek Rhodes]

please ignore this if you'd rather not bother with it yet, but your question nerd sniped me . Here's one way to do it without mentioning odd or even at all, it uses recursion which is mentioned later on in chapter 6 among the topic strong induction:

theorem sans_parity (n : ℕ) : ∃ k: ℕ, n^2 + n = 2*k := by
  match n with
  | 0 => use 0; ring
  | 1 => use 1; ring
  | n+2 =>
    · have h := sans_parity n
      obtain ⟨p, hp⟩ := h
      have h₁ :=
        calc (n + 2) ^ 2 + (n + 2)
          _= n^2 + 4*n + 4 + n + 2 := by ring
          _= n^2 + n + 4*n + 6 := by ring
          _= 2*p + 4*n + 6 := by rw [hp]
      rw [h₁]
      use p + 2*n + 3
      ring

I couldn't get simple_induction working because of the pesky 2, tried a bunch of ways.

[rzeta0]

Hi Derek - yes that's far too advanced for me :)

[Damiano Testa]

If you want to use Nat.even_or_odd', you should "deconstruct" more: try with obtain ⟨k, (rfl | rfl)⟩ := n.even_or_odd'.

[Damiano Testa]

The first angle bracket extracts the witness for the existential and the property that the existential satisfies. The round bracket extracts the two sides of the or. Finally, rfl is a way to get Lean to notice that the two sides of the or are of the form n = something, and it makes Lean replace n with whatever it is equal to.

[rzeta0]

I finally got this working - well, no errors reported.

I'd welcome comments and feedback.

-- 12 - Using Lemmas

import Mathlib.Tactic

example {n : ℕ} : ∃ k: ℕ, n^2 + n = 2*k := by
  have h : ∃ m, n = 2 * m ∨ n = 2 * m + 1 := Nat.even_or_odd' n
  obtain ⟨m , hm⟩ := h
  obtain ha | hb := hm
  · use 2*m^2 + m
    calc
      n^2 + n = (2*m)^2 + (2*m) := by rw [ha]
      _ = 4*m^2 + 2*m := by ring
      _ = 2*(2*m^2 + m) := by ring
  · use 2*m^2 + 3*m + 1
    calc
      n^2 + n = (2*m + 1)^2 + (2*m + 1) := by rw [hb]
      _ = 4*m^2 + 4*m + 1 + 2*m + 1 := by ring
      _ = 2*(2*m^2 + 3*m + 1) := by ring

[Yakov Pechersky]

I suggest factoring your sum first

[Yakov Pechersky]

Then proving a lemma about the product of an even and an odd.

[Yakov Pechersky]

Or, since you have this version of Nat.even_or_odd', using associativity of multiplication to factor out a 2 to get an "obvious" form

[Damiano Testa]

In case it is useful, this is a slightly less verbose version:

example {n : ℕ} : ∃ k: ℕ, n^2 + n = 2*k := by
  obtain ⟨k, rfl | rfl⟩ := n.even_or_odd'
  · use (2 * k + 1) * k
    ring
  · use (2 * k + 1) * (k + 1)
    ring