Predicate induction with product type arguments

Question

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 fictitious 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 of an almost 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 replaced inductionwith inversion, it will behave as expected.

The lemma is still provable with help 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, in this way the evidence becomes completely cluttered and impossible for more complex predicates.

One obvious solution would be to declare baras follows:

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

. , , , ( "" ) . , , ? ?

Answer 1

, , . -

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

now induction 1., .

, , : Coq remember, , .

, , - , .

Answer 2

.

n,

Lemma bar_refl : forall n n' m m',  bar (n, m) (n', m') -> n = n'.
Proof. induction n; intros; inversion H; auto. Qed.

Answer 3

... ... ? induction inversion, , .

, , : Coq . :

Coq , . , destruct (, even 3: !) ( forall n, even (2*n+1) -> False ( nat) - !). Coq . , . destruct - : - . ( inversion ). . , . .

, destruct H. :

Lemma bar_refl : forall n n' m m',
  bar (n, m) (n', m') -> n = n'.
Proof.
  intros n n' m m' H.
  refine (match H with
          | Bar a b => _
          end).

:

n, n', m, m' : nat
H : bar (n, m) (n', m')
a, b : nat
============================
n = n'

, H , clear H.: refine (...); clear H.. . Coq (n, m) (n',m'), p p', , p = (a, b) p' = (a, b). , n = n', (n,m), (n',m') - Coq a = a.

Coq . , , , . @Vinz, , :

  Undo.  (* to undo the previous pattern-matching *)
  refine (match H in (bar p p') return fst p = fst p' with
          | Bar a b => _
          end).

Coq, H - p p' , Coq fst p = fst p' p p' (a,b). :

n, n', m, m' : nat
H : bar (n, m) (n', m')
a, b : nat
============================
fst (a, b) = fst (a, b)

reflexivity .

, , destruct ( , ):

Lemma bar_refl_all : forall n n' m m',
  bar (n, m) (n', m') -> (n, m) = (n', m').
Proof.
  intros. destruct H. reflexivity.
Qed.

: , , Coq .

Answer 4

Another way...

Lemma bar_refl n n' m m' : bar (n, m) (n', m') -> n = n'.
Proof.
  change (n = n') with (fst (n,m) = fst (n',m')).
  generalize (n,m) (n',m').
  intros ? ? [ ]; reflexivity.
Qed.