The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

I have a lot of theorems in which I implicitly destruct pairs by using a forall construct. Here is an example:

Definition f : nat -> nat * nat := fun x => (x, x).

Lemma silly : forall x y, f 1 = (x, y) -> x = y.
Proof. Admitted.

Now, I'd like to use lemmas like silly as hypothesis in other proofs. But the point is that there is an obvious value for x and y which can be used since f is a function.

I tried writing a tactic that automatically destructs the term (f 1) and finds x and y so that the part after the -> can be used.

Ltac introsP H a b :=
  match goal with
  | [ H : (forall x y, ?f ?t = (x, y) -> ?X) |- _ ] =>
    destruct (f t) as [a b] eqn:XX; specialize (H x y XX)
  | [ H : (forall x y, (x, y) = ?f ?t -> ?X) |- _ ] =>
    destruct (f t) as [a b] eqn:XX; specialize (H x y XX)
  end.

However, I can't get this to work:

Goal 2 = 2.
  pose proof silly.
  introsP H a b.

How do I get this tactic to work?

--Agnishom