Simp fails to apply with `Function.update`

Stream: mathlib4

[David Loeffler]

Here's a MWE of a strange failure that came up when reviewing one of @Chris Birkbeck 's modular forms PR's #32959 [edit: simplified MWE slightly] [edit: changed it back, I had simplified it too much]:

import Mathlib

lemma foo (f : ℂ → ℂ)
    (H : (Function.update f 0 1) 0 = 1) :
    (Function.update f 0 1) (0 + 0) = 1 := by
  simp only [zero_add] -- fails, but `rw [zero_add]` works
  exact H

I don't understand why simp only fails here. It works fine if you replace Function.update f 0 1 with f, so it must be something specifically about the interaction between simp and Function.update.

[Ruben Van de Velde]

Odd.

import Mathlib

lemma foo (f : ℕ → ℕ)
    (H : (Function.update f 0 1) 0 = 1) :
    (Function.update f 0 1) (0 + 0) = 1 := by
  conv =>
    enter [1, 4]
    simp only [zero_add (0 : Nat)] -- works
  exact H

[Aaron Liu]

Is it because Function.update is dependent in that position

[David Loeffler]

Aaron Liu said:

Is it because Function.update is dependent in that position

Indeed, it seems to be! The definition of Function.update allows dependent functions, and if you make a non-dependent copy of it, then the problem goes away.

Here's a completely de-mathlibified version:

universe u v

variable {α : Type u} [DecidableEq α]


/-- Mathlib's `Function.update` allowing dependent functions
(copied from Mathlib.Logic.Function.Basic) -/
def dupdate {β : α → Type v}
    (f : ∀ a, β a) (a' : α) (v : β a') (a : α) : β a :=
  if h : a = a' then Eq.ndrec v h.symm else f a

theorem foo (f : Nat → Nat) (a b : Nat) (hab : a = b) :
    (dupdate f 0 1) a = (dupdate f 0 1) b := by
  simp only [hab] -- fails, but `rw [hab]` works


/-- Non-dependent version of `Function.update` -/
def ndupdate {β : Type v}
    (f : α → β) (a' : α) (v : β) (a : α) : β :=
  if a = a' then v else f a

theorem foo2 (f : Nat → Nat) (a b : Nat) (hab : a = b) :
    (ndupdate f 0 1) a = (ndupdate f 0 1) b := by
  simp only [hab] -- works

I could report this as a Lean issue, but I'm not sure if this would be considered as a "bug" in simp or just "not in simp's scope" – any thoughts?

[Joachim Breitner]

It's not a bug, at most a missing feature.

The component in question is probably the simp congruence theorem generation. I wonder if for functions where the dependency depends on some higher order argument, like here or in match statements, one could create specialized congr theorems for when that higher order function is actually constant.

But it's not a simple change, so don't hold your breath.

An issue to record the desires for this and to collect instances would be appreciated.

[David Loeffler]

Thanks Joachim! I have filed a Lean issue for this at lean4#12478.

[Robin Arnez]

I'll also note the workaround which is to create a congruence lemma yourself:

import Mathlib

@[congr]
lemma Function.update_congr.{u, v}
    {α : Sort u} {β : Sort v} [DecidableEq α]
    {f₁ f₂ : α → β} (hf : f₁ = f₂)
    {a'₁ a'₂ : α} (ha' : a'₁ = a'₂)
    {v₁ v₂ : β} (hv : v₁ = v₂)
    {a₁ a₂ : α} (ha : a₁ = a₂) :
    Function.update f₁ a'₁ v₁ a₁ = Function.update f₂ a'₂ v₂ a₂ := by
  subst hf; subst ha'; subst hv; subst ha; rfl

lemma foo (f : ℂ → ℂ)
    (H : (Function.update f 0 1) 0 = 1) :
    (Function.update f 0 1) (0 + 0) = 1 := by
  simp only [zero_add] -- works!
  exact H

[Eric Wieser]

We should probably add that and the Pi.single version to mathlib, with comments noting they are specialized to the non-dependent case

[Robin Arnez]

Here: #35423