Proof of equality with destructuring let…in
-
04-11-2019 - |
Question
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.
No correct solution
Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange