Using Odd/Even

Stream: new members

[JK]

I'm trying to solve Exercise 7 in Section 2.5.9 of Mechanics of Proof. I thought to prove this using notions of Even/Odd, though I'm not sure this is what was intended since Even/Odd is not introduced until the following section nor have proofs by contradiction been discussed.

Arguing toward a contradiction, I was able to prove that m=5 implies Even m and Odd m, but I am unsure where to go from there. I see there is a lemma Int.even_xor'_odd but I am not sure how to apply it.

import Mathlib
example {m : ℤ} (h : ∃ a, 2 * a = m) : m ≠ 5 := by
  obtain ⟨a, ha⟩ := h
  have odd5: Odd 5 := by
    use 2
    norm_num
  obtain m_eq_5 | m_ne_5 := eq_or_ne m 5
  have evenm : Even m := by
    use a
    calc
      m = 2*a := by rw [ha]
      _ = a+a := by ring
  have oddm : Odd m := by
    use 2
    calc
      m = 5 := m_eq_5
      _ = 2*2+1:= by ring

[JK]

OK, I have figured out how to use Int.even_xor'_odd but now I am mystified why the following proof doesn't succeed:

import Mathlib

example {m : ℤ} (h : ∃ a, 2 * a = m) : m ≠ 5 := by
  obtain ⟨a, ha⟩ := h
  have odd5: Odd 5 := by
    use 2
    norm_num
  obtain m_eq_5 | m_ne_5 := eq_or_ne m 5
  . have evenm : Even m := by
      use a
      calc
        m = 2*a := by rw [ha]
        _ = a+a := by ring
    have oddm : Odd m := by
      use 2
      calc
        m = 5 := m_eq_5
        _ = 2*2 + 1 := by ring
    have f : Xor' (Even m) (Odd m) := by apply Int.even_xor'_odd m
    dsimp [Xor'] at f
    obtain f1 | f2 := f
    obtain ⟨f21 , f12⟩  := f1
    contradiction
    obtain ⟨f21, f22⟩ := f2
    contradiction
  . exact m_ne_5

[Ruben Van de Velde]

It seems to succeed

[JK]

Argh, yes, you are right

[JK]

Since my solution seems more advanced than what is expected at this stage of the tutorial, I'd be interested to know if I am missing a much simpler solution.

[Dan Velleman]

Looking at Examples 2.3.2, my guess is that, after introducing a and ha, you should assert that a ≤ 2 ∨ 3 ≤ a. (See Example 2.3.2 for how to justify that.) Then break into cases based on that assertion and show m < 5 in the first case and m > 5 in the second.