在 Coq 中反转向量

Question

我正在尝试反转 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. auto.
Qed.

Theorem plus_n_O : forall n, plus n O = n.
Proof.
  induction n.
  - reflexivity.
  - simpl. rewrite IHn. reflexivity.
Qed.

Definition vreverse {T : Type} {n} (v : vect T n) : vect T n.
  induction v.
  - apply [[]].
  - rewrite <- plus_n_O. simpl. rewrite <- plus_n_S.
    apply (vappend IHv (t ::: [[]])).
  Show Proof.
Defined.

问题是，当我尝试计算该函数时，它会产生类似以下内容的结果：

match plus_n_O (S (S O)) in (_ = y) return (vect nat y) with
...

并且无法进一步。这里有什么问题？我怎样才能解决这个问题？

Answer 1

问题是您的函数使用不透明的证明，plus_n_S并且plus_n_O. 为了计算vreverse，你需要计算这些证明，如果它们是不透明的，计算将会被阻塞。

您可以通过透明地定义函数来解决此问题。就我个人而言，我不喜欢在执行此操作时使用证明模式，因为这样更容易看到发生了什么。（我在这里使用了向量的标准库定义。）

Require Import Coq.Vectors.Vector.
Import VectorNotations.

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

Fixpoint plus_n_S n m : n + S m = S (n + m) :=
  match n with
  | 0 => eq_refl
  | S n => f_equal S (plus_n_S n m)
  end.

Fixpoint plus_n_O n : n + 0 = n :=
  match n with
  | 0 => eq_refl
  | S n => f_equal S (plus_n_O n)
  end.

Fixpoint vreverse {T : Type} {n} (v : t T n) : t T n :=
  match v in t _ n return t T n with
  | [] => []
  | x :: v =>
    eq_rect _ (t T)
      (eq_rect _ (t T) (vappend (vreverse v) [x]) _ (plus_n_S _ 0))
              _ (f_equal S ( plus_n_O _))
  end.

Compute vreverse (1 :: 2 :: 3 :: []).