Getting simp to chain together lemmas

Stream: general

[Joseph Tooby-Smith]

Consider this mwe

import Mathlib

def g : ℕ → ℕ := fun n => 0

lemma congr_fun' (f : ℕ → ℕ) {a b : ℕ} (h : g a = g b) :
    g (f a) = g (f b) := by
  rw [g, g]

lemma congr_fun_seq (f : ℕ → ℕ) {a b : ℕ} (h : g a = g b) :
    g (f a) = g (f b) := by
  simp [congr_fun', h] -- does nothing
  simp  [congr_fun' _ <| h] -- works


lemma congr_fun_seq' (f : ℕ → ℕ) {a b : ℕ} (h : g a = g b) :
    g (f (f a)) = g (f (f b)) := by
  simp [congr_fun', h] -- does nothing
  simp  [congr_fun' _ <| congr_fun' _ <| h] -- works

The situation I am working in is a more complicated than this, but I think this gives the idea. My question is this:

Are there any settings for simp that I can use to get it to chain lemmas together, so that it considers e.g. congr_fun' _ <| congr_fun' _ <| h automatically when given congr_fun and h? Maybe up to some level of recursion

[Joseph Tooby-Smith]

(Replacing simp with simpa on the lines which do nothing actually works but only by the nature of g and not be chaining lemmas).

[Kyle Miller]

Congruence lemmas don't work well as simp lemmas. The issue is that simp sees congr_fun' as a conditional rewrite rule g (?f ?a) ==> g (?f ?b), given that g ?a = g ?b can be discharged. This means that when simp [congr_fun', h] sees the target g (f a) = g (f b), while it considers rewriting g (f a) ==> g (f ?b) and g (f b) ==> g (f ?b), it fails because g a = g ?b and g b = g ?b can't be discharged (it won't assign ?b to something in this context just because there's an h in hand; that would be fragile).

In particular, notice that the equality turns into a rule. It won't apply to the entire expression.

If you want it to apply to the entire expression, you can do

lemma congr_fun'' (f : ℕ → ℕ) {a b : ℕ} (h : g a = g b) :
    (g (f a) = g (f b)) = True := by
  rw [g, g]

lemma congr_fun_seq (f : ℕ → ℕ) {a b : ℕ} (h : g a = g b) :
    g (f a) = g (f b) := by
  simp only [congr_fun'', h]

This lemma is instead creating the rule g (?f ?a) = g (?f ?b) ==> True.

There's a mechanism to override the congruence lemmas that simp uses with the @[congr] attribute, but congr_fun'' isn't a valid congruence lemma in that sense.

[Kyle Miller]

Joseph Tooby-Smith said:

(Replacing simp with simpa on the lines which do nothing actually works but only by the nature of g and not be chaining lemmas).

Very likely.

lemma congr_fun_seq (f : ℕ → ℕ) {a b : ℕ} (h : g a = g b) :
    g (f a) = g (f b) := by
  exact h -- `assumption` works too

[Joseph Tooby-Smith]

Ok, thanks @Kyle Miller ! I'll have a think and see what I can get to work!