Lean中是否存在中缀符号可简化不等式传递证明的书写？

你可以在Lean中通过自定义中缀符号，把嵌套的不等式传递证明改成链式调用的形式。具体实现方式如下：

自定义中缀符号示例 #

Lean支持通过infix命令为定理绑定中缀运算符，你可以为lt_of_le_of_lt、lt_of_lt_of_le、lt_trans分别定义合适的中缀符号，代码示例：

-- 为 lt_of_le_of_lt 定义中缀符号（可自选未被占用的符号，这里用⊢₁）
infix:50 " ⊢₁ " => lt_of_le_of_lt
-- 为 lt_of_lt_of_le 定义中缀符号
infix:50 " ⊢₂ " => lt_of_lt_of_le
-- 为 lt_trans 定义中缀符号
infix:50 " ⊢₃ " => lt_trans

example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) :
  a < e := ((h₀ ⊢₁ h₁) ⊢₂ h₂) ⊢₃ h₃

补充说明 #

• 符号可以根据个人偏好选择，只要未被Lean系统占用即可；infix:n中的n是优先级数值，数值越小优先级越高，可按需调整
• Lean本身不支持直接用反引号包裹函数名作为中缀符号的一部分，所以用简洁符号替代是更简便的方案

更简洁的替代写法 #

Lean的mathlib库提供了更简洁的链式证明方式，无需自定义符号：

-- 使用trans tactic
example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) :
  a < e := by trans <;> assumption

-- 使用自带的链式方法
example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) :
  a < e := h₀.trans_lt h₁.trans_le h₂.trans_lt h₃

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