关于Coq.Vectors库shiftin与last-shiftout逆性的证明求助

我正在进行一项Coq验证任务，需大量使用标准向量库Coq.Vectors。该库包含诸多实用定义，但缺少我所需的部分性质证明。我需要对向量的最后一个元素进行操作，认为非空向量上shiftin与last-shiftout构成逆操作，但无法证明如下引理：

From Coq Require Import Vector.

Lemma shiftin_last_shiftout:
  forall A (n:nat) (x: t A (S n)),
  x = shiftin (last x) (shiftout x).

证明方案 #

要完成这个引理的证明，核心是对向量的结构进行归纳，结合Vector库的基础定义与性质：

• 关键定义回顾：
  • shiftout：移除非空向量的最后一个元素，返回长度为n的向量
  • last：获取非空向量的最后一个元素
  • shiftin：在向量末尾追加一个元素

具体证明代码如下：

From Coq Require Import Vector.

Lemma shiftin_last_shiftout:
  forall A (n:nat) (x: t A (S n)),
  x = shiftin (last x) (shiftout x).
Proof.
  intros A n x.
  induction x as [|n' h t IH].
  - (* 单元素向量基础情况 *)
    simpl. reflexivity.
  - (* 多元素向量归纳步骤 *)
    simpl. f_equal. apply IH.
Qed.

证明说明 #

• 基础情况：当向量是单元素[h]时，shiftout返回空向量，last取到h，shiftin将h追加到空向量末尾，结果与原向量完全一致，用reflexivity直接完成。
• 归纳步骤：对于长度为S (S n')的向量h :: t，化简等式后只需证明子向量t满足归纳假设，直接调用归纳假设IH即可完成证明。

内容的提问来源于stack exchange，提问作者KingsAlpaca