gcongr and local definitions

Stream: mathlib4

[Yury G. Kudryashov]

import Mathlib.Tactic.GCongr

example (m n : ℕ) (h : m ≤ n) : m + 1 ≤ n + 1 := by
  set f : ℕ → ℕ := (· + 1)
  change f m ≤ f n
  gcongr -- Makes no progress

[Yury G. Kudryashov]

What's the proper way to fix this: change gcongr or unfold f before calling it?

[Yury G. Kudryashov]

In fact, I'm not sure if it is about set or about (· + 1) m vs m + 1

[Yury G. Kudryashov]

Both make gcongr fail:

import Mathlib.Tactic.GCongr

attribute [gcongr] Nat.succ_le_succ in
example (m n : ℕ) (h : m ≤ n) : Nat.succ m ≤ Nat.succ n := by
  set f := Nat.succ
  gcongr

[Yury G. Kudryashov]

@Heather Macbeth :up:

[Heather Macbeth]

That behaviour is what I would expect at the moment. With the operation + 1 hidden behind a definition, gcongr has no way of knowing that operation is monotone. And it doesn't beta-reduce, which is why it fails on (· + 1) m ≤ (· + 1) n.

[Yury G. Kudryashov]

Shouldn't it do both (beta reduction and unfolding let definitions)?

[Heather Macbeth]

A related beta-reduction issue has been discussed several times before: it's not possible to tag as @[gcongr] a lemma with a missing beta-reduction in the wrong place. This is why docs#GCongr.sum_le_sum exists: the standard version of the lemma, docs#Finset.sum_le_sum, has a non-beta-reduced conclusion, (Finset.sum s fun (i : ι) => f i) ≤ Finset.sum s fun (i : ι) => g i. Same issue with integrals, etc.

[Heather Macbeth]

Yury G. Kudryashov said:

Shouldn't it do both (beta reduction and unfolding let definitions)?

My tentative opinion is: gcongr should beta-reduce, and it should have a ! version which unfolds let definitions and perhaps makes other reducibility adjustments.

[Heather Macbeth]

But the reducibility settings seem to be performance-critical:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60gcongr.60.20speed
so I assume this is a delicate question.

[Yury G. Kudryashov]

Thank you for the explanation about performance.