精益注记法

Question

是否有可以重写这些证明的内插即用符号？

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

example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) :
  a < e := by
  { apply lt_trans,
    {apply lt_of_lt_of_le, 
      {apply lt_of_le_of_lt, apply h₀, apply h₁}
     , apply h₂},
    apply h₃
 }

更自然地

example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) :
  a < e := ((h₀ `lt_of_le_of_lt` h₁) `lt_of_lt_of_le` h₂) `lt_trans` h₃

Answer 1

例如，您可以使用精益的点表示法来制作参数的infix版本。

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

这里要做的是，h₀的类型是le a b (在has_le命名空间中)，所以h₀.trans_lt的意思是le.trans_lt h₀，在mathlib中的order.basic中可以看到le.trans_lt只是lt_of_le_of_lt的缩写。