chore: fix test

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -283,6 +283,17 @@ private def addSplitCandidatesForFunext (arg : Expr) (generation : Nat) (parent?
   unless (← getConfig).funext do return ()
   addSplitCandidatesForExt arg generation parent?
 
+/--
+Tries to eta-reduce the given expression.
+If successful, pushes a new equality between the two terms.
+-/
+private def tryEta (e : Expr) (generation : Nat) : GoalM Unit := do
+  let e' := e.eta
+  if e != e' then
+    let e' ← shareCommon e'
+    internalize e' generation
+    pushEq e e' (← mkEqRefl e)
+
 @[export lean_grind_internalize]
 private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := withIncRecDepth do
   if (← alreadyInternalized e) then
@@ -313,6 +324,7 @@ where
     | .lam .. =>
       addSplitCandidatesForFunext e generation parent?
       mkENode' e generation
+      tryEta e generation
     | .forallE _ d b _ =>
       mkENode' e generation
       internalizeImpl d generation e

tests/lean/run/grind_beta.lean

@@ -30,8 +30,8 @@ example (f : Nat → Nat → Nat) : f 2 3 ≠ 5 → f = (fun x y : Nat => x + y)
 opaque bla : Nat → Nat → Nat → Nat
 
 /--
-trace: [grind.beta] f 2 3 = bla 2 3 2, using fun x y => bla x y x
-[grind.beta] f 2 3 = 2 + 3, using fun x y => x + y
+trace: [grind.beta] f 2 3 = 2 + 3, using fun x y => x + y
+[grind.beta] f 2 3 = bla 2 3 2, using fun x y => bla x y x
 -/
 #guard_msgs (trace) in
 set_option trace.grind.beta true in

tests/lean/run/grind_eta.lean

@@ -0,0 +1,15 @@
+reset_grind_attrs%
+set_option grind.warning false
+
+example {l : List α} {f : β → α → β} {b : β} :
+    l.foldl f b = l.reverse.foldr (fun x y => f y x) b := by
+  grind [List.foldr_reverse]
+
+/-
+The following example doesn't work yet. `grind` doesn't have a mechanism
+for inferring that `fun x y => g y x` is equal to `f` given
+the equality `g = (f x y => f y x)`
+-/
+-- example {l : List α} {f : β → α → β} {b : β} :
+--    g = (fun x y => f y x) → l.foldl f b = l.reverse.foldr g b := by
+--  grind [List.foldr_reverse]

tests/lean/run/grind_funext.lean

@@ -4,8 +4,10 @@ example (f : (Nat → Nat) → Nat → Nat → Nat) : a = b → f (fun x => a +
   grind
 
 example (f : (Nat → Nat) → Nat) : a = b → f (fun x => a + x) = f (fun x => b + x) := by
-  fail_if_success grind -funext
-  sorry
+  -- This test used to check `fail_if_success grind -funext`,
+  -- but now it succeeds even without funext
+  -- due to adding the eta rule in https://github.com/leanprover/lean4/pull/7977.
+  grind
 
 example (g : Nat → Nat → Nat) (f : (Nat → Nat) → Nat → (Nat → Nat) → Nat) :
     a = b → f (fun x => a + x) 1 (fun x => g x a) = f (fun x => x + b) 1 (fun x => g x b) := by