Inverser un vecteur en Coq

Question

Je tente d'inverser un vecteur en Coq. Mon implémentation est la suivante :

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.

Le problème est que, lors de la tentative de calcul de la fonction, cela produit quelque chose comme :

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

et je ne peux pas aller plus loin. Quel est le problème ici ? Comment puis-je le corriger ?

Answer 1

Le problème est que vos fonctions utilisent des preuves opaques, plus_n_S et plus_n_O. Pour calculer vreverse, vous devez calculer ces preuves, et si elles sont opaques, le calcul sera bloqué.

Vous pouvez corriger ce problème en définissant les fonctions de manière transparente. Personnellement, je préfère ne pas utiliser le mode preuve lors de la réalisation de cela, car il est plus facile de voir ce qui se passe. (J'ai utilisé la définition de la bibliothèque standard des vecteurs ici.)

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