Coq vector permutations

Question

I need to reason about vectors' permutations in Coq. The standard library only includes permutation definitions for lists. As my first attempt, I tried to mimic it for vectors as:

  Inductive VPermutation: forall n, vector A n -> vector A n -> Prop :=
  | vperm_nil: VPermutation 0 [] []
  | vperm_skip {n} x l l' : VPermutation n l l' -> VPermutation (S n) (x::l) (x::l')
  | vperm_swap {n} x y l : VPermutation (S (S n)) (y::x::l) (x::y::l)
  | vperm_trans {n} l l' l'' :
      VPermutation n l l' -> VPermutation n l' l'' -> VPermutation n l l''.

I quickly realized that there are many permutation lemmas, already proven on lists which needs to be also proven for vectors. It is a lot of work, and I thought that perhaps I can take a shortcut by proving the following lemma:

  Lemma ListVecPermutation {n} {l1 l2} {v1 v2}:
    l1 = list_of_vec v1 ->
    l2 = list_of_vec v2 ->
    Permutation l1 l2 ->
    VPermutation A n v1 v2.
  Proof.

It would allow me to re-use list permutation lemmas for vectors as long as I can show that vectors could be converted to corresponding lists.

Aside: I am using list_of_vec definition from coq-color library as it seems to be easier to reason about than VectorDef.to_list.

  Fixpoint list_of_vec n (v : vector A n) : list A :=
    match v with
      | Vnil => nil
      | Vcons x v => x :: list_of_vec v
    end.

Proving this lemma ended being tricky. I tried to do this by induction:

  Proof.
    intros H1 H2 P.
    revert H1 H2.
    dependent induction P.
    -
      intros H1 H2.
      dep_destruct v1; auto.
      dep_destruct v2; auto.
      inversion H1.
    -

But it leaves me with inductive hypotehsis which is not sufficiently generalized and depends on v1 and v2:

  IHP : l = list_of_vec v1 -> l' = list_of_vec v2 -> VPermutation A n v1 v2

I will be glad to hear suggestions on the approach in general and my formulation of it.

P.S. The full self-contained example: https://gist.github.com/vzaliva/c31300aa484ff6ad2089cb0c45c3828a

Answer 1

I used these simple lemmas:

Lemma list_of_vec_eq (A : Type) (n : nat) (v1 v2 : vector A n) :
  list_of_vec v1 = list_of_vec v2 -> v1 = v2.
Admitted.

Lemma list_of_vec_length {A : Type} {n : nat} {v : vector A n} :
  length (list_of_vec v) = n.
Admitted.

Lemma list_of_vec_vec_of_list {A : Type} {l : list A} :
  list_of_vec (vec_of_list l) = l.
Admitted.

and generalized the induction hypotheses some more:

Section VPermutation_properties.

  Require Import Sorting.Permutation.

  Variable A:Type.

  Lemma ListVecPermutation {n} {l1 l2} {v1 v2}:
    l1 = list_of_vec v1 ->
    l2 = list_of_vec v2 ->
    Permutation l1 l2 ->
    VPermutation A n v1 v2.
  Proof.
    intros H1 H2 P; revert n v1 v2 H1 H2.
    dependent induction P; intros n v1 v2 H1 H2.
    - dependent destruction v1; inversion H1; subst.
      dependent destruction v2; inversion H2; subst.
      apply vperm_nil.
    - dependent destruction v1; inversion H1; subst.
      dependent destruction v2; inversion H2; subst.
      apply vperm_skip.
      now apply IHP.
    - do 2 (dependent destruction v1; inversion H1; subst).
      do 2 (dependent destruction v2; inversion H2; subst).
      apply list_of_vec_eq in H5; subst.
      apply vperm_swap.
    - assert (n = length l').
      { pose proof (Permutation_length P1) as len.
        subst.
        now rewrite list_of_vec_length in len.
      }
      subst.
      apply vperm_trans with (l' := vec_of_list l').
      -- apply IHP1; auto.
         now rewrite list_of_vec_vec_of_list.
      -- apply IHP2; auto.
         now rewrite list_of_vec_vec_of_list.
  Qed.

End VPermutation_properties.

Caveat: I didn't try to simplify the proof or get rid of the JMeq_eq axiom.

Answer 2

Here is a solution without axioms, using auxiliary lemmas to destruct vectors.

Require Import Coq.Arith.Arith.
Require Export Coq.Vectors.Vector.

Arguments nil {_}.
Arguments cons {_} _ {_} _.

Section VPermutation.

  Variable A:Type.

  Inductive VPermutation: forall n, Vector.t A n -> Vector.t A n -> Prop :=
  | vperm_nil: VPermutation 0 nil nil
  | vperm_skip {n} x l l' : VPermutation n l l' -> VPermutation (S n) (cons x l) (cons x l')
  | vperm_swap {n} x y l : VPermutation (S (S n)) (cons y (cons x l)) (cons x (cons y l))
  | vperm_trans {n} l l' l'' :
      VPermutation n l l' -> VPermutation n l' l'' -> VPermutation n l l''.

End VPermutation.

Section VPermutation_properties.

  Require Import Sorting.Permutation.

  Context {A:Type}.

  Fixpoint list_of_vec {n} (v : Vector.t A n) : list A :=
    match v with
      | nil => List.nil
      | cons x v => x :: list_of_vec v
    end.

  Lemma inversion_aux : forall n (v:Vector.t A n),
    match n return Vector.t A n -> Prop with
    | 0 => fun v => v = nil
    | _ => fun v => exists x y, v = cons x y
    end v.
  Proof.
    intros. destruct v; repeat eexists; trivial.
  Qed.
  Lemma inversion_0 : forall (v:Vector.t A 0), v = nil.
  Proof.
    intros. apply (inversion_aux 0).
  Qed.
  Lemma inversion_Sn : forall {n} (v : Vector.t A (S n)),
    exists a b, v = cons a b.
  Proof.
    intros. apply (inversion_aux (S n)).
  Qed.

  Ltac vdestruct v :=
    match type of v with
    | Vector.t _ ?n => match n with
                       | 0 => pose proof (inversion_0 v); subst v
                       | S ?n' => let H := fresh in
                                  pose proof (inversion_Sn v) as H;
                                  destruct H as (?h & ?t & H); subst v
                       | _ => fail 2 n "is not of the form 0 or S n"
                       end
    | _ => fail 0 v "is not a vector"
    end.

  Lemma list_of_vec_inj : forall n (v1 v2 : Vector.t A n),
      list_of_vec v1 = list_of_vec v2 -> v1 = v2.
  Proof.
    induction n; intros.
    - vdestruct v1. vdestruct v2. reflexivity.
    - vdestruct v1. vdestruct v2. simpl in H. inversion H; subst.
      apply f_equal. apply IHn; assumption.
  Qed.

  Lemma list_of_vec_surj : forall l,
    exists v : Vector.t A (length l), l = list_of_vec v.
  Proof.
    intros. induction l; intros.
    - exists nil. reflexivity.
    - destruct IHl as (v & IHl).
      exists (cons a v). simpl. apply f_equal. assumption.
  Qed.

  Lemma list_of_vec_length {n} (v:Vector.t A n) :
    List.length (list_of_vec v) = n.
  Proof.
    induction v.
    - reflexivity.
    - simpl. apply f_equal. assumption.
  Qed.

  Lemma ListVecPermutation {n} {l1 l2} {v1 v2}:
    l1 = list_of_vec v1 ->
    l2 = list_of_vec v2 ->
    Permutation l1 l2 ->
    VPermutation A n v1 v2.
  Proof.
    intros H1 H2 P.
    revert n v1 v2 H1 H2.
    induction P; intros.
    - destruct v1; [|discriminate].
      vdestruct v2. constructor.
    - destruct v1; [discriminate|]. vdestruct v2. simpl in H1, H2.
      inversion H1; subst. inversion H2; subst.
      apply vperm_skip. apply IHP; reflexivity.
    - destruct v1; [discriminate|]. destruct v1; [discriminate|].
      vdestruct v2. vdestruct t.
      simpl in H1, H2. inversion H1; subst. inversion H2; subst.
      apply list_of_vec_inj in H4. subst.
      apply vperm_swap.
    - pose proof (list_of_vec_surj l').
      rewrite <- (Permutation_length P1) in H.
      rewrite H1 in H.
      rewrite list_of_vec_length in H.
      destruct H as (v & H).
      eapply vperm_trans. apply IHP1; eassumption.
      apply IHP2; assumption.
  Qed.

End VPermutation_properties.