小编luk*_*e36的帖子

我正在尝试反转 Coq 中的向量。我的实现如下：

Fixpoint vappend {T : Type} {n m} (v1 : vect T n) (v2 : vect T m)
  : vect T (plus n m) :=
  match v1 in vect _ n return vect T (plus n m) with
  | vnil => v2
  | x ::: v1' => x ::: (vappend v1' v2)
  end.

Theorem plus_n_S : forall n m, plus n (S m) = S (plus n m).
Proof.
  intros. induction n; auto.
  - simpl. rewrite <- IHn. …