How to prove that x

Question

I'm working my way through tutorials and also formalizing mathematics course and trying to solve other problems I find interesting. There is surprisingly little examples with inequalities.

How one can prove that if two ℤ numbers are both even or both odd, the closest they can be if not equal is 2 apart?

import data.int.basic
import data.int.parity

theorem even_even_at_least_two_apart { x y : ℤ } : even x ∧ even y → x < y → x ≤ y - 2 :=
begin
  sorry
end

I'm having trouble converting from mod to minimal differences. Or I'm stuck with x ≤ y - 1 that can be obtained from lt. I suspect my initial formalization can be off.

This is as far as i can get:

  rintros ⟨ hx, hy ⟩ hlt,
  rw int.even_iff at hx hy,
  rw ← int.le_sub_one_iff at hlt,

user_7605614 · Answer

Using library_search and linarith can save you a lot of trouble. The lines ending with the comment -- library_search where found using library_search.

import data.int.parity
import tactic.linarith

theorem even_even_at_least_two_apart { x y : ℤ } : even x ∧ even y → x < y → x ≤ y - 2 :=
begin
  rintros ⟨hx, hy⟩ hxy,
  have h₁ : even (y - x),
  exact int.even.sub_even hy hx,  -- library_search,
  have h₂ : 0 < y - x,
  exact sub_pos.mpr hxy, -- library_search
  rcases h₁ with ⟨k, hk⟩,
  rw hk at *,
  have : 1 ≤ k, by linarith,
  linarith
end

Note that the statement would be nicer to read and use as

theorem even_even_at_least_two_apart {x y : ℤ} (hx : even x) (hy : even y) (hxy : x < y) :
  x ≤ y - 2

user_17207970 · Answer

Rather than using the modulo operator, it seems to be much easier to use the definition of even directly, which is (when specialized to integers)

def even (a : ℤ) : Prop := ∃ (k : ℤ), a = 2*k

We can use this to take an even number and write it as 2*k for some k.

By the way, since the first step of your proof is to use intros, you may as well put those hypotheses before the colon:

theorem even_even_at_least_two_apart {x y : ℤ}
  (hx : even x) (hy : even y) (hlt : x < y) : x ≤ y - 2 := sorry

Here's a possible proof:

import data.int.basic
import data.int.parity

theorem even_even_at_least_two_apart {x y : ℤ}
  (hx : even x) (hy : even y) (hlt : x < y) : x ≤ y - 2 :=
begin
  -- use the definition of `even` to get that each integer is
  -- 2 times some number
  cases hx with kx hkx,
  cases hy with ky hky,
  -- since hkx and khy are `x = 2*kx` and `y = 2*ky`, we can
  -- substitute these in everywhere
  subst x,
  subst y,
  -- now we put the goal into the proper form to apply `mul_sub`
  change _ ≤ 2 * ky - 2 * 1,
  rw ←mul_sub,
  -- for some remaining inequalities, we need that `0` (as an integer)
  -- is less than `2` (as an integer; I'm using Lean's coercion rules,
  -- which lets me not write the coercion for both)
  have : (0 : ℤ) < 2 := by simp,
  rw mul_le_mul_left this,
  rw mul_lt_mul_left this at hlt,
  -- at this point, we have `hlt : kx < ky` and the goal `kx ≤ ky - 1`
  rw int.le_sub_one_iff,
  exact hlt,
end

Edit: like Patrick Massot, I used library_search to discover some of these lemmas, like int.le_sub_one_iff.

How to prove that x < y → x ≤ y - 2 if both are odd or both are even in Lean?

2 Answers