The Coq mailing list

[Carl Patenaude-Poulin <carlpaten AT protonmail.com>]

If you add idtac H; (basically a printf) at the start of each pattern branch, you can see that in your example the first branch is entered, but is then exited. This points to one of the tactics in that branch failing. You can pinpoint the problem further by testing with parts of the branch commented out. In particular, commenting out the call to specialize makes the tactic succeed, so you know there's something wrong with that part.

Hope that helps.

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐

On Tuesday, April 14, 2020 12:32 PM, Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

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