feat: use binrel! gadget to define >, <, ... notations

It has better support for applying coercions.

src/Init/Notation.lean

@@ -80,6 +80,20 @@ infix:50 " = "  => Eq
 infix:50 " == " => BEq.beq
 infix:50 " ~= " => HEq
 infix:50 " ≅ "  => HEq
+/-
+  Remark: the infix commands above ensure a delaborator is generated for each relations.
+  We redefine the macros below to be able to use the auxiliary `binrel!` elaboration helper for binary relations.
+  It has better support for applying coercions. For example, suppose we have `binrel! Eq n i` where `n : Nat` and
+  `i : Int`. The default elaborator fails because we don't have a coercion from `Int` to `Nat`, but
+  `binrel!` succeeds because it also tries a coercion from `Nat` to `Int` even when the nat occurs before the int. -/
+macro_rules | `($x <= $y) => `(binrel! HasLessEq.LessEq $x $y)
+macro_rules | `($x ≤ $y)  => `(binrel! HasLessEq.LessEq $x $y)
+macro_rules | `($x < $y)  => `(binrel! HasLess.Less $x $y)
+macro_rules | `($x > $y)  => `(binrel! Greater $x $y)
+macro_rules | `($x >= $y) => `(binrel! GreaterEq $x $y)
+macro_rules | `($x ≥ $y)  => `(binrel! GreaterEq $x $y)
+macro_rules | `($x = $y)  => `(binrel! Eq $x $y)
+macro_rules | `($x == $y) => `(binrel! BEq.beq $x $y)
 
 infixr:35 " /\\ " => And
 infixr:35 " ∧ "   => And

tests/lean/macroStack.lean.expected.out

@@ -1,7 +1,7 @@
 macroStack.lean:4:5: error: unknown identifier 'x'
 macroStack.lean:8:6: error: unknown identifier 'x'
 with resulting expansion
-  Greater✝ x 0
+  binrel! Greater✝x 0
 while expanding
   x > 0
 while expanding

tests/lean/run/binrelmacros.lean

@@ -0,0 +1,98 @@
+theorem ex1 : ∀ x : Int, ∃ n : Nat, n > x :=
+  sorry
+
+theorem ex2 : ∀ x : Int, ∃ n : Nat, x > n :=
+  sorry
+
+namespace Lt
+
+def ex1 (x y : Nat) (i j : Int) :=
+  x < i
+
+def ex2 (x y : Nat) (i j : Int) :=
+  i < x
+
+def ex3 (x y : Nat) (i j : Int) :=
+  i + 1 < x
+
+def ex4 (x y : Nat) (i j : Int) :=
+  i < x + 1
+
+def ex5 (x y : Nat) (i j : Int) :=
+  i < x + y
+
+def ex6 (x y : Nat) (i j : Int) :=
+  i + j < x + 0
+
+def ex7 (x y : Nat) (i j : Int) :=
+  i + j < x + i
+
+def ex8 (x y : Nat) (i j : Int) :=
+  i + 0 < x + i
+
+def ex9 (n : UInt32) :=
+  n < 0xd800
+
+end Lt
+
+namespace Eq
+
+def ex1 (x y : Nat) (i j : Int) :=
+  x = i
+
+def ex2 (x y : Nat) (i j : Int) :=
+  i = x
+
+def ex3 (x y : Nat) (i j : Int) :=
+  i + 1 = x
+
+def ex4 (x y : Nat) (i j : Int) :=
+  i = x + 1
+
+def ex5 (x y : Nat) (i j : Int) :=
+  i = x + y
+
+def ex6 (x y : Nat) (i j : Int) :=
+  i + j = x + 0
+
+def ex7 (x y : Nat) (i j : Int) :=
+  i + j = x + i
+
+def ex8 (x y : Nat) (i j : Int) :=
+  i + 0 = x + i
+
+def ex9 (n : UInt32) :=
+  n = 0xd800
+
+end Eq
+
+namespace BEq
+
+def ex1 (x y : Nat) (i j : Int) :=
+  x == i
+
+def ex2 (x y : Nat) (i j : Int) :=
+  i == x
+
+def ex3 (x y : Nat) (i j : Int) :=
+  i + 1 == x
+
+def ex4 (x y : Nat) (i j : Int) :=
+  i == x + 1
+
+def ex5 (x y : Nat) (i j : Int) :=
+  i == x + y
+
+def ex6 (x y : Nat) (i j : Int) :=
+  i + j == x + 0
+
+def ex7 (x y : Nat) (i j : Int) :=
+  i + j == x + i
+
+def ex8 (x y : Nat) (i j : Int) :=
+  i + 0 == x + i
+
+def ex9 (n : UInt32) :=
+  n == 0xd800
+
+end BEq