如何在Lean中证明两个同奇偶整数满足x<y时x≤y-2？

证明逻辑 #

你的形式化定义不存在错误，核心推导思路如下：

1. 两个奇偶性一致的整数的差必为偶数
2. 由x < y可推得y - x是大于0的正整数
3. 大于0的偶数最小取值为2，因此y - x ≥ 2，移项后即可得到目标结论x ≤ y - 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
  rintros ⟨ hx, hy ⟩ hlt,
  rw int.even_iff at hx hy,
  rw ← int.le_sub_one_iff at hlt,
  -- 推导y - x为正整数
  have h_sub_pos : 0 < y - x := by linarith,
  -- 推导两个偶数的差为偶数
  have h_sub_even : even (y - x) := int.even_sub hy hx,
  rw int.even_iff at h_sub_even,
  -- 证明正偶数最小为2
  have h_sub_ge2 : y - x ≥ 2,
  { by_contra h,
    push_neg at h,
    have : y - x = 1 := by linarith,
    rw this at h_sub_even,
    norm_num at h_sub_even },
  -- 移项得到结论
  linarith,
end

扩展到所有同奇偶场景的通用证明 #

如果需要覆盖两个整数同为奇数的情况，只需要把定理条件修改为奇偶性等价即可：

theorem same_parity_at_least_two_apart {x y : ℤ} : (even x ↔ even y) → x < y → x ≤ y - 2 :=
begin
  rintros h_parity hlt,
  have h_sub_pos : 0 < y - x := by linarith,
  have h_sub_even : even (y - x),
  { rw int.even_sub_iff, exact h_parity },
  rw int.even_iff at h_sub_even,
  have h_sub_ge2 : y - x ≥ 2,
  { by_contra h,
    push_neg at h,
    have : y - x = 1 := by linarith,
    rw this at h_sub_even,
    norm_num at h_sub_even },
  linarith,
end

内容的提问来源于stack exchange，提问作者lonelyelk