infix notation in Lean

userT111 0
Viewed 33

Is there an infix notation that would allow to rewrite those proofs

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₃
 }

more naturally as

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₃
lean
1 Answers

You can use Lean's dot notation to make an infix version of the argument, for example

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

What's going on here is that the type of h₀ is le a b (in the has_le namespace), so h₀.trans_lt means le.trans_lt h₀, and you can see in order.basic in mathlib that le.trans_lt is just an abbreviation for lt_of_le_of_lt.

Kevin Buzzard0
Related