feat: allow anonymous equality proofs in match expressions (#6853)

This PR adds support for anonymous equality proofs in `match`
expressions of the form `match _ : e with ...`.

Closes #6759.

src/Lean/Elab/Match.lean

@@ -30,7 +30,7 @@ private def mkUserNameFor (e : Expr) : TermElabM Name := do
 
 
 /--
-   Remark: if the discriminat is `Syntax.missing`, we abort the elaboration of the `match`-expression.
+   Remark: if the discriminant is `Syntax.missing`, we abort the elaboration of the `match`-expression.
    This can happen due to error recovery. Example
    ```
    example : (p ∨ p) → p := fun h => match
@@ -56,6 +56,11 @@ private def elabAtomicDiscr (discr : Syntax) : TermElabM Expr := do
   let term := discr[1]
   elabTerm term none
 
+/-- Creates syntax for a fresh `h : `-notation annotation for a discriminant, copying source
+    information from an existing annotation `stx`. -/
+private def mkFreshDiscrIdentFrom (stx : Syntax) : CoreM Ident :=
+  return mkIdentFrom stx (← mkFreshUserName `h)
+
 structure Discr where
   expr : Expr
   /-- `some h` if discriminant is annotated with the `h : ` notation. -/
@@ -78,11 +83,11 @@ private partial def elabMatchTypeAndDiscrs (discrStxs : Array Syntax) (matchOptM
     -- motive := leading_parser atomic ("(" >> nonReservedSymbol "motive" >> " := ") >> termParser >> ")"
     let matchTypeStx := matchOptMotive[0][3]
     let matchType ← elabType matchTypeStx
-    let (discrs, isDep) ← elabDiscrsWitMatchType matchType
+    let (discrs, isDep) ← elabDiscrsWithMatchType matchType
     return { discrs := discrs, matchType := matchType, isDep := isDep, alts := matchAltViews }
 where
   /-- Easy case: elaborate discriminant when the match-type has been explicitly provided by the user.  -/
-  elabDiscrsWitMatchType (matchType : Expr) : TermElabM (Array Discr × Bool) := do
+  elabDiscrsWithMatchType (matchType : Expr) : TermElabM (Array Discr × Bool) := do
     let mut discrs := #[]
     let mut i := 0
     let mut matchType := matchType
@@ -105,6 +110,10 @@ where
   markIsDep (r : ElabMatchTypeAndDiscrsResult) :=
     { r with isDep := true }
 
+  expandDiscrIdent : Syntax → MetaM Syntax
+    | stx@`(_) => mkFreshDiscrIdentFrom stx
+    | stx => return stx
+
   /-- Elaborate discriminants inferring the match-type -/
   elabDiscrs (i : Nat) (discrs : Array Discr) : TermElabM ElabMatchTypeAndDiscrsResult := do
     if h : i < discrStxs.size then
@@ -112,7 +121,12 @@ where
       let discr     ← elabAtomicDiscr discrStx
       let discr     ← instantiateMVars discr
       let userName ← mkUserNameFor discr
-      let h? := if discrStx[0].isNone then none else some discrStx[0][0]
+      let h? ←
+        if discrStx[0].isNone then
+          pure none
+        else
+          let h ← expandDiscrIdent discrStx[0][0]
+          pure (some h)
       let discrs := discrs.push { expr := discr, h? }
       let mut result ← elabDiscrs (i + 1) discrs
       let matchTypeBody ← kabstract result.matchType discr
@@ -916,7 +930,7 @@ where
         | none => return { expr := i : Discr }
         | some h =>
           -- If the discriminant that introduced this index is annotated with `h : discr`, then we should annotate the new discriminant too.
-          let h := mkIdentFrom h (← mkFreshUserName `h)
+          let h ← mkFreshDiscrIdentFrom h
           return { expr := i, h? := h : Discr }
       let discrs    := indDiscrs ++ discrs
       let indexFVarIds := indices.filterMap fun | .fvar fvarId .. => some fvarId | _  => none
@@ -1194,7 +1208,7 @@ Remark the `optIdent` must be `none` at `matchDiscr`. They are expanded by `expa
 -/
 private def elabMatchCore (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
   let expectedType   ← waitExpectedTypeAndDiscrs stx expectedType?
-  let discrStxs      := (getDiscrs stx).map fun d => d
+  let discrStxs      := getDiscrs stx
   let gen?           := getMatchGeneralizing? stx
   let altViews       := getMatchAlts stx
   let matchOptMotive := getMatchOptMotive stx

src/Lean/Parser/Term.lean

@@ -418,7 +418,7 @@ def matchAlts (rhsParser : Parser := termParser) : Parser :=
 /-- `matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as
 `match h1 : e1, e2, h3 : e3 with ...`. -/
 @[builtin_doc] def matchDiscr := leading_parser
-  optional (atomic (ident >> " : ")) >> termParser
+  optional (atomic (binderIdent >> " : ")) >> termParser
 
 def trueVal  := leading_parser nonReservedSymbol "true"
 def falseVal := leading_parser nonReservedSymbol "false"

tests/lean/run/6759.lean

@@ -0,0 +1,49 @@
+/-!
+# Match expressions with unnamed equality proofs
+
+https://github.com/leanprover/lean4/issues/6759
+
+Tests that `match` expressions successfully elaborate when providing a hole instead of an identifier
+to which to bind the optional equality proof.
+-/
+
+def getLast? {α : Type} (a : Array α) : Option α :=
+  match _ : a.size with
+  | 0 => none
+  | m + 1 => some a[m]
+
+/-- info: some 4 -/
+#guard_msgs in
+#eval getLast? #[3, 4]
+
+
+def getLasts? {α : Type} (a b : Array α) : Option (α × α) :=
+  match _ : a.size, _ : b.size with
+  | 0, _ => none
+  | _, 0 => none
+  | m + 1, n + 1 => some (a[m], b[n])
+
+/-- info: some (4, 5) -/
+#guard_msgs in
+#eval getLasts? #[3, 4] #[5]
+
+
+def getLasts?' (a b : Array α) : Option (α × α) :=
+  match _ : a.size, h : b.size with
+  | 0, _ => none
+  | _, 0 => none
+  | m + 1, n + 1 => some (a[m], b[n]'(h ▸ Nat.lt.base n))
+
+/-- info: some (4, 5) -/
+#guard_msgs in
+#eval getLasts?' #[3, 4] #[5]
+
+
+theorem test_tactic (n : Nat) (h : n - 1 > 2) : n - 1 > 2 := by
+  match _ : n - 1 with
+  | 0 =>
+    have : n - 1 = 0 := by assumption
+    rwa [this] at h
+  | n' + 1 =>
+    have : n - 1 = n' + 1 := by assumption
+    rwa [← this]