From eba3983658faef2d41b7ad00fc2c2e540a1e43e6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 29 Dec 2020 16:49:25 -0800
Subject: [PATCH] feat: use `binrel!` gadget to define `>`, `<`, ... notations

It has better support for applying coercions.
---
 src/Init/Notation.lean                  | 14 ++++
 tests/lean/macroStack.lean.expected.out |  2 +-
 tests/lean/run/binrelmacros.lean        | 98 +++++++++++++++++++++++++
 3 files changed, 113 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/binrelmacros.lean

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 8f23f8f0dc..9c1e4ffc25 100644
--- a/src/Init/Notation.lean
+++ b/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
diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out
index 34f89f406b..48c1949577 100644
--- a/tests/lean/macroStack.lean.expected.out
+++ b/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
diff --git a/tests/lean/run/binrelmacros.lean b/tests/lean/run/binrelmacros.lean
new file mode 100644
index 0000000000..82799401a6
--- /dev/null
+++ b/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