Coqベクトルの置換

Question

Coqのベクトルの順列について、私は理由を考える必要があります。標準ライブラリには、リストの置換定義のみが含まれています。私の最初の試みとして、私はのようなベクターのためにそれを模倣しようとした：

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

私はすぐにもベクトルに対して証明する必要があり、既にリストに実績のある多くの順列補題があることに気づきました。それは多くの仕事である、と私は多分、私は次の補題を証明することにより、ショートカットを取ることができることを考えた：

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. 

それは限り、私はあることを示すことができるように私は、ベクトルの再利用リストの順列補題できるようになりますベクトルを対応するリストに変換することができます。

脇に：より理由が分かりやすいと思われるので、私はcoq-colorのライブラリからlist_of_vecの定義を使用しています。

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. 

この補題を証明するのは難解です。私は、誘導によってこれを実行しようとしました：

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

しかし、それは十分に一般的なものではなく、v1とv2に依存誘導hypotehsisで私の葉：私は上のアドバイスを聞いて喜んでいるでしょう

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

一般的なアプローチと私のそれの策定。

P.S.フル自己完結型の例：https://gist.github.com/vzaliva/c31300aa484ff6ad2089cb0c45c3828a

Answer 1

が、私はこれらの簡単な補題使用：

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. 

をし、一般の誘導は、いくつかのより多くの仮説：

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. 

警告を：私は簡素化しようとしませんでした証明またはJMeq_eq公理を取り除く。

Answer 2

ここでは、補題を使ってベクトルを破壊する公理のない解です。

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.