Перестановки векторов Coq

Мне нужно рассуждать о перестановках векторов в 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.

Это позволило бы мне повторно использовать леммы перестановки списков для векторов, пока я могу показать, что векторы могут быть преобразованы в соответствующие списки.

Кроме того: я использую определение list_of_vec из библиотеки coq-color, поскольку его легче рассуждать, чем 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.
    -

Но это оставляет меня с индуктивной гипотезой, которая недостаточно обобщена и зависит от 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


list vector permutation induction coq
person krokodil    schedule 20.10.2017    source источник
comment
Для перестановок вам лучше работать с библиотеками seq и tuple, доступными в math-comp.   -  person ejgallego    schedule 20.10.2017

Ответы (2)


arrow_upward
3
arrow_downward

Я использовал эти простые леммы:

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.

person Anton Trunov    schedule 21.10.2017

arrow_upward
2
arrow_downward

Вот решение без аксиом, использующее вспомогательные леммы для разрушения векторов.

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.
person eponier    schedule 25.10.2017