chore: upstream Std.Util.ExtendedBinders (leanprover#3320)

This is not a complete upstreaming of that file (it also supports `∀ᵉ (x
< 2) (y < 3), p x y` as shorthand for `∀ x < 2, ∀ y < 3, p x y`, but I
don't think we need this; it is used in Mathlib).

Syntaxes still need to be made built-in.

---------

Co-authored-by: Leonardo de Moura <[email protected]>

src/Init.lean

@@ -30,3 +30,4 @@ import Init.Conv
 import Init.Guard
 import Init.Simproc
 import Init.SizeOfLemmas
+import Init.BinderPredicates

src/Init/BinderPredicates.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
+-/
+prelude
+import Init.NotationExtra
+
+namespace Lean
+
+/--
+The syntax category of binder predicates contains predicates like `> 0`, `∈ s`, etc.
+(`: t` should not be a binder predicate because it would clash with the built-in syntax for ∀/∃.)
+-/
+declare_syntax_cat binderPred
+
+/--
+`satisfies_binder_pred% t pred` expands to a proposition expressing that `t` satisfies `pred`.
+-/
+syntax "satisfies_binder_pred% " term:max binderPred : term
+
+-- Extend ∀ and ∃ to binder predicates.
+
+/--
+The notation `∃ x < 2, p x` is shorthand for `∃ x, x < 2 ∧ p x`,
+and similarly for other binary operators.
+-/
+syntax "∃ " binderIdent binderPred ", " term : term
+/--
+The notation `∀ x < 2, p x` is shorthand for `∀ x, x < 2 → p x`,
+and similarly for other binary operators.
+-/
+syntax "∀ " binderIdent binderPred ", " term : term
+
+macro_rules
+  | `(∃ $x:ident $pred:binderPred, $p) =>
+    `(∃ $x:ident, satisfies_binder_pred% $x $pred ∧ $p)
+  | `(∃ _ $pred:binderPred, $p) =>
+    `(∃ x, satisfies_binder_pred% x $pred ∧ $p)
+
+macro_rules
+  | `(∀ $x:ident $pred:binderPred, $p) =>
+    `(∀ $x:ident, satisfies_binder_pred% $x $pred → $p)
+  | `(∀ _ $pred:binderPred, $p) =>
+    `(∀ x, satisfies_binder_pred% x $pred → $p)
+
+/-- Declare `∃ x > y, ...` as syntax for `∃ x, x > y ∧ ...` -/
+binder_predicate x " > " y:term => `($x > $y)
+/-- Declare `∃ x ≥ y, ...` as syntax for `∃ x, x ≥ y ∧ ...` -/
+binder_predicate x " ≥ " y:term => `($x ≥ $y)
+/-- Declare `∃ x < y, ...` as syntax for `∃ x, x < y ∧ ...` -/
+binder_predicate x " < " y:term => `($x < $y)
+/-- Declare `∃ x ≤ y, ...` as syntax for `∃ x, x ≤ y ∧ ...` -/
+binder_predicate x " ≤ " y:term => `($x ≤ $y)
+/-- Declare `∃ x ≠ y, ...` as syntax for `∃ x, x ≠ y ∧ ...` -/
+binder_predicate x " ≠ " y:term => `($x ≠ $y)
+
+end Lean

src/Lean/Elab.lean

@@ -10,6 +10,7 @@ import Lean.Elab.Command
 import Lean.Elab.Term
 import Lean.Elab.App
 import Lean.Elab.Binders
+import Lean.Elab.BinderPredicates
 import Lean.Elab.LetRec
 import Lean.Elab.Frontend
 import Lean.Elab.BuiltinNotation

src/Lean/Elab/BinderPredicates.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
+-/
+import Lean.Parser.Syntax
+import Lean.Elab.MacroArgUtil
+import Lean.Linter.MissingDocs
+
+namespace Lean.Elab.Command
+
+@[builtin_command_elab binderPredicate] def elabBinderPred : CommandElab := fun stx => do
+  match stx with
+  | `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind binder_predicate%$tk
+      $[(name := $name?)]? $[(priority := $prio?)]? $x $args:macroArg* => $rhs) => do
+    let prio ← liftMacroM do evalOptPrio prio?
+    let (stxParts, patArgs) := (← args.mapM expandMacroArg).unzip
+    let name ← match name? with
+      | some name => pure name.getId
+      | none => liftMacroM do mkNameFromParserSyntax `binderTerm (mkNullNode stxParts)
+    let nameTk := name?.getD (mkIdentFrom tk name)
+    /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
+    So, we must include current namespace when we create a pattern for the following
+    `macro_rules` commands. -/
+    let pat : TSyntax `binderPred := ⟨(mkNode ((← getCurrNamespace) ++ name) patArgs).1⟩
+    elabCommand <|<-
+    `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind syntax%$tk
+        (name := $nameTk) (priority := $(quote prio)) $[$stxParts]* : binderPred
+      $[$doc?:docComment]? macro_rules%$tk
+        | `(satisfies_binder_pred% $$($x):term $pat:binderPred) => $rhs)
+  | _ => throwUnsupportedSyntax
+
+open Linter.MissingDocs Parser Term in
+/-- Missing docs handler for `binder_predicate` -/
+@[builtin_missing_docs_handler Lean.Parser.Command.binderPredicate]
+def checkBinderPredicate : SimpleHandler := fun stx => do
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
+    if stx[4].isNone then lint stx[3] "binder predicate"
+    else lintNamed stx[4][0][3] "binder predicate"
+
+end Lean.Elab.Command

src/Lean/Parser/Syntax.lean

@@ -104,6 +104,16 @@ def elabTail := leading_parser atomic (" : " >> ident >> optional (" <= " >> ide
   optional docComment >> optional Term.«attributes» >> Term.attrKind >>
   "elab" >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (ppSpace >> elabArg) >> elabTail
 
+/--
+Declares a binder predicate.  For example:
+```
+binder_predicate x " > " y:term => `($x > $y)
+```
+-/
+@[builtin_command_parser] def binderPredicate := leading_parser
+   optional docComment >>  optional Term.attributes >> optional Term.attrKind >>
+   "binder_predicate" >> optNamedName >> optNamedPrio >> ppSpace >> ident >> many (ppSpace >> macroArg) >> " => " >> termParser
+
 end Command
 
 end Parser