congr_arg puzzle

Stream: general

[Kevin Buzzard]

A friend pointed out to me that one of these three proofs doesn't work:

example (a b : int) (h : b = 0) : 2*b+a = 2*0+a :=
congr_arg (fun t, 2*t+a) h

example (a b : int) (h : b = 0) : a+2*b = a+2*0 :=
congr_arg (λ t, a+2*t) h

example (a b : int) (h : b = 0) : a+b = a+0 :=
congr_arg (fun t, a+t) h

Can you guess which without using Lean? I cannot figure out what is going on from the error message in the one which fails.

[Mario Carneiro]

My bet (haven't checked) is that the second one fails, with the error that h does not have the type 2*b = 2*0

[Mathieu Guay-Paquet]

A fun fact is that the error goes away when I replace congr_arg with @congr_arg _ _ _ _.

It's the one that uses λ rather than fun.

[Mario Carneiro]

another fun fact is that the error goes away if you use (congr_arg (λ t, a+2*t) h : _). (assuming my guess is correct)

[Mathieu Guay-Paquet]

@Mario Carneiro you have (one of?) the right error, but your fun fact seems false

[Mathieu Guay-Paquet]

Oh no wait it's true, I entered it wrong

[Mario Carneiro]

I didn't think lean would be able to report both errors here, usually it only gets one per application

[Mathieu Guay-Paquet]

I see 2 errors in the infoview, but they're under different headings, so you're probably still right

[Mario Carneiro]

anyway, what's happening is that since congr_arg has no special elaborator markings on it, and it has the type f x = f y, lean tries to match this pattern against the goal which is add a (2*b) = add a (2*0), and decides that f := add a and x := 2*b, y := 2*0. This eventually leads to a failure, and the resulting errors. With the : _ trick, it has no expected type to match against so it leaves f,x,y as unbound, and eventually uses h and the provided lambda to produce the right answer. The target type becomes (λ t, a+2*t) b = (λ t, a+2*t) 0 at this point, and this is then unified against a+2*b = a+2*0, which succeeds

[Mario Carneiro]

In the first example, the application heuristic fails, because add (2*b) a = add (2*0) a does not have the form f x = f y (since add (2*b) is not defeq to add (2*0)), so it falls back on checking the type as in the : _ version, which works

[Mario Carneiro]

In the third example, it uses the application heuristic, leading to f := add a and x := b, y := 0, but this time it works, because (fun t, a+t) is defeq to add a and h actually does have the type b = 0