## Stream: general

### Topic: congr_arg puzzle

#### Kevin Buzzard (Mar 12 2021 at 21:12):

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 (Mar 12 2021 at 21:28):

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 (Mar 12 2021 at 21:33):

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

#### Mario Carneiro (Mar 12 2021 at 21:34):

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 (Mar 12 2021 at 21:39):

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

#### Mathieu Guay-Paquet (Mar 12 2021 at 21:39):

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

#### Mario Carneiro (Mar 12 2021 at 21:40):

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

#### Mathieu Guay-Paquet (Mar 12 2021 at 21:41):

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

#### Mario Carneiro (Mar 12 2021 at 21:44):

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 (Mar 12 2021 at 21:46):

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 (Mar 12 2021 at 21:47):

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

Last updated: Aug 03 2023 at 10:10 UTC