feat: allow naming the hypothesis generated by have? (#9454)

Previously, there was no way to specify the name for a hypothesis generated by `have?` (and if it suggested a let, it used an inaccessible `this`).

(Also, fixes a problem with `observe?`, that the suggestion was not respecting the requested name.)





Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib/Tactic/Observe.lean

@@ -41,8 +41,7 @@ elab_rules : tactic |
     else
       let v := (← instantiateMVars (mkMVar goal)).headBeta
       if trace.isSome then
-        -- TODO: we should be allowed to pass an identifier to `addHaveSuggestion`.
-        addHaveSuggestion tk type v
+        addHaveSuggestion tk (some name) type v
       let (_, newGoal) ← (← getMainGoal).note name v
       replaceMainGoal [newGoal]
 

Mathlib/Tactic/Propose.lean

@@ -113,11 +113,11 @@ only the types of the lemmas in the `using` clause.
 
 Suggestions are printed as `have := f a b c`.
 -/
-syntax (name := propose') "have?" "!"? (" : " term)? " using " (colGt term),+ : tactic
+syntax (name := propose') "have?" "!"? (ident)? (" : " term)? " using " (colGt term),+ : tactic
 
 open Elab.Tactic Elab Tactic in
 elab_rules : tactic
-  | `(tactic| have?%$tk $[!%$lucky]? $[ : $type:term]? using $[$terms:term],*) => do
+  | `(tactic| have?%$tk $[!%$lucky]? $[$h:ident]? $[ : $type:term]? using $[$terms:term],*) => do
     let stx ← getRef
     let goal ← getMainGoal
     goal.withContext do
@@ -130,7 +130,7 @@ elab_rules : tactic
         throwError "propose could not find any lemmas using the given hypotheses"
       -- TODO we should have `proposals` return a lazy list, to avoid unnecessary computation here.
       for p in proposals.toList.take 10 do
-        addHaveSuggestion tk (← inferType p.2) p.2 stx
+        addHaveSuggestion tk (h.map (·.getId)) (← inferType p.2) p.2 stx
       if lucky.isSome then
         let mut g := goal
         for p in proposals.toList.take 10 do

Mathlib/Tactic/TryThis.lean

@@ -15,21 +15,25 @@ This file could be upstreamed to `Std`.
 open Lean Elab Elab.Tactic PrettyPrinter Meta Std.Tactic.TryThis
 
 /-- Add a suggestion for `have : t := e`. -/
-def addHaveSuggestion (ref : Syntax) (t? : Option Expr) (e : Expr)
+def addHaveSuggestion (ref : Syntax) (h? : Option Name) (t? : Option Expr) (e : Expr)
     (origSpan? : Option Syntax := none) : TermElabM Unit := do
   let estx ← delabToRefinableSyntax e
   let prop ← isProp (← inferType e)
   let tac ← if let some t := t? then
     let tstx ← delabToRefinableSyntax t
     if prop then
-      `(tactic| have : $tstx := $estx)
+      match h? with
+      | some h => `(tactic| have $(mkIdent h) : $tstx := $estx)
+      | none => `(tactic| have : $tstx := $estx)
     else
-      `(tactic| let this : $tstx := $estx)
+      `(tactic| let $(mkIdent (h?.getD `_)) : $tstx := $estx)
   else
     if prop then
-      `(tactic| have := $estx)
+      match h? with
+      | some h => `(tactic| have $(mkIdent h) := $estx)
+      | none => `(tactic| have := $estx)
     else
-      `(tactic| let this := $estx)
+      `(tactic| let $(mkIdent (h?.getD `_)) := $estx)
   addSuggestion ref tac origSpan?
 
 open Lean.Parser.Tactic

test/LibrarySearch/observe.lean

@@ -1,6 +1,9 @@
 import Mathlib.Tactic.Observe
+import Std.Tactic.GuardMsgs
 
+/-- info: Try this: have h : x + y = y + x := Nat.add_comm x y -/
+#guard_msgs in
 example (x y : Nat) : True := by
-  observe h : x + y = y + x
+  observe? h : x + y = y + x
   guard_hyp h : x + y = y + x
   trivial

test/propose.lean

@@ -41,16 +41,15 @@ example (K L M : List α) (w : L.Disjoint M) (m : K ⊆ L) : True := by
 
 def bar (n : Nat) (x : String) : Nat × String := (n + x.length, x)
 
--- FIXME notice a bug here: should not generate `let this✝` with an inaccessible name.
 /--
-info: Try this: let this✝ : ℕ × String := bar p.1 p.2
+info: Try this: let a : ℕ × String := bar p.1 p.2
 ---
-info: Try this: let this✝ : ℕ × String := bar p.1 p.2
+info: Try this: let _ : ℕ × String := bar p.1 p.2
 -/
 #guard_msgs in
 example (p : Nat × String) : True := by
   fail_if_success have? using p
-  have? : Nat × String using p.1, p.2
+  have? a : Nat × String using p.1, p.2
   have? : Nat × _ using p.1, p.2
   trivial