From 3a369938c8bb88d0f3acb43083cd676e2440bc3a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Jan 2021 09:52:01 -0800
Subject: [PATCH] feat: `simpLambda`

---
 src/Lean/Meta/AppBuilder.lean       |  4 ++++
 src/Lean/Meta/Tactic/Simp/Main.lean | 10 +++++++++-
 tests/lean/run/simp3.lean           |  8 ++++++++
 3 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index c0a2549782..cdbe00e354 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -391,6 +391,10 @@ def mkArbitrary (α : Expr) : MetaM Expr :=
 def mkSyntheticSorry (type : Expr) : MetaM Expr :=
   return mkApp2 (mkConst `sorryAx [← getLevel type]) type (mkConst `Bool.true)
 
+/-- Return `funext h` -/
+def mkFunExt (h : Expr) : MetaM Expr :=
+  mkAppM `funext #[h]
+
 builtin_initialize registerTraceClass `Meta.appBuilder
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 0f5ee8e1d3..6192c6a960 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -141,7 +141,15 @@ where
         return r
 
   simpLambda (e : Expr) : M σ Result :=
-    return { expr := e } -- TODO
+    lambdaTelescope e fun xs e => do
+      -- TODO: cfg.contextual
+      let r ← simp e
+      match r.proof? with
+      | none   => return { expr := (← mkLambdaFVars xs r.expr) }
+      | some h =>
+        let p ← xs.foldrM (init := h) fun x h => do
+          mkFunExt (← mkLambdaFVars #[x] h)
+        return { expr := (← mkLambdaFVars xs r.expr), proof? := p }
 
   simpForall (e : Expr) : M σ Result :=
     return { expr := e } -- TODO
diff --git a/tests/lean/run/simp3.lean b/tests/lean/run/simp3.lean
index cacb5038e5..183965e2a0 100644
--- a/tests/lean/run/simp3.lean
+++ b/tests/lean/run/simp3.lean
@@ -10,3 +10,11 @@ constant g (x : Nat) : Nat
 @[simp] theorem add1 (x : Nat) : x + 1 = x.succ := rfl
 
 theorem ex3 (x : Nat) : g (x + 1) = 2 := by simp
+
+theorem ex4 (x : Nat) : (fun x => x + 1) = (fun x => x.succ) := by simp
+
+@[simp] theorem comm (x y : Nat) : x + y = y + x := Nat.addComm ..
+@[simp] theorem addZ (x : Nat) : x + 0 = x := rfl
+@[simp] theorem zAdd (x : Nat) : 0 + x = x := Nat.zeroAdd ..
+
+theorem ex5 (x y : Nat) : (fun x y : Nat => x + 0 + y) = (fun x y : Nat => y + x + 0) := by simp