[Merged by Bors] - feat: add an eval% elaborator for interpolating the output of #eval

Mathlib.lean

@@ -3442,6 +3442,7 @@ import Mathlib.Tactic.DeriveFintype
 import Mathlib.Tactic.DeriveToExpr
 import Mathlib.Tactic.DeriveTraversable
 import Mathlib.Tactic.Eqns
+import Mathlib.Tactic.Eval
 import Mathlib.Tactic.Existsi
 import Mathlib.Tactic.Explode
 import Mathlib.Tactic.Explode.Datatypes

Mathlib/Tactic.lean

@@ -39,6 +39,7 @@ import Mathlib.Tactic.DeriveFintype
 import Mathlib.Tactic.DeriveToExpr
 import Mathlib.Tactic.DeriveTraversable
 import Mathlib.Tactic.Eqns
+import Mathlib.Tactic.Eval
 import Mathlib.Tactic.Existsi
 import Mathlib.Tactic.Explode
 import Mathlib.Tactic.Explode.Datatypes

Mathlib/Tactic/Eval.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2024 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+
+import Qq.Macro
+import Std.Lean.Expr
+
+/-!
+# The `eval%` term elaborator
+
+This file provides the `eval% x` term elaborator, which evaluates the constant `x` at compile-time
+in the interpreter, and interpolates it into the expression.
+-/
+
+
+open Qq Lean Elab Term
+
+namespace Mathlib.Meta
+
+/--
+`eval% x` evaluates the term `x : X` in the interpreter, and then injects the resulting expression.
+
+As an example:
+```lean
+example : 2^10 = eval% 2^10 := by
+  -- goal is `2^10 = 1024`
+  sorry
+```
+This only works if a `Lean.ToExpr X` instance is available.
+-/
+syntax (name := eval_expr) "eval% " term : term
+
+@[term_elab eval_expr]
+unsafe def elabEvalExpr : Lean.Elab.Term.TermElab
+| `(term| eval% $stx) => fun exp => do
+  let e ← Lean.Elab.Term.elabTermAndSynthesize stx exp
+  let e ← instantiateMVars e
+  let ee ← Elab.Term.elabTerm (← `(Lean.toExpr $(← e.toSyntax))) (some q(Expr))
+  Lean.Meta.evalExpr Expr q(Expr) ee (safety := .unsafe)
+| _ => fun _ => Elab.throwUnsupportedSyntax
+
+end Mathlib.Meta

test/eval_elab.lean

@@ -0,0 +1,45 @@
+import Mathlib.Tactic.Eval
+import Mathlib.Data.Finset.Powerset
+import Mathlib.Data.Finset.Sort
+import Std.Tactic.GuardExpr
+
+#guard_expr eval% 2^10 =ₛ 1024
+
+#guard_expr (eval% 2^10 : Int) =ₛ .ofNat 1024
+
+-- https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/How.20to.20simplify.20this.20proof.20without.20using.20a.20have.20statement.3F/near/422294189
+section from_zulip
+
+open Lean Qq
+
+/-- `HasInstance (Foo X)` means than an `inst : Foo X` exists. -/
+class HasInstance (α : Type u) where
+  /-- The reflected version of `inst`. -/
+  expr : Expr
+
+-- this obviously doesn't scale, which is why this is only in the test file
+instance : HasInstance (DecidableEq ℕ) :=
+  ⟨q(inferInstanceAs <| DecidableEq ℕ)⟩
+instance : HasInstance (DecidableEq (Finset ℕ)) :=
+  ⟨q(inferInstanceAs <| DecidableEq (Finset ℕ))⟩
+instance : HasInstance (DecidableEq (Finset (Finset ℕ))) :=
+  ⟨q(inferInstanceAs <| DecidableEq (Finset (Finset ℕ)))⟩
+
+open Qq Lean
+/-- `Finset α` can be converted to an expr only if there is some way to find `DecidableEq α`. -/
+unsafe nonrec instance Finset.toExpr
+    {α : Type u} [ToLevel.{u}] [ToExpr α] [HasInstance (DecidableEq α)] : ToExpr (Finset α) :=
+  have u' : Level := ToLevel.toLevel.{u}
+  have α' : Q(Type u') := Lean.ToExpr.toTypeExpr α
+  letI : Q(DecidableEq $α') := HasInstance.expr (DecidableEq α)
+  { toTypeExpr := q(Finset $α')
+    toExpr := fun x => show Q(Finset $α') from
+      match show List Q($α') from x.val.unquot.reverse.map toExpr with
+      | [] => q(∅)
+      | x0 :: xs => List.foldl (fun s x => q(insert $x $s)) q({$x0}) xs }
+
+#guard_expr
+  (eval% Finset.powerset ({1, 2, 3} : Finset ℕ)) =
+    {∅, {1}, {2}, {1, 2}, {3}, {1, 3}, {2, 3}, {1, 2, 3}}
+
+end from_zulip