如何在 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) 是x 的第一个n 元素（倒序），但firstn n (rev x) 是x 的最后一个n 元素（也倒序）。要使这个引理在任何一般性中成立，您将需要 x 最多具有 n 元素。正如 Arthur Azevedo De Amorim 在 cmets 中指出的那样，如果您插入 skipn n 以查看 x 的最后一个 n（最多）元素，您也可以获得此引理的正确版本。

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