Permutations de vecteur Coq

Question

J'ai besoin de raisonner sur les permutations de vecteurs dans Coq. La bibliothèque standard inclut uniquement des définitions de permutation pour les listes. Comme ma première tentative, j'ai essayé de l'imiter pour les vecteurs comme:

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''. 

Je suis vite rendu compte qu'il ya beaucoup de lemmes de permutation, déjà fait leurs preuves sur les listes qui doit être aussi éprouvée pour les vecteurs. Il est beaucoup de travail, et je pensais que peut-être que je peux prendre un raccourci en prouvant le lemme suivant:

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. 

Il me permettrait de réutiliser lemmes de permutation de liste pour des vecteurs aussi longtemps que je peux montrer que les vecteurs pourraient être convertis en listes correspondantes.

À côté: J'utilise la définition list_of_vec de la bibliothèque coq-color car il semble être plus facile à raisonner que 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. 

En supposant que ce lemme soit terminé, il est difficile de le faire. J'ai essayé de le faire par 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. 
    - 

Mais il me laisse avec hypotehsis inductive qui est pas suffisamment généralisé et dépend de v1 et v2:

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

Je serai heureux d'entendre des suggestions sur la approche en général et ma formulation de celui-ci.

P.S. L'exemple autonome complet: https://gist.github.com/vzaliva/c31300aa484ff6ad2089cb0c45c3828a

Answer 1

J'utilisé ces simples lemmes:

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. 

et généralisé l'induction des hypothèses un peu plus:

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: Je n'ai pas essayé de simplifier la preuve ou se débarrasser de l'axiome JMeq_eq.

Answer 2

Voici une solution sans axiomes, utilisant des lemmes auxiliaires pour détruire les vecteurs.

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.