Induction on predicates with product type arguments

If I have a predicate like this:

Inductive foo : nat -> nat -> Prop :=
  | Foo : forall n, foo n n.

then I can trivially use induction to prove some dummy lemmas:

Lemma foo_refl : forall n n',
  foo n n' -> n = n'.
Proof.
  intros.
  induction H.
  reflexivity.
Qed.

However, for a predicate with product type arguments:

Inductive bar : (nat * nat) -> (nat * nat) -> Prop :=
  | Bar : forall n m, bar (n, m) (n, m).

a similar proof for nearly identical lemma gets stuck because all assumptions about variables disappear:

Lemma bar_refl : forall n n' m m',
  bar (n, m) (n', m') -> n = n'.
Proof.
  intros.
  induction H.
  (* :( *)

Why is this happening? If I replace induction with inversion, then it behaves as expected.

The lemma is still provable with induction but requires some workarounds:

Lemma bar_refl : forall n n' m m',
  bar (n, m) (n', m') -> n = n'.
Proof.
  intros.
  remember (n, m) as nm.
  remember (n', m') as n'm'.
  induction H.
  inversion Heqnm. inversion Heqn'm'. repeat subst.
  reflexivity.
Qed.

Unfortunately, this way proofs gets completely cluttered and are impossible to follow for more complicated predicates.

One obvious solution would be to declare bar like this:

Inductive bar' : nat -> nat -> nat -> nat -> Prop :=
  | Bar' : forall n m, bar' n m n m.

This solves all the problems. Yet, for my purposes, I find the previous ("tupled") approach somewhat more elegant. Is there a way to keep the predicate as it is and still be able to do manageable inductive proofs? Where does the problem even come from?

Solution

The issue is that induction can only works with variables, not constructed terms. This is why you should first prove something like

Lemma bar_refl : forall p q, bar p q -> fst p = fst q.

which is trivially proved by now induction 1. to prove your lemma.

If you don't want the intermediate lemma to have a name, your solution is the correct one: you need to help Coq with remember to generalize your goal, and then you'll be able to prove it.

I don't remember exactly where this restriction comes from, but I recall something about making some unification problem undecidable.