Lean中能否定义定理的假设？含整数平方约束证明示例

当然可以给Lean的定理定义假设，核心是把约束条件作为定理陈述的一部分，常见有两种写法：

1. 将假设作为定理参数传入 #

直接把约束条件以(假设名 : 命题)的形式放在定理的参数列表里，针对你的需求可以这样定义：

theorem sq_between (min max : ℤ) (h : min ≤ max) : ∀ x : ℤ, min ≤ x ∧ x ≤ max → min^2 ≤ x^2 ∧ x^2 ≤ max^2 := by
  intro x hx
  -- 拆分x的范围约束
  have x_ge_min : min ≤ x := hx.left
  have x_le_max : x ≤ max := hx.right
  -- 注意：原命题存在反例，比如min=-2、max=1、x=0时，min²=4 > x²=0，结论不成立
  -- 若补充假设min ≥ 0，可完成证明，示例逻辑：
  -- 添加假设(h_min_nonneg : min ≥ 0)到定理参数后，用整数乘法单调性推导：
  -- apply And.intro
  -- · exact mul_le_mul x_ge_min x_ge_min h_min_nonneg (le_trans h_min_nonneg x_ge_min)
  -- · exact mul_le_mul x_le_max x_le_max (le_trans h_min_nonneg x_ge_min) (le_trans h_min_nonneg x_le_max)

2. 用蕴含式→表示假设 #

把约束条件放在蕴含式箭头左侧，形成“若P则Q”的结构，等价写法如下：

theorem sq_between' : ∀ min max : ℤ, min ≤ max → ∀ x : ℤ, min ≤ x ∧ x ≤ max → min^2 ≤ x^2 ∧ x^2 ≤ max^2 := by
  intro min max h x hx
  -- 后续证明逻辑和第一种写法完全一致

命题正确性补充 #

你提出的原命题存在逻辑漏洞：当min为负数时，容易找到反例（比如min=-3、max=2、x=0），此时min²=9远大于x²=0，不满足min² ≤ x²。若想让命题成立，可补充额外约束（比如min ≥ 0，此时x ≥ min ≥ 0，正数平方的单调性成立），或调整结论为x² ≤ max(min², max²) ∧ x² ≥ min(min², max²)。

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