The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le lundi 09 février 2009 à 22:12 +0900, Keiko Nakata a écrit :

> How can I prove the following goal? 
> It looked so obvious that I thought auto would handle.

While obvious, the proof that both expressions compute the same result
requires to decompose inductive objects, so as to get convertible
expressions. The auto tactic does not perform such transformations, as
far as I know.

> Goal forall (p : nat -> Prop) (f : nat -> nat) (n : nat * nat),
> (let (n1, _) := n in p (f n1)) -> p (f (let (n1, _) := n in n1)).
> intros p f n h. apply h.

intros p f n h. destruct n. apply h.

Or shorter:

intros p f (n1,n2) h. apply h.

Best regards,

Guillaume