From 98085661c770fbbcffa73342ff722591db11ddd5 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 15 Feb 2024 12:36:01 +1100
Subject: [PATCH] chore: upstream haveI tactic

chore: `haveI` and `letI` builtin parsers
---
 src/Lean/Elab/Tactic.lean       |  1 +
 src/Lean/Elab/Tactic/HaveI.lean | 59 +++++++++++++++++++++++++++++++++
 src/Lean/Parser/Term.lean       |  6 ++++
 3 files changed, 66 insertions(+)
 create mode 100644 src/Lean/Elab/Tactic/HaveI.lean

diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean
index b0dc3647c3..86a7d6b0a4 100644
--- a/src/Lean/Elab/Tactic.lean
+++ b/src/Lean/Elab/Tactic.lean
@@ -27,3 +27,4 @@ import Lean.Elab.Tactic.Guard
 import Lean.Elab.Tactic.RCases
 import Lean.Elab.Tactic.Repeat
 import Lean.Elab.Tactic.Change
+import Lean.Elab.Tactic.HaveI
diff --git a/src/Lean/Elab/Tactic/HaveI.lean b/src/Lean/Elab/Tactic/HaveI.lean
new file mode 100644
index 0000000000..01fb27c869
--- /dev/null
+++ b/src/Lean/Elab/Tactic/HaveI.lean
@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
+-/
+import Lean.Elab.ElabRules
+open Lean Elab Parser Term Meta Macro
+
+/-!
+Defines variants of `have` and `let` syntax which do not produce `let_fun` or `let` bindings,
+but instead inline the value instead.
+
+This is useful to declare local instances and proofs in theorem statements
+and subgoals, where the extra binding is inconvenient.
+-/
+
+#exit
+
+namespace Std.Tactic
+
+
+macro_rules
+  | `(haveI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) =>
+    `(haveI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body)
+  | `(haveI _ $bs* := $val; $body) => `(haveI x $bs* : _ := $val; $body)
+  | `(haveI _ $bs* : $ty := $val; $body) => `(haveI x $bs* : $ty := $val; $body)
+  | `(haveI $x:ident $bs* := $val; $body) => `(haveI $x $bs* : _ := $val; $body)
+  | `(haveI $_:ident $_* : $_ := $_; $_) => throwUnsupported -- handled by elab
+
+macro_rules
+  | `(letI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) =>
+    `(letI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body)
+  | `(letI _ $bs* := $val; $body) => `(letI x $bs* : _ := $val; $body)
+  | `(letI _ $bs* : $ty := $val; $body) => `(letI x $bs* : $ty := $val; $body)
+  | `(letI $x:ident $bs* := $val; $body) => `(letI $x $bs* : _ := $val; $body)
+  | `(letI $_:ident $_* : $_ := $_; $_) => throwUnsupported -- handled by elab
+
+elab_rules <= expectedType
+  | `(haveI $x:ident $bs* : $ty := $val; $body) => do
+    let (ty, val) ← elabBinders bs fun bs => do
+      let ty ← elabType ty
+      let val ← elabTermEnsuringType val ty
+      pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val)
+    withLocalDeclD x.getId ty fun x => do
+      return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val]
+
+elab_rules <= expectedType
+  | `(letI $x:ident $bs* : $ty := $val; $body) => do
+    let (ty, val) ← elabBinders bs fun bs => do
+      let ty ← elabType ty
+      let val ← elabTermEnsuringType val ty
+      pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val)
+    withLetDecl x.getId ty val fun x => do
+      return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val]
+
+/-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/
+macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_)
+/-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
+macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_)
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index b4de1bbd3a..16701816b4 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -569,6 +569,12 @@ def haveDecl     := leading_parser (withAnonymousAntiquot := false)
   haveIdDecl <|> (ppSpace >> letPatDecl) <|> haveEqnsDecl
 @[builtin_term_parser] def «have» := leading_parser:leadPrec
   withPosition ("have" >> haveDecl) >> optSemicolon termParser
+/-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/
+@[builtin_term_parser] def «haveI» := leading_parser
+  withPosition ("haveI " >> haveDecl) >> optSemicolon termParser
+/-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
+@[builtin_term_parser] def «letI» := leading_parser
+  withPosition ("letI " >> haveDecl) >> optSemicolon termParser
 
 def «scoped» := leading_parser "scoped "
 def «local»  := leading_parser "local "