I have some expression (
f n in the example below) returning a tuple. I would like to prove that
f n is equal to
let (x, y) := f n in (x, y), which seems like it should be easy. What tactic should I use?
Definition f (n : nat) : nat * nat := match n with | 0 => (3, 4) | _ => (2, 3) end. Lemma foo : forall n, f n = (let (x, y) := f n in (x, y)). auto. (*doesn't do anything*) destruct n. auto. auto. Qed.
The same task with
let tup := f n in tup can be done with the tactic
trivial. The same task with both
f n replaced by an explicit tuple
(f n, 12) is also covered by
trivial. Here I had to
destruct n (or do a pointless
induction n) to make the "tupleness" of
f n be manifest.