Reversing a vector in Coq

user_6794730 0
Viewed 79

I am trying to reverse a vector in Coq. My implementation is as follows:

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.

The problem is, when I try to compute the function, it produces something like:

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

and couldn't get further. What's the problem here? How can I fix this?

coq
1 Answers

The problem is that your functions use opaque proofs, plus_n_S and plus_n_O. To compute vreverse, you need to compute these proofs, and if they are opaque, the computation will be blocked.

You can fix this issue by defining the functions transparently. Personally, I prefer not to use proof mode when doing this, since it is easier to see what is going on. (I have used the standard library definition of vectors here.)

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 :: []).
user_16337700
Related