Simplify lambda expressions

Stream: Is there code for X?

[Jeremy Salwen]

Here is a MWE. I would like to simplify the LHS of the equation to just f. (RHS is irrelevant).

import Lean
import Mathlib.Tactic.Find

def f: ℕ  → ℕ  := sorry
def asdf : (λ a => f a) = (λ a => f (f a)) := by simp

unfortunately simp does nothing here. It seems like there were a few previous threads about reducing these sorts of expressions (e.g. https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Simplifying.20lambda.20expressions) and that the conclusion was that this simplification is called beta reduction and dsimp only or simp only should handle it, but that does not seem to be happening here.

[Chris Bailey]

You need to give it a little bit more direction, I think.

def asdf : (λ a => f a) = (λ a => f (f a)) := by
  simp only [show (λ a => f a) = f by rfl]
  trace_state

[Jeremy Salwen]

Hmm, this doesn't seem ideal. Why is simp unable to do the beta reduction? In general do I need to manually clean up the beta reductions that simp fails to do? Or is there another tactic for this scenario?

[Chris Bailey]

This is not beta reduction, it's eta reduction/expansion. The definitional equality procedure checks eta equivalence which is why rfl works, but simp needs to know what you want to rewrite with in this case.

[Chris Bailey]

There's an eta := true option for the simp config, but I'm not sure how it works.

[Yaël Dillies]

simp (config := { eta := true }) should do, if not unacceptably long

[Jeremy Salwen]

Yaël Dillies said:

simp (config := { eta := true }) should do, if not unacceptably long

I tried this, it still doesn't have any effect.

[Jeremy Salwen]

I've tried searching more through zulip and the mathlib docs, and came up short. #reduce doesn't simplify this expression either.

There is the Expr.etaExpanded? function, which I can use to calculate the eta-reduced form of a a type:

def transformEtaReduce (e: Expr): MetaM Expr := do
  transform e (λ node => do
  pure (match node.etaExpanded? with
        | some reduced =>
          TransformStep.continue reduced
        | none => TransformStep.continue
        ))

but this is not actually generating proof terms.

[Kyle Miller]

Oh, now that you've written that, it's not so hard to wrap an interactive tactic around it:

import Lean

open Lean Meta Elab.Tactic

def transformEtaReduce (e: Expr): MetaM Expr := do
  transform e fun node => pure <| TransformStep.continue node.etaExpanded?

syntax "eta_reduce" : tactic

elab_rules : tactic
  | `(tactic| eta_reduce) =>
    liftMetaTactic1 fun mvarId => do
      let ty ← instantiateMVars (← mvarId.getType)
      -- Eta reduction is defeq:
      mvarId.change (← transformEtaReduce ty)

def f: Nat  → Nat  := sorry
def asdf : (λ a => f a) = (λ a => f (f a)) := by
  eta_reduce
  -- goal: f = fun a ↦ f (f a)

[Kyle Miller]

With a little more work you can support eta_reduce at h syntax too.

[Kyle Miller]

Here, with locations:

import Mathlib.Tactic.Basic

open Lean Meta Elab.Tactic

def transformEtaReduce (e: Expr): MetaM Expr := do
  transform e fun node => pure <| TransformStep.continue node.etaExpanded?

syntax "eta_reduce" (ppSpace Parser.Tactic.location)? : tactic

elab_rules : tactic
  | `(tactic| eta_reduce $[$loc?]?) =>
  withLocation (expandOptLocation (Lean.mkOptionalNode loc?))
    (atLocal := fun h => liftMetaTactic1 fun mvarId => do
      let ty ← instantiateMVars (← h.getType)
      mvarId.changeLocalDecl' h (← transformEtaReduce ty))
    (atTarget := liftMetaTactic1 fun mvarId => do
      let ty ← instantiateMVars (← mvarId.getType)
      mvarId.change (← transformEtaReduce ty))
    (failed := fun _ => throwError "eta_reduce failed")

def f: Nat  → Nat  := sorry
theorem asdf : (λ a => f a) = (λ a => f (f a)) := by
  eta_reduce
  -- goal: f = fun a ↦ f (f a)

theorem asdf' (h : (λ a => f a) = (λ a => f (f a))) : True := by
  eta_reduce at h
  -- h : f = fun a ↦ f (f a)

theorem asdf'' (h : (λ a => f a) = (λ a => f (f a))) : (λ a => f a) = (λ a => f (f a)) := by
  eta_reduce at *
  -- h : f = fun a ↦ f (f a)
  -- ⊢ f = fun a ↦ f (f a)

[Kyle Miller]

An eta_expand would be interesting too, but to do that right you'd need a transformer that processes entire function applications. This transformer expands every function:

def transformEtaExpand (e : Expr) : MetaM Expr := do
  transform e (post := fun node => TransformStep.done <$> Meta.etaExpand node)

That gives some silly results:

example : (fun (a b : Nat) => a + b) = (· + ·) := by
  eta_expand
  -- goal: (fun {α} a a_1 ↦ a = a_1) (fun a b ↦ (fun a b ↦ (fun {α β} {γ}
  --   [HAdd α β γ] a a_1 ↦ a + a_1) a b) a b) fun x x_1 ↦ (fun x x_2 ↦ (fun {α β} {γ} [HAdd α β γ]
  --   a a_1 ↦ a + a_1) x x_2) x x_1

Beta reducing the result fixes that, but maybe there's a better way?

def transformEtaExpand (e : Expr) : MetaM Expr := do
  let e' ← transform e (post := fun node => TransformStep.done <$> Meta.etaExpand node)
  Core.betaReduce e'

This at least works as an inverse to eta_reduce:

example : (fun (a b : Nat) => a + b) = (· + ·) := by
  -- goal: (fun a b ↦ a + b) = fun x x_1 ↦ x + x_1
  eta_reduce
  -- goal: HAdd.hAdd = HAdd.hAdd   (has implicit arguments for Nat instances)
  eta_expand
  -- goal: (fun a a_1 ↦ a + a_1) = fun a a_1 ↦ a + a_1

[Kyle Miller]

Here are both tactics together:

code

import Mathlib.Tactic.Basic
import Mathlib.Data.Set.Basic

open Lean Meta Elab.Tactic

def transformEtaReduce (e : Expr) : MetaM Expr := do
  transform e fun node => pure <| TransformStep.continue node.etaExpanded?

/-- Like `Lean.Meta.etaExpand` but using reducible transparancy. This prevents `Set` for example
from being eta expanded. -/
def etaExpand' (e : Expr) : MetaM Expr :=
  withReducible do forallTelescopeReducing (← inferType e) fun xs _ => mkLambdaFVars xs (mkAppN e xs)

def transformEtaExpand (e : Expr) : MetaM Expr := do
  let e' ← transform e (post := fun node => TransformStep.done <$> etaExpand' node)
  Core.betaReduce e'

