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. 전체 자체에 포함 된 예 : 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.