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

但这给我留下了归纳假设，它没有被充分概括并且取决于 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.

Coq 向量排列

Coq vector permutations

list

vector

permutation

coq

induction