Dealing with let-in expressions in current goal

Question

I got stuck while doing some coq proofs around the state monad. Concretely, I've simplified the situation to this proof:

Definition my_call {A B C} (f : A -> B * C) (a : A) : B * C :=
  let (b, c) := f a in (b, c).

Lemma mycall_is_call : forall {A B C} (f : A -> B * C) (a : A),
    my_call f a = f a.
forall (A B C : Type) (f : A -> B * C) (a : A),
my_call f a = f a
Proof.
forall (A B C : Type) (f : A -> B * C) (a : A),
my_call f a = f a
  intros A B C f a.
A, B, C: Type
f: A -> B * C
a: A
my_call f a = f a unfold my_call.
A, B, C: Type
f: A -> B * C
a: A
(let (b, c) := f a in (b, c)) = f a
  (* stuck! *)

The resulting goal after invoking unfold is

1 subgoal

  A : Type
  B : Type
  C : Type
  f : A -> B * C
  a : A
  ============================
  (let (b, c) := f a in (b, c)) = f a

If I'm not wrong, both sides of the equality should be exactly the same, but I don't know how to show it from here. Any help?

As a side note, I've seen that coq automatically applies the simplification when no product types are involved in the result of the function:

Definition my_call' {A B : Type} (f : A -> B) (a : A) : B :=
  let b := f a in b.

Lemma my_call_is_call' : forall A B (f : A -> B) (a : A),
    my_call' f a = f a.
forall (A B : Type) (f : A -> B) (a : A),
my_call' f a = f a
Proof.
forall (A B : Type) (f : A -> B) (a : A),
my_call' f a = f a
  intros A B f a.
A, B: Type
f: A -> B
a: A
my_call' f a = f a unfold my_call'.
A, B: Type
f: A -> B
a: A
f a = f a reflexivity.
Qed.

Answer

It's easy to see what you need to do next, once you recall that

let (b, c) := f a in (b, c)

is syntactic sugar for

match f a with (b, c) => (b, c) end

This means you need to destruct on f a to finish the proof:

Lemma mycall_is_call {A B C} (f : A -> B * C) a :
  my_call f a = f a.
A, B, C: Type
f: A -> B * C
a: A
my_call f a = f a
Proof.
A, B, C: Type
f: A -> B * C
a: A
my_call f a = f a
  unfold my_call.
A, B, C: Type
f: A -> B * C
a: A
(let (b, c) := f a in (b, c)) = f a now destruct (f a).
Qed.

A: Note that you can Set Printing All to make the syntactic sugar go away.

A: With pairs defined with primitive projections (as here), we can prove mycall_is_call lemma using just reflexivity.