chore: builtin haveI and letI

src/Init/NotationExtra.lean

@@ -391,6 +391,23 @@ macro_rules
     `($mods:declModifiers class $id $params* extends $parents,* $[: $ty]?
       attribute [instance] $ctor)
 
+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 $_* : $_ := $_; $_) => Lean.Macro.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 $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab
+
+
 syntax cdotTk := patternIgnore("· " <|> ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic

src/Init/Tactics.lean

@@ -944,6 +944,12 @@ macro_rules | `(tactic| and_intros) => `(tactic| repeat' refine And.intro ?_ ?_)
 /-- The `run_tac doSeq` tactic executes code in `TacticM Unit`. -/
 syntax (name := runTac) "run_tac " doSeq : tactic
 
+/-- `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; ?_)
+
 end Tactic
 
 namespace Attr

src/Lean/Elab/BuiltinNotation.lean

@@ -10,6 +10,7 @@ import Lean.Meta.MatchUtil
 import Lean.Compiler.ImplementedByAttr
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.Eval
+import Lean.Elab.Binders
 
 namespace Lean.Elab.Term
 open Meta
@@ -467,4 +468,28 @@ def elabUnsafe : TermElab := fun stx expectedType? =>
       (← `(do $cmds)))
   | _ => throwUnsupportedSyntax
 
+@[builtin_term_elab Lean.Parser.Term.haveI] def elabHaveI : TermElab := fun stx expectedType? => do
+  match stx with
+  | `(haveI $x:ident $bs* : $ty := $val; $body) =>
+    withExpectedType expectedType? fun expectedType => 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]
+  | _ => throwUnsupportedSyntax
+
+@[builtin_term_elab Lean.Parser.Term.letI] def elabLetI : TermElab := fun stx expectedType? => do
+  match stx with
+  | `(letI $x:ident $bs* : $ty := $val; $body) =>
+    withExpectedType expectedType? fun expectedType => 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]
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Term

src/Lean/Elab/ElabRules.lean

@@ -11,12 +11,6 @@ open Lean.Syntax
 open Lean.Parser.Term hiding macroArg
 open Lean.Parser.Command
 
-def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr := do
-  Term.tryPostponeIfNoneOrMVar expectedType?
-  let some expectedType ← pure expectedType?
-    | throwError "expected type must be known"
-  x expectedType
-
 def elabElabRulesAux (doc? : Option (TSyntax ``docComment))
     (attrs? : Option (TSepArray ``attrInstance ",")) (attrKind : TSyntax ``attrKind)
     (k : SyntaxNodeKind) (cat? expty? : Option (Ident)) (alts : Array (TSyntax ``matchAlt)) :
@@ -54,7 +48,7 @@ def elabElabRulesAux (doc? : Option (TSyntax ``docComment))
     if catName == `term then
       `($[$doc?:docComment]? @[$(← mkAttrs `term_elab),*]
         aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab :=
-        fun stx expectedType? => Lean.Elab.Command.withExpectedType expectedType? fun $expId => match stx with
+        fun stx expectedType? => Lean.Elab.Term.withExpectedType expectedType? fun $expId => match stx with
           $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax)
     else
       throwErrorAt expId "syntax category '{catName}' does not support expected type specification"

src/Lean/Elab/Tactic.lean

@@ -27,4 +27,3 @@ 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

src/Lean/Elab/Tactic/HaveI.lean

@@ -1,59 +0,0 @@
-/-
-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; ?_)

src/Lean/Elab/Term.lean

@@ -865,6 +865,12 @@ def tryPostponeIfHasMVars (expectedType? : Option Expr) (msg : String) : TermEla
     throwError "{msg}, expected type contains metavariables{indentD expectedType?}"
   return expectedType
 
+def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr := do
+  tryPostponeIfNoneOrMVar expectedType?
+  let some expectedType ← pure expectedType?
+    | throwError "expected type must be known"
+  x expectedType
+
 /--
   Save relevant context for term elaboration postponement.
 -/

tests/lean/1021.lean.expected.out

@@ -1,8 +1,8 @@
-some { range := { pos := { line := 192, column := 42 },
+some { range := { pos := { line := 193, column := 42 },
              charUtf16 := 42,
-             endPos := { line := 198, column := 31 },
+             endPos := { line := 199, column := 31 },
              endCharUtf16 := 31 },
-  selectionRange := { pos := { line := 192, column := 46 },
+  selectionRange := { pos := { line := 193, column := 46 },
                       charUtf16 := 46,
-                      endPos := { line := 192, column := 58 },
+                      endPos := { line := 193, column := 58 },
                       endCharUtf16 := 58 } }

tests/lean/run/haveI.lean

@@ -0,0 +1,4 @@
+example (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
+    haveI : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
+    (a.push x)[i] = a[i] := by
+  sorry