How do I prove the following lemma in Coq?

Question

Lemma rev_firstn : forall (x : list bool) (n : nat),
rev (firstn n x) = firstn n (rev x).

I have spent quite a bit of time on this. I start out with a sensible goal but always end up with a goal that is impossible to prove.

Here is my current approach:

Proof.
  intros. generalize dependent x. induction n. 
  + easy. 
  + induction x.
    - easy. 
    -

In my context, I now have:

IHn : forall x : list bool, rev (firstn n x) = firstn n (rev x)
IHx : rev (firstn (S n) x) = firstn (S n) (rev x)

and my goal is:

rev (firstn (S n) (a :: x)) = firstn (S n) (rev (a :: x))

Is there a way to generalize x in IHx so that I can specialize it to (a :: x)? Since I don't know the right tactic to do this, I try the following, and end up with the previously mentioned impossible goal.

Proof.
  intros. generalize dependent x. induction n. 
  + easy. 
  + induction x.
    - easy. 
    - assert (rev_cons : forall (b : bool) (l : list bool), 
              rev (b :: l) = rev l ++ [b]).
      { easy. } rewrite firstn_cons. 
      rewrite rev_cons. rewrite rev_cons. specialize (@IHn x).
      rewrite IHn.
Goal: firstn n (rev x) ++ [a] = firstn (S n) (rev x ++ [a])

This goal is impossible because for n = 0 and rev x = h :: t, the goal reduces to [a] = List.hd (rev (h :: t)) ++ [a].

Is this lemma actually unsound, or am I just missing some tactics?

SCappella SCappella · Accepted Answer · 2019-04-03T21:40:32

Assuming firstn and rev are what I think they are, I don't think the lemma is true.

rev (firstn 2 [true, false, false])
= rev [true, false]
= [false, true]

but

firstn 2 (rev [true, false, false])
= firstn 2 [false, false, true]
= [false, false]

Essentially, rev (firstn n x) is the first n elements of x (in reverse order), but firstn n (rev x) is the last n elements of x (also in reverse order). For this lemma to be true in any sort of generality, you would need x to have at most n elements. As Arthur Azevedo De Amorim notes in the comments, you can also get a correct version of this lemma if you insert a skipn n to just look at the last n (at most) elements of x.

rev (firstn n (skipn (length x - n)) x) = firstn n (rev x)

How do I prove the following lemma in Coq?

1 Answers