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定义，因为它似乎比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. 

证明这个引理结束了棘手。我试图通过感应来做到这一点：

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

但它给我留下了感性hypotehsis这是不足够广义的，取决于v1和v2：

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.