COQ向量：Shiftin，ShiftOut和Last

Question

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

首先证明了辅助引理，可以证明这一引理可以简单地证明。具体来说，如果我们知道

shiftin (last t0) (shiftout t0) = t0

，那么其余的很快就会随之而来。证明辅助引理需要一个技巧：

From Coq Require Import Vector.

Lemma vec_shiftin_eq' A n (t0 : t A n) :
  match n as n' return t A n' -> Prop with 0 => fun _ => True | S nn =>
      fun t0 => shiftin (last t0) (shiftout t0) = t0 end t0.
Proof.
  induction t0 as [|el1 n t0' IH]; [easy|].
  destruct t0' as [|el2 n t0']; [easy|].
  simpl in IH|-*. rewrite IH. easy.
Qed.

Lemma vec_shiftin_eq A n (t0 t1 : t A (S n)) :
    t0 = t1 <-> shiftin (last t0) (shiftout t0) = shiftin (last t1) (shiftout t1).
Proof. now rewrite !(vec_shiftin_eq' A (S n)). Qed.

Print Assumptions vec_shiftin_eq.
(* Closed under the global context *)

Answer 1

我们希望通过归纳对向量证明我们的助手引理。但是，对向量的归纳始终要求

n

表示其长度不受限制，即它是一个自由变量。进行归纳，

S n

是行不通的。为了解决这个问题，我们被迫将归纳声明概括为对所有人有效的事物，这需要说出应该在

n

中持有的内容。我们说，在

n=0

，即

n=0

。这样，诱导就没有缠绕。