如何在精益中证明 x < y → x ≤ y - 2 如果两者都是奇数或偶数？

Question

我正在努力完成教程，并将数学课程形式化，并尝试解决我觉得有趣的其他问题。令人惊讶的是，不等式的例子很少。

如何证明如果两个 ℤ 数均为偶数或均为奇数，如果不相等，最接近的数相差 2？

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

我在从 mod 转换为最小差异时遇到问题。或者我坚持使用可以从 lt 获得的 x ≤ y - 1。我怀疑我的初始形式可能会关闭。

这是我所能得到的：

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

Answer 1

使用library_search和linarith可以省去很多麻烦。使用 library_search.

找到的以注释 -- 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

请注意，该语句更易于阅读和使用

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

Answer 2

与其使用模运算符，不如直接使用 even 的定义更容易，即（当专门用于整数时）

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

我们可以用它来取一个偶数并将其写成 2*k 对于某些 k。

顺便说一句，既然你证明的第一步是使用intros，你不妨把这些假设放在冒号之前：

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

这是一个可能的证明：

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

编辑：像 Patrick Massot 一样，我使用 library_search 发现了其中一些引理，例如 int.le_sub_one_iff。

如何在精益中证明 x < y → x ≤ y - 2 如果两者都是奇数或偶数？

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

formal-verification

lean