syntax "eta_reduce" (ppSpace Parser.Tactic.location)? : tactic

elab_rules : tactic
  | `(tactic| eta_reduce $[$loc?]?) =>
  withLocation (expandOptLocation (Lean.mkOptionalNode loc?))
    (atLocal := fun h => liftMetaTactic1 fun mvarId => do
      let ty ← instantiateMVars (← h.getType)
      mvarId.changeLocalDecl' h (← transformEtaReduce ty))
    (atTarget := liftMetaTactic1 fun mvarId => do
      let ty ← instantiateMVars (← mvarId.getType)
      mvarId.change (← transformEtaReduce ty))
    (failed := fun _ => throwError "eta_reduce failed")

syntax "eta_expand" (ppSpace Parser.Tactic.location)? : tactic

elab_rules : tactic
  | `(tactic| eta_expand $[$loc?]?) =>
  withLocation (expandOptLocation (Lean.mkOptionalNode loc?))
    (atLocal := fun h => liftMetaTactic1 fun mvarId => do
      let ty ← instantiateMVars (← h.getType)
      mvarId.changeLocalDecl' h (← transformEtaExpand ty))
    (atTarget := liftMetaTactic1 fun mvarId => do
      let ty ← instantiateMVars (← mvarId.getType)
      mvarId.change (← transformEtaExpand ty))
    (failed := fun _ => throwError "eta_expand failed")

def f: Nat  → Nat  := sorry
theorem asdf : (λ a => f a) = (λ a => f (f a)) := by
  eta_reduce
  -- goal: f = fun a ↦ f (f a)

theorem asdf' (h : (λ a => f a) = (λ a => f (f a))) : True := by
  eta_reduce at h
  -- h : f = fun a ↦ f (f a)

theorem asdf'' (h : (λ a => f a) = (λ a => f (f a))) : (λ a => f a) = (λ a => f (f a)) := by
  eta_reduce at *
  -- h : f = fun a ↦ f (f a)
  -- ⊢ f = fun a ↦ f (f a)

example : (fun (a b : Nat) => a + b) = (· + ·) := by
  -- goal: (fun a b ↦ a + b) = fun x x_1 ↦ x + x_1
  eta_reduce
  -- goal: HAdd.hAdd = HAdd.hAdd   (has implicit arguments of course)
  eta_expand
  -- goal: (fun a a_1 ↦ a + a_1) = fun a a_1 ↦ a + a_1

example (s t : Set α) : s = t := by
  eta_expand
  -- goal: s = t  (good; don't want `Set` to be seen as a function)

[Kevin Buzzard]

well and truly nerdsniped :-) Very nice!

[Jeremy Salwen]

For the transformEtaExpand would it make sense to do the beta reduction as part of the transform so it's single pass? Like this?

def betaReduceHead (e:Expr): Expr :=
  if e.isHeadBetaTarget then e.headBeta else e

def transformEtaExpand (e : Expr) : MetaM Expr := do
  let e' ← transform e (post := fun node => TransformStep.done <$> betaReduceHead <$> Meta.etaExpand node)
  Core.betaReduce e'

[Kyle Miller]

The thing this is working around is that if you have an expression f x, then we first look at f and we get (fun y => f y) x, so then when we look at this whole application we need to beta reduce it. Beta reducing as part of the post pass will work, but really it'd be better to never do these sorts of eta expansions in the first place so that we never need to beta reduce.