congr matching addition and subtraction

Stream: mathlib4

[Michael Rothgang]

Yesterday at the SLMath+ICARM event (introducing Lean to PDE people), @Rémy Degenne and I hit this behaviour of congr that surprised us a lot. The starting example is one where a bare congr recurses too deep (and you want to use congr 1 instead). Explaining how a + b = b + a gets converted into two subgoals is easy.

However, with a + b = b - (-a), we still get two subgoals: why is this?

-- minimised from the Short track of GlimpseOfLean
import Mathlib

example (a b : ℝ) (f : ℝ → ℝ) : f (a + b) = f (b + a) := by
  congr
  -- congr is too eager, and reduces the goal to two goals a = b (and b = a)
  · guard_target = a = b
    sorry
  · guard_target = b = a
    sorry

example (a b : ℝ) (f : ℝ → ℝ) : f (a + b) = f (b - -a) := by
  -- Question: why does congr still fire, and create two subgoals?
  congr
  · guard_target = a = b
    sorry
  · guard_target = b = -(-a)
    sorry
-- Adding parentheses around (-a) seems to make no difference.
example (a b : ℝ) (f : ℝ → ℝ) : f (a + b) = f (b - (-a)) := by
  congr
  · guard_target = a = b
    sorry
  · guard_target = b = -(-a)
    sorry

[Kenny Lau]

import Mathlib

def f : Nat → Nat := fun n ↦ 3
def g : Nat → Nat := fun n ↦ 4

example : 4 = g 1 := by congr

well it looks like congr looks through definitions

[Kenny Lau]

and a-b is defined to be a+(-b)

[Michael Rothgang]

Ok, but then why does congr make no progress here?

import Mathlib

example (a b : ℝ) : (a + b) ^ 2 - 2 * a * b = a ^ 2 + b ^ 2 := by
  congr -- makes no progress
  sorry

[Michael Rothgang]

I think this is good behaviour (considered in isolation) --- but I don't know how to explain this!

[Kevin Buzzard]

import Mathlib

example (a b : ℝ) : (a + b) ^ 2 - 2 * a * b = a ^ 2 + b ^ 2 := by
  unfold HSub.hSub instHSub Sub.sub Real.instSub
  dsimp only
  congr -- two goals
  sorry
  sorry

Aah congr doesn't look through definitions after all! Or maybe it looks through some definitions?

[Edward van de Meent]

i think it uses the LHS to figure out the pattern, as congr works after symm:

example (a b : ℝ) : (a + b) ^ 2 - 2 * a * b = a ^ 2 + b ^ 2 := by
  symm
  congr 1 -- just to show the initial step
  · guard_target = a ^ 2 = (a + b) ^ 2
    sorry -- `congr` by itself would lead to `a = a + b` as a goal
  · guard_target = b ^ 2 = -(2 * a * b)

[Edward van de Meent]

other than that, it seems to use default reducibility to check defeq.

[Edward van de Meent]

which means it sees through most defs, instances and abbrevs on the right-hand side (with the caviat that recursive defs can automatically be marked irreducible)

[Kyle Miller]

My suggestion is to use congr! instead.

That tactic attempts to do congr correctly, and eventually I will get around to updating congr.

I have not read this thread carefully, but the likely issue being activated is that congr uses the LHS to choose a congruence lemma, and then it applies it. This can unfold definitions on the RHS. What congr! does instead is look at both sides when deciding how to match things up.

Another benefit to congr! is that it has some heuristics to avoid equating types, so it's more likely you don't need to include a limit, though arithmetic operations can still create weird goals (like a goal to prove that HAdd.hAdd = HSub.hSub for the Real instances).

[Kyle Miller]

(The ! in congr! is "try harder to do the right thing", though it also is able to make use of HEq more effectively to make more progress.)