5
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ This seems weird... at the very least the migration should have been discussed, if only for consistency. $\endgroup$ – ejgallego Sep 12 '16 at 19:54
  • $\begingroup$ So who migrated this question and why? $\endgroup$ – Zimm i48 Sep 13 '16 at 11:24
  • $\begingroup$ @ejgallego Consensus appears to be that this kind of question is on-topic, here at Computer Science, and you'll notice that the question had been answered by somebody with reasonably high reputatation here (2.5k is peanuts on Stack Overflow but, on a smaller site like this, it puts you around the top 50 users). I'm not sure what you think is weird. $\endgroup$ – David Richerby Sep 14 '16 at 10:37
  • 1
    $\begingroup$ @DavidRicherby , Anton Tunov perfectly expressed the concern, but I can't seem to find his comment now. In short, the question is not about the CS/theory side of Coq, but more about the programming part; moreover, all the related questions about Coq currently live in SO, so this move seems to break "consistency", that is to say, if you want to place this question here you should also more +100 question IMHO. Regards! $\endgroup$ – ejgallego Sep 14 '16 at 12:54
  • $\begingroup$ I (personally) still think it's a technical question as opposed to something like this question on the functional extensionality axiom. $\endgroup$ – Anton Trunov Sep 15 '16 at 14:18
7
$\begingroup$

You can destruct not only on variables, but on expressions like f n as well. So, this will get you a solution:

Lemma foo : forall n, f n = (let (x, y) := f n in (x, y)).
  intro n.
  now destruct (f n).    (* or destruct (f n). reflexivity. *)
Qed.
| cite | improve this answer | |
$\endgroup$
5
$\begingroup$

You could also consider a more equational proof that will avoid/encapsulate the destruction:

Lemma foo n : f n = (let (x, y) := f n in (x, y)).
Proof. now rewrite (surjective_pairing (f n)). Qed.
| cite | improve this answer | |
$\endgroup$
  • 2
    $\begingroup$ Thanks. Just a comment for later readers: here n is an argument of the lemma so it can be used directly inside the proof instead of having to do intro n first as in my question and Anton Trunov's answer. $\endgroup$ – Bruno Le Floch Aug 8 '16 at 6:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy