From 90428cc09b86892e022d2fc4dd7900673e70abfa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 31 Dec 2020 09:41:00 -0800
Subject: [PATCH] feat: expand `let`-decls at `decide!`

---
 src/Lean/Elab/BuiltinNotation.lean |  6 +++++-
 src/Lean/Meta/Transform.lean       | 15 +++++++++++++++
 tests/lean/run/decidelet.lean      |  3 +++
 3 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/decidelet.lean

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 10c7ce4911..e878044ec2 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Init.Data.ToString
 import Lean.Compiler.BorrowedAnnotation
 import Lean.Meta.KAbstract
+import Lean.Meta.Transform
 import Lean.Elab.Term
 import Lean.Elab.SyntheticMVars
 
@@ -135,7 +136,9 @@ private def getPropToDecide (expectedType? : Option Expr) : TermElabM Expr := do
   | none => throwError "invalid macro, expected type is not available"
   | some expectedType =>
     synthesizeSyntheticMVars
-    let expectedType ← instantiateMVars expectedType
+    let mut expectedType ← instantiateMVars expectedType
+    if expectedType.hasFVar then
+      expectedType ← zetaReduce expectedType
     if expectedType.hasFVar || expectedType.hasMVar then
       throwError! "expected type must not contain free or meta variables{indentExpr expectedType}"
     pure expectedType
@@ -150,6 +153,7 @@ private def getPropToDecide (expectedType? : Option Expr) : TermElabM Expr := do
 
 @[builtinTermElab Lean.Parser.Term.decide] def elabDecide : TermElab := fun stx expectedType? => do
   let p ← getPropToDecide expectedType?
+  trace[Meta.debug]! "elabDecide: {p}"
   let d ← mkDecide p
   let d ← instantiateMVars d
   let s := d.appArg! -- get instance from `d`
diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean
index db8f31ffca..0d8b87a989 100644
--- a/src/Lean/Meta/Transform.lean
+++ b/src/Lean/Meta/Transform.lean
@@ -107,5 +107,20 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
         | _                  => visitPost e
   visit input |>.run
 
+def zetaReduce (e : Expr) : MetaM Expr := do
+  let lctx ← getLCtx
+  let pre (e : Expr) : CoreM TransformStep := do
+    match e with
+    | Expr.fvar fvarId _ =>
+      match lctx.find? fvarId with
+      | none => return TransformStep.done e
+      | some localDecl =>
+        if let some value := localDecl.value? then
+          return TransformStep.visit value
+        else
+          return TransformStep.done e
+    | e => if e.hasFVar then return TransformStep.visit e else return TransformStep.done e
+  liftM (m := CoreM) <| Core.transform e (pre := pre)
+
 end Meta
 end Lean
diff --git a/tests/lean/run/decidelet.lean b/tests/lean/run/decidelet.lean
new file mode 100644
index 0000000000..2f0fe461ab
--- /dev/null
+++ b/tests/lean/run/decidelet.lean
@@ -0,0 +1,3 @@
+theorem ex : let x := 1; x < 2 := by
+  intro x
+  decide!