如何在Coq中证明以下引理？

Question

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

我花了很多时间在这上面。我从一个明智的目标开始，但最终总是有一个无法证明的目标。

这是我目前的做法：

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

在我的背景下，我现在有：

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

我的目标是：

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

有没有办法在IHx中推广x，以便我可以将它专门化为（a :: x）？由于我不知道这样做的正确策略，我尝试以下内容，并最终得到前面提到的不可能的目标。

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])

这个目标是不可能的，因为对于n = 0和rev x = h :: t，目标减少到[a] = List.hd (rev (h :: t)) ++ [a]。

这个引理实际上是不健全的，还是我只是缺少一些策略？

Answer 1

假设firstn和rev是我认为的那样，我不认为引理是真的。

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

但

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

基本上，rev (firstn n x)是n的第一个x元素（以相反的顺序），但firstn n (rev x)是n的最后x元素（也以相反的顺序）。为了使这个引理在任何一般性中都是正确的，你需要x才能拥有最多n元素。正如Arthur Azevedo De Amorim在评论中指出的那样，如果你插入一个skipn n来查看n的最后一个x（最多）元素，你也可以得到这个引理的正确版本。

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