(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

(* Require Import Arith Omega Max List. *)

Require Import Arith Omega List Permutation.
Require Import utils pos.

Set Implicit Arguments.

Section vector.

  Variable X : Type.

  Inductive vec : nat -> Type :=
    | vec_nil  : vec 0
    | vec_cons : forall n, X -> vec n -> vec (S n).

  Let vec_decomp_type n := 
    match n with
      | 0   => Prop
      | S n => (X * vec n)%type
    end.

  Definition vec_decomp n (v : vec n) :=
    match v in vec k return vec_decomp_type k with
      | vec_nil  => False
      | @vec_cons n x v => (x,v)
    end.
    
  Definition vec_head n (v : vec (S n)) := match v with @vec_cons _ x _ => x end.
  Definition vec_tail n (v : vec (S n)) := match v with @vec_cons _ _ w => w end.

  Let vec_head_tail_type n : vec n -> Prop := 
    match n with
      | 0   => fun v => v = vec_nil
      | S n => fun v => v = vec_cons (vec_head v) (vec_tail v)
    end.

  Let vec_head_tail_prop n v :  @vec_head_tail_type n v.
(* Goal: forall _ : @eq nat (@vec_sum n v) O, @eq (vec nat n) v (@vec_zero n) *)
  Proof. induction v; simpl; auto. Qed.

  Fact vec_0_nil (v : vec 0) : v = vec_nil.
  Proof. apply (vec_head_tail_prop v). Qed.

  Fact vec_head_tail n (v : vec (S n)) : v = vec_cons (vec_head v) (vec_tail v).
  Proof. apply (vec_head_tail_prop v). Qed.

  Fixpoint vec_pos n (v : vec n) : pos n -> X.
  Proof.
    refine (match v with
      | vec_nil => fun p => _
      | @vec_cons n x v => fun p => _
    end); invert pos p.
(* Goal: X *)
(* Goal: X *)
    exact x.
(* Goal: X *)
    exact (vec_pos _ v p).
  Defined.

  Fact vec_pos0 n (v : vec (S n)) : vec_pos v pos0 = vec_head v.
  Proof. 
(* Goal: @eq X (@vec_pos (S n) v (@pos_fst n)) (@vec_head n v) *)
    rewrite (vec_head_tail v).
(* Goal: @eq X (@vec_pos (S n) (@vec_cons n (@vec_head n v) (@vec_tail n v)) (@pos_fst n)) (@vec_head n (@vec_cons n (@vec_head n v) (@vec_tail n v))) *)
    reflexivity.
  Qed.
  
  Fact vec_pos_tail n (v : vec (S n)) p : vec_pos (vec_tail v) p = vec_pos v (pos_nxt p).
  Proof.
(* Goal: @eq X (@vec_pos n (@vec_tail n v) p) (@vec_pos (S n) v (@pos_nxt n p)) *)
    rewrite vec_head_tail at 2; simpl; auto.
  Qed.
  
  Fact vec_pos1 n (v : vec (S (S n))) : vec_pos v pos1 = vec_head (vec_tail v).
  Proof.
(* Goal: @eq X (@vec_pos (S (S n)) v (@pos_nxt (S n) (@pos_fst n))) (@vec_head n (@vec_tail (S n) v)) *)
    rewrite <- vec_pos0, vec_pos_tail; auto.
  Qed.

  Fact vec_pos_ext n (v w : vec n) : (forall p, vec_pos v p = vec_pos w p) -> v = w.
  Proof.
(* Goal: forall _ : forall p : pos n, @eq X (@vec_pos n v p) (@vec_pos n w p), @eq (vec n) v w *)
    revert v w; induction n as [ | n IHn ]; intros v w H.
(* Goal: @eq (vec O) v w *)
(* Goal: @eq (vec (S n)) v w *)
    rewrite (vec_0_nil v), (vec_0_nil w); auto.
(* Goal: @eq (vec (S n)) v w *)
    revert H; rewrite (vec_head_tail v), (vec_head_tail w); f_equal.
(* Goal: forall _ : forall p : pos (S n), @eq X (@vec_pos (S n) (@vec_cons n (@vec_head n v) (@vec_tail n v)) p) (@vec_pos (S n) (@vec_cons n (@vec_head n w) (@vec_tail n w)) p), @eq (vec (S n)) (@vec_cons n (@vec_head n v) (@vec_tail n v)) (@vec_cons n (@vec_head n w) (@vec_tail n w)) *)
    intros H; f_equal.
(* Goal: @eq X (@vec_head n v) (@vec_head n w) *)
(* Goal: @eq (vec n) (@vec_tail n v) (@vec_tail n w) *)
    apply (H pos0).
(* Goal: @eq X (@vec_pos (S n) (@vec_set_pos (S n) g) (@pos_nxt n p)) (g (@pos_nxt n p)) *)
    apply IHn.
(* Goal: forall p : pos n, @eq X (@vec_pos n (@vec_tail n v) p) (@vec_pos n (@vec_tail n w) p) *)
    intros p; apply (H (pos_nxt p)).
  Qed.

  Fixpoint vec_set_pos n : (pos n -> X) -> vec n :=
    match n return (pos n -> X) -> vec n with 
      | 0   => fun _ => vec_nil
      | S n => fun g => vec_cons (g pos0) (vec_set_pos (fun p => g (pos_nxt p)))
    end.

  Fact vec_pos_set n (g : pos n -> X) p : vec_pos (vec_set_pos g) p = g p. 
  Proof.
(* Goal: @eq X (@vec_pos n (@vec_set_pos n g) p) (g p) *)
    revert g p; induction n as [ | n IHn ]; intros g p; pos_inv p; auto.
(* Goal: @eq X (@vec_pos (S n) (@vec_set_pos (S n) g) (@pos_nxt n p)) (g (@pos_nxt n p)) *)
    apply IHn.
  Qed.

  Fixpoint vec_change n (v : vec n) : pos n -> X -> vec n.
  Proof.
    refine (match v with
      | vec_nil         => fun _ _ => vec_nil
      | @vec_cons n y v => fun p x => _
    end).
(* Goal: @eq nat (@vec_sum (S n) (@vec_one (S n) p)) (S O) *)
    pos_inv p.
(* Goal: vec (S n) *)
(* Goal: vec (S n) *)
    exact (vec_cons x v).
(* Goal: vec (S n) *)
    apply (vec_cons y), (vec_change _ v p x).
  Defined.

  Fact vec_change_eq n v p q x : p = q -> vec_pos (@vec_change n v p x) q = x.
  Proof. 
(* Goal: forall _ : @eq (pos n) p q, @eq X (@vec_pos n (@vec_change n v p x) q) x *)
    intro; subst q; revert p x.
(* Goal: forall (p : pos n) (x : X), @eq X (@vec_pos n (@vec_change n v p x) p) x *)
    induction v; intros p ?; invert pos p; auto.
  Qed.

  Fact vec_change_neq n v p q x : p <> q -> vec_pos (@vec_change n v p x) q = vec_pos v q.
  Proof. 
(* Goal: forall _ : not (@eq (pos n) p q), @eq X (@vec_pos n (@vec_change n v p x) q) (@vec_pos n v q) *)
    revert p q x.
(* Goal: forall (p q : pos n) (x : X) (_ : not (@eq (pos n) p q)), @eq X (@vec_pos n (@vec_change n v p x) q) (@vec_pos n v q) *)
    induction v as [ | n y v IH ]; intros p q x H; invert pos p; invert pos q; auto.
(* Goal: @eq nat (S O) O *)
    destruct H; auto.
(* Goal: @eq X (@vec_pos n (@vec_change n v p x) q) (@vec_pos n v q) *)
    apply IH; contradict H; subst; auto.
  Qed.

  Fact vec_change_idem n v p x y : vec_change (@vec_change n v p x) p y = vec_change v p y.
  Proof.
(* Goal: @eq (vec n) (@vec_change n v p (@vec_pos n v p)) v *)
    apply vec_pos_ext; intros q.
(* Goal: @eq X (@vec_pos n (@vec_change n v p (@vec_pos n v p)) q) (@vec_pos n v q) *)
    destruct (pos_eq_dec p q).
(* Goal: @eq X (@vec_pos n (@vec_change n (@vec_change n v p x) p y) q) (@vec_pos n (@vec_change n v p y) q) *)
(* Goal: @eq X (@vec_pos n (@vec_change n (@vec_change n v p x) p y) q) (@vec_pos n (@vec_change n v p y) q) *)
    repeat rewrite vec_change_eq; auto.
(* Goal: @eq X (@vec_pos n (@vec_change n v p (@vec_pos n v p)) q) (@vec_pos n v q) *)
    repeat rewrite vec_change_neq; auto.
  Qed.

  Fact vec_change_same n v p : @vec_change n v p (vec_pos v p) = v.
  Proof.
(* Goal: @eq (vec n) (@vec_change n v p (@vec_pos n v p)) v *)
    apply vec_pos_ext; intros q.
(* Goal: @eq X (@vec_pos n (@vec_change n v p (@vec_pos n v p)) q) (@vec_pos n v q) *)
    destruct (pos_eq_dec p q).
(* Goal: @eq X (@vec_pos n (@vec_change n v p (@vec_pos n v p)) q) (@vec_pos n v q) *)
(* Goal: @eq X (@vec_pos n (@vec_change n v p (@vec_pos n v p)) q) (@vec_pos n v q) *)
    repeat rewrite vec_change_eq; subst; auto.
(* Goal: @eq X (@vec_pos n (@vec_change n v p (@vec_pos n v p)) q) (@vec_pos n v q) *)
    repeat rewrite vec_change_neq; auto.
  Qed.

  Variable eq_X_dec : forall x y : X, { x = y } + { x <> y }.

  Fixpoint vec_eq_dec n (u v : vec n) : { u = v } + { u <> v }.
  Proof.
(* Goal: sumbool (@eq (vec n) u v) (not (@eq (vec n) u v)) *)
    destruct u as [ | n x u ].
(* Goal: sumbool (@eq (vec O) vec_nil v) (not (@eq (vec O) vec_nil v)) *)
(* Goal: sumbool (@eq (vec (S n)) (@vec_cons n x u) v) (not (@eq (vec (S n)) (@vec_cons n x u) v)) *)
    left.
(* Goal: @eq (vec O) vec_nil v *)
(* Goal: sumbool (@eq (vec (S n)) (@vec_cons n x u) v) (not (@eq (vec (S n)) (@vec_cons n x u) v)) *)
    rewrite vec_0_nil; trivial.
(* Goal: sumbool (@eq (vec (S n)) (@vec_cons n x u) v) (not (@eq (vec (S n)) (@vec_cons n x u) v)) *)
    destruct (eq_X_dec x (vec_head v)) as [ E1 | D ].
(* Goal: sumbool (@eq (vec (S n)) (@vec_cons n x u) v) (not (@eq (vec (S n)) (@vec_cons n x u) v)) *)
(* Goal: sumbool (@eq (vec (S n)) (@vec_cons n x u) v) (not (@eq (vec (S n)) (@vec_cons n x u) v)) *)
    destruct (vec_eq_dec _ u (vec_tail v)) as [ E2 | D ].
(* Goal: sumbool (@eq (vec (S n)) (@vec_cons n x u) v) (not (@eq (vec (S n)) (@vec_cons n x u) v)) *)
(* Goal: sumbool (@eq (vec (S n)) (@vec_cons n x u) v) (not (@eq (vec (S n)) (@vec_cons n x u) v)) *)
(* Goal: sumbool (@eq (vec (S n)) (@vec_cons n x u) v) (not (@eq (vec (S n)) (@vec_cons n x u) v)) *)
    left; subst; rewrite <- vec_head_tail; auto.
(* Goal: sumbool (@eq (vec (S n)) (@vec_cons n x u) v) (not (@eq (vec (S n)) (@vec_cons n x u) v)) *)
(* Goal: sumbool (@eq (vec (S n)) (@vec_cons n x u) v) (not (@eq (vec (S n)) (@vec_cons n x u) v)) *)
    right; contradict D; subst; rewrite <- D; auto.
(* Goal: sumbool (@eq (vec (S n)) (@vec_cons n x u) v) (not (@eq (vec (S n)) (@vec_cons n x u) v)) *)
    right; contradict D; subst; auto.
  Defined.
  
  Fixpoint vec_list n (v : vec n) := 
    match v with  
      | vec_nil      => nil
      | vec_cons x v => x::vec_list v
    end.
    
  Fact vec_list_length n v : length (@vec_list n v) = n.
  Proof. induction v; simpl; f_equal; auto. Qed.

  Fact vec_list_inv n v x : In x (@vec_list n v) -> exists p, x = vec_pos v p.
  Proof.
(* Goal: forall _ : @In X x (@vec_list n v), @ex (pos n) (fun p : pos n => @eq X x (@vec_pos n v p)) *)
    induction v as [ | n y v IHl ].
(* Goal: forall _ : @eq (pos n) p q, @eq nat (@vec_pos nat n (vec_one p) q) (S O) *)
    intros [].
(* Goal: forall _ : @In X x (@vec_list (S n) (@vec_cons n y v)), @ex (pos (S n)) (fun p : pos (S n) => @eq X x (@vec_pos (S n) (@vec_cons n y v) p)) *)
    intros [ H | H ]; subst.
(* Goal: @ex (pos (S n)) (fun p : pos (S n) => @eq X x (@vec_pos (S n) (@vec_cons n x v) p)) *)
(* Goal: @ex (pos (S n)) (fun p : pos (S n) => @eq X x (@vec_pos (S n) (@vec_cons n y v) p)) *)
    exists pos0; auto.
(* Goal: @ex (pos (S n)) (fun p : pos (S n) => @eq X x (@vec_pos (S n) (@vec_cons n y v) p)) *)
    destruct IHl as (p & Hp); auto.
(* Goal: @ex (pos (S n)) (fun p : pos (S n) => @eq X x (@vec_pos (S n) (@vec_cons n y v) p)) *)
    subst; exists (pos_nxt p); auto.
  Qed.

End vector.

(* notations *)

Arguments vec_nil { X }.

Infix "##" := vec_cons (at level 60, right associativity).

Section vec_app_split.

  Variable (X : Type) (n m : nat).

  Definition vec_app (v : vec X n) (w : vec X m) : vec X (n+m).
  Proof. 
(* Goal: vec X (Init.Nat.add n m) *)
    apply vec_set_pos; intros p.
(* Goal: X *)
    destruct (pos_both _ _ p) as [ q | q ]; refine (vec_pos _ q); assumption.
  Defined.

  Definition vec_split (v : vec X (n+m)) : vec X n * vec X m.
  Proof.
(* Goal: prod (vec X n) (vec X m) *)
    split; apply vec_set_pos; intros p; refine (vec_pos v _).
    + apply pos_left, p.
    + apply pos_right, p.
  Defined.

  Fact vec_app_split u : let (v,w) := vec_split u in vec_app v w = u.
  Proof.
(* Goal: let (v, w) := vec_split u in @eq (vec X (Init.Nat.add n m)) (vec_app v w) u *)
    case_eq (vec_split u); intros v w; unfold vec_split, vec_app; intros H.
(* Goal: @eq (vec X (Init.Nat.add n m)) (@vec_set_pos X (Init.Nat.add n m) (fun p : pos (Init.Nat.add n m) => match pos_both n m p with | inl q => @vec_pos X n v q | inr q => @vec_pos X m w q end)) u *)
    injection H; clear H; intros Hw Hv.
(* Goal: @eq (vec X (Init.Nat.add n m)) (@vec_set_pos X (Init.Nat.add n m) (fun p : pos (Init.Nat.add n m) => match pos_both n m p with | inl q => @vec_pos X n v q | inr q => @vec_pos X m w q end)) u *)
    apply vec_pos_ext; unfold vec_app; simpl.
(* Goal: forall p : pos (Init.Nat.add n m), @eq X (@vec_pos X (Init.Nat.add n m) (@vec_set_pos X (Init.Nat.add n m) (fun p0 : pos (Init.Nat.add n m) => match pos_both n m p0 with | inl q => @vec_pos X n v q | inr q => @vec_pos X m w q end)) p) (@vec_pos X (Init.Nat.add n m) u p) *)
    intros p; rewrite vec_pos_set. 
(* Goal: @eq X match pos_both n m p with | inl q => @vec_pos X n v q | inr q => @vec_pos X m w q end (@vec_pos X (Init.Nat.add n m) u p) *)
    case_eq (pos_both n m p); intros q Hq.
    + rewrite <- Hv, vec_pos_set; f_equal.
(* Goal: @eq (pos (Init.Nat.add n m)) (@pos_right n m q) p *)
      apply f_equal with (f := @pos_lr _ _) in Hq.
(* Goal: @eq (pos (Init.Nat.add n m)) (@pos_right n m q) p *)
      simpl in Hq; rewrite <- Hq; apply pos_lr_both.
    + rewrite <- Hw, vec_pos_set; f_equal.
(* Goal: @eq (pos (Init.Nat.add n m)) (@pos_right n m q) p *)
      apply f_equal with (f := @pos_lr _ _) in Hq.
(* Goal: @eq (pos (Init.Nat.add n m)) (@pos_right n m q) p *)
      simpl in Hq; rewrite <- Hq; apply pos_lr_both.
  Qed.

  Fact vec_split_app v w : vec_split (vec_app v w) = (v,w).
  Proof.
(* Goal: @eq (prod (vec X n) (vec X m)) (vec_split (vec_app v w)) (@pair (vec X n) (vec X m) v w) *)
    unfold vec_split, vec_app; f_equal; apply vec_pos_ext; intros p; repeat rewrite vec_pos_set.
    + rewrite pos_both_left; auto.
    + rewrite pos_both_right; auto.
  Qed.

  Fact vec_pos_app_left v w i : vec_pos (vec_app v w) (pos_left _ i) = vec_pos v i.
  Proof. unfold vec_app; rewrite vec_pos_set, pos_both_left; auto. Qed.

  Fact vec_pos_app_right v w i : vec_pos (vec_app v w) (pos_right _ i) = vec_pos w i.
  Proof. unfold vec_app; rewrite vec_pos_set, pos_both_right; auto. Qed.

End vec_app_split.

Fact vec_app_nil X n v : @vec_app X 0 n vec_nil v = v.
Proof.
(* Goal: @eq (vec X (Init.Nat.add O n)) (@vec_app X O n (@vec_nil X) v) v *)
  apply vec_pos_ext; unfold vec_app; simpl; intros p.
(* Goal: @eq X (@vec_pos X n (@vec_set_pos X n (fun p : pos n => @vec_pos X n v p)) p) (@vec_pos X n v p) *)
  rewrite vec_pos_set; auto.
Qed.

Fact vec_app_cons X n m x v w : @vec_app X (S n) m (x##v) w = x##vec_app v w.
Proof.
(* Goal: @eq (vec X (Init.Nat.add (S n) m)) (@vec_app X (S n) m (@vec_cons X n x v) w) (@vec_cons X (Init.Nat.add n m) x (@vec_app X n m v w)) *)
  apply vec_pos_ext; unfold vec_app; intros p.
(* Goal: @eq X (@vec_pos X (Init.Nat.add (S n) m) (@vec_set_pos X (Init.Nat.add (S n) m) (fun p : pos (Init.Nat.add (S n) m) => match pos_both (S n) m p with | inl q => @vec_pos X (S n) (@vec_cons X n x v) q | inr q => @vec_pos X m w q end)) p) (@vec_pos X (Init.Nat.add (S n) m) (@vec_cons X (Init.Nat.add n m) x (@vec_set_pos X (Init.Nat.add n m) (fun p : pos (Init.Nat.add n m) => match pos_both n m p with | inl q => @vec_pos X n v q | inr q => @vec_pos X m w q end))) p) *)
  rewrite vec_pos_set; simpl in p.
(* Goal: @eq X match pos_both (S n) m p with | inl q => @vec_pos X (S n) (@vec_cons X n x v) q | inr q => @vec_pos X m w q end (@vec_pos X (Init.Nat.add (S n) m) (@vec_cons X (Init.Nat.add n m) x (@vec_set_pos X (Init.Nat.add n m) (fun p : pos (Init.Nat.add n m) => match pos_both n m p with | inl q => @vec_pos X n v q | inr q => @vec_pos X m w q end))) p) *)
  analyse pos p.
  + simpl; auto.
  + simpl vec_pos at 3; rewrite vec_pos_set.
(* Goal: @eq X match pos_both (S n) m (@pos_nxt (Init.Nat.add n m) p) with | inl q => @vec_pos X (S n) (@vec_cons X n x v) q | inr q => @vec_pos X m w q end match pos_both n m p with | inl q => @vec_pos X n v q | inr q => @vec_pos X m w q end *)
    simpl pos_both.
(* Goal: @eq X match match pos_both n m p with | inl a => @inl (pos (S n)) (pos m) (@pos_nxt n a) | inr b => @inr (pos (S n)) (pos m) b end with | inl q => @vec_pos X (S n) (@vec_cons X n x v) q | inr q => @vec_pos X m w q end match pos_both n m p with | inl q => @vec_pos X n v q | inr q => @vec_pos X m w q end *)
    destruct (pos_both n m p); auto.
Qed.

Section vec_map.

  Variable (X Y : Type) (f : X -> Y). 

  Fixpoint vec_map n (v : vec X n) :=
    match v with 
      | vec_nil => vec_nil
      | x ## v  => f x ## vec_map v 
    end.

End vec_map.

Section vec_map2.

  (* Definitions taken from stdlib *)
  
  Definition case0 {A} (P:vec A 0 -> Type) (H:P (@vec_nil A)) v:P v :=
    match v with
    |vec_nil => H
    |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
    end.

  Definition caseS' {A} {n : nat} (v : vec A (S n)) : forall (P : vec A (S n) -> Type)
                                                      (H : forall h t, P (h ## t)), P v :=
    match v with
    | h ## t => fun P H => H h t
    | _ => fun devil => False_rect (@IDProp) devil
    end.

  Definition rect2 {A B} (P:forall {n}, vec A n -> vec B n -> Type)
             (bas : P vec_nil vec_nil) (recvec : forall {n v1 v2}, P v1 v2 ->
                                                              forall a b, P (a ## v1) (b ## v2)) :=
    fix rect2_fix {n} (v1 : vec A n) : forall v2 : vec B n, P v1 v2 :=
      match v1 with
      | vec_nil => fun v2 => case0 _ bas v2
      | @vec_cons _ n' h1 t1 => fun v2 =>
                                 caseS' v2 (fun v2' => P (h1##t1) v2') (fun h2 t2 => recvec (rect2_fix t1 t2) h1 h2)
      end.

  Definition vec_map2 {A B C} (g:A -> B -> C) :
    forall (n : nat), vec A n -> vec B n -> vec C n :=
    @rect2 _ _ (fun n _ _ => vec C n) (@vec_nil C) (fun _ _ _ H a b => (g a b) ## H).
  Global Arguments vec_map2 {A B C} g {n} v1 v2.

End vec_map2.

Fact vec_pos_map X Y (f : X -> Y) n (v : vec X n) p : vec_pos (vec_map f v) p = f (vec_pos v p).
Proof.
(* Goal: @eq nat (if @pos_eq_dec (S n) (@pos_nxt n p) (@pos_fst n) then S O else O) (@vec_pos nat (S n) (@vec_cons nat n O (@vec_set_pos nat n (fun q : pos n => if @pos_eq_dec n p q then S O else O))) (@pos_fst n)) *)
(* Goal: @eq nat (if @pos_eq_dec (S n) (@pos_nxt n p) (@pos_nxt n q) then S O else O) (@vec_pos nat (S n) (@vec_cons nat n O (@vec_set_pos nat n (fun q : pos n => if @pos_eq_dec n p q then S O else O))) (@pos_nxt n q)) *)
  revert p; induction v; intros p; pos_inv p; simpl; auto.
Qed.

  
Section vec_plus.

  Variable n : nat.

  Definition vec_plus (v w : vec nat n) := vec_set_pos (fun p => vec_pos v p + vec_pos w p).
  Definition vec_zero : vec nat n := vec_set_pos (fun _ => 0).
  
  Fact vec_pos_plus v w p : vec_pos (vec_plus v w) p = vec_pos v p + vec_pos w p.
  Proof.
(* Goal: @eq X (@vec_pos X n (@vec_set_pos X n (fun p : pos n => @vec_pos X n v p)) p) (@vec_pos X n v p) *)
    unfold vec_plus; rewrite vec_pos_set; auto.
  Qed.

  Fact vec_zero_plus v : vec_plus vec_zero v = v.
  Proof. 
(* Goal: @eq (vec X n) (fun2vec O n (@vec2fun n v x)) v *)
    apply vec_pos_ext.
(* Goal: forall p : pos n, @eq nat (@vec_pos nat n (vec_plus u (vec_plus v w)) p) (@vec_pos nat n (vec_plus (vec_plus u v) w) p) *)
    intros p; unfold vec_zero, vec_plus. 
(* Goal: @eq X (@vec_pos X n (@vec_set_pos X n (fun p : pos n => @vec_pos X n v p)) p) (@vec_pos X n v p) *)
    repeat rewrite vec_pos_set; auto.
  Qed.
  
  Fact vec_zero_spec p : vec_pos vec_zero p = 0.
  Proof. unfold vec_zero; rewrite vec_pos_set; trivial. Qed.

  Fact vec_plus_comm v w : vec_plus v w = vec_plus w v.
  Proof.
(* Goal: @eq (vec X n) (fun2vec O n (@vec2fun n v x)) v *)
    apply vec_pos_ext.
(* Goal: forall p : pos n, @eq nat (@vec_pos nat n (vec_plus u (vec_plus v w)) p) (@vec_pos nat n (vec_plus (vec_plus u v) w) p) *)
    intros p; unfold vec_zero, vec_plus.
(* Goal: @eq nat (@vec_pos nat n (@vec_set_pos nat n (fun p : pos n => Init.Nat.add (@vec_pos nat n u p) (@vec_pos nat n (@vec_set_pos nat n (fun p0 : pos n => Init.Nat.add (@vec_pos nat n v p0) (@vec_pos nat n w p0))) p))) p) (@vec_pos nat n (@vec_set_pos nat n (fun p : pos n => Init.Nat.add (@vec_pos nat n (@vec_set_pos nat n (fun p0 : pos n => Init.Nat.add (@vec_pos nat n u p0) (@vec_pos nat n v p0))) p) (@vec_pos nat n w p))) p) *)
    repeat rewrite vec_pos_set; omega.
  Qed.

  Fact vec_plus_assoc u v w : vec_plus u (vec_plus v w) = vec_plus (vec_plus u v) w.
  Proof.
(* Goal: @eq (vec X n) (fun2vec O n (@vec2fun n v x)) v *)
    apply vec_pos_ext.
(* Goal: forall p : pos n, @eq nat (@vec_pos nat n (vec_plus u (vec_plus v w)) p) (@vec_pos nat n (vec_plus (vec_plus u v) w) p) *)
    intros p; unfold vec_zero, vec_plus.
(* Goal: @eq nat (@vec_pos nat n (@vec_set_pos nat n (fun p : pos n => Init.Nat.add (@vec_pos nat n u p) (@vec_pos nat n (@vec_set_pos nat n (fun p0 : pos n => Init.Nat.add (@vec_pos nat n v p0) (@vec_pos nat n w p0))) p))) p) (@vec_pos nat n (@vec_set_pos nat n (fun p : pos n => Init.Nat.add (@vec_pos nat n (@vec_set_pos nat n (fun p0 : pos n => Init.Nat.add (@vec_pos nat n u p0) (@vec_pos nat n v p0))) p) (@vec_pos nat n w p))) p) *)
    repeat rewrite vec_pos_set; omega.
  Qed.

  Fact vec_plus_is_zero u v : vec_zero = vec_plus u v -> u = vec_zero /\ v = vec_zero.
  Proof.
   unfold vec_zero, vec_plus; intros H; split; apply vec_pos_ext;
   intros p; apply f_equal with (f := fun v => vec_pos v p) in H;
(* Goal: lt O (@vec_sum n v) *)
(* Goal: P v *)
   repeat rewrite vec_pos_set in * |- *; omega.
  Qed.
  
  Definition vec_one p : vec _ n := vec_set_pos (fun q => if pos_eq_dec p q then 1 else 0).
  
  Fact vec_one_spec_eq p q : p = q -> vec_pos (vec_one p) q = 1.
  Proof.
(* Goal: forall _ : @eq (pos n) p q, @eq nat (@vec_pos nat n (vec_one p) q) (S O) *)
    intros [].
(* Goal: @eq nat (@vec_pos nat n (vec_one p) q) O *)
    unfold vec_one; rewrite vec_pos_set.
(* Goal: @eq nat (if @pos_eq_dec n p p then S O else O) (S O) *)
    destruct (pos_eq_dec p p) as [ | [] ]; auto.
  Qed.
  
  Fact vec_one_spec_neq p q : p <> q -> vec_pos (vec_one p) q = 0.
  Proof.
(* Goal: forall _ : lt i n, @eq X (@vec2fun n (fun2vec O n f) x i) (f i) *)
    intros H.
(* Goal: @eq nat (@vec_pos nat n (vec_one p) q) O *)
    unfold vec_one; rewrite vec_pos_set.
(* Goal: @eq nat (if @pos_eq_dec n p q then S O else O) O *)
    destruct (pos_eq_dec p q) as [ | ]; auto.
(* Goal: @eq nat (S O) O *)
    destruct H; auto.
  Qed.
  
End vec_plus.

Arguments vec_plus {n}.
Arguments vec_zero {n}.
Arguments vec_one {n}.

Reserved Notation " e '#>' x " (at level 58).
Reserved Notation " e [ v / x ] " (at level 57, v at level 0, x at level 0, left associativity).

Local Notation " e '#>' x " := (vec_pos e x) (at level 58).
Local Notation " e [ v / x ] " := (vec_change e x v) (at level 57, v at level 0, x at level 0, left associativity).

Tactic Notation "rew" "vec" :=
  repeat lazymatch goal with 
    |              |- context[ _[_/?x]#>?x ] => rewrite vec_change_eq with (p := x) (1 := eq_refl)
    | _ : ?x = ?y  |- context[ _[_/?x]#>?y ] => rewrite vec_change_eq with (p := x) (q := y)
    | _ : ?y = ?x  |- context[ _[_/?x]#>?y ] => rewrite vec_change_eq with (p := x) (q := y)
    | _ : ?x <> ?y |- context[ _[_/?x]#>?y ] => rewrite vec_change_neq with (p := x) (q := y)
    | _ : ?y <> ?x |- context[ _[_/?x]#>?y ] => rewrite vec_change_neq with (p := x) (q := y)
    |              |- context[ vec_pos vec_zero ?x ] => rewrite vec_zero_spec with (p := x)
    |              |- context[ vec_pos (vec_one ?x) ?x ] => rewrite vec_one_spec_eq with (p := x) (1 := eq_refl)
    | _ : ?x = ?y  |- context[ vec_pos (vec_one ?x) ?y ] => rewrite vec_one_spec_eq with (p := x) (q := y)
    | _ : ?y = ?x  |- context[ vec_pos (vec_one ?x) ?y ] => rewrite vec_one_spec_eq with (p := x) (q := y)
    | _ : ?x <> ?y |- context[ vec_pos (vec_one ?x) ?y ] => rewrite vec_one_spec_neq with (p := x) (q := y)
    | _ : ?y <> ?x |- context[ vec_pos (vec_one ?x) ?y ] => rewrite vec_one_spec_neq with (p := x) (q := y)
    | |- context[ _[_/?x][_/?x] ] => rewrite vec_change_idem with (p := x) 
    | |- context[ ?v[(?v#>?x)/?x] ] => rewrite vec_change_same with (p := x)
    | |- context[ _[_/?x]#>?y ] => rewrite vec_change_neq with (p := x) (q := y); [ | discriminate ]
    | |- context[ vec_plus vec_zero ?x ] => rewrite vec_zero_plus with (v := x)
    | |- context[ vec_plus ?x vec_zero ] => rewrite (vec_plus_comm x vec_zero); rewrite vec_zero_plus with (v := x)
    | |- vec_plus ?x ?y = vec_plus ?y ?x => apply vec_plus_comm
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
  end; auto.

Tactic Notation "vec" "split" hyp(v) "with" ident(n) :=
  rewrite (vec_head_tail v); generalize (vec_head v) (vec_tail v); clear v; intros n v.

Tactic Notation "vec" "nil" hyp(v) := rewrite (vec_0_nil v).

Fact vec_zero_S n : @vec_zero (S n) = 0##vec_zero.
Proof. auto. Qed.

Fact vec_one_fst n : @vec_one (S n) pos0 = 1##vec_zero.
Proof.
(* Goal: @eq (vec X n) (fun2vec O n (@vec2fun n v x)) v *)
  apply vec_pos_ext.
(* Goal: forall p : pos (S n), @eq nat (@vec_pos nat (S n) (@vec_one (S n) (@pos_fst n)) p) (@vec_pos nat (S n) (@vec_cons nat n (S O) (@vec_zero n)) p) *)
  intros p; pos_inv p; rew vec.
Qed.

Fact vec_one_nxt n p : @vec_one (S n) (pos_nxt p) = 0##vec_one p.
Proof.
(* Goal: @eq (vec X n) (fun2vec O n (@vec2fun n v x)) v *)
  apply vec_pos_ext.
(* Goal: forall p0 : pos (S n), @eq nat (@vec_pos nat (S n) (@vec_one (S n) (@pos_nxt n p)) p0) (@vec_pos nat (S n) (@vec_cons nat n O (@vec_one n p)) p0) *)
  unfold vec_one.
(* Goal: forall p0 : pos (S n), @eq nat (@vec_pos nat (S n) (@vec_set_pos nat (S n) (fun q : pos (S n) => if @pos_eq_dec (S n) (@pos_nxt n p) q then S O else O)) p0) (@vec_pos nat (S n) (@vec_cons nat n O (@vec_set_pos nat n (fun q : pos n => if @pos_eq_dec n p q then S O else O))) p0) *)
  intros q; rewrite vec_pos_set.
(* Goal: @eq nat (if @pos_eq_dec (S n) (@pos_nxt n p) q then S O else O) (@vec_pos nat (S n) (@vec_cons nat n O (@vec_set_pos nat n (fun q : pos n => if @pos_eq_dec n p q then S O else O))) q) *)
  pos_inv q.
(* Goal: @eq nat (if @pos_eq_dec (S n) (@pos_nxt n p) (@pos_fst n) then S O else O) (@vec_pos nat (S n) (@vec_cons nat n O (@vec_set_pos nat n (fun q : pos n => if @pos_eq_dec n p q then S O else O))) (@pos_fst n)) *)
(* Goal: @eq nat (if @pos_eq_dec (S n) (@pos_nxt n p) (@pos_nxt n q) then S O else O) (@vec_pos nat (S n) (@vec_cons nat n O (@vec_set_pos nat n (fun q : pos n => if @pos_eq_dec n p q then S O else O))) (@pos_nxt n q)) *)
  simpl; auto.
(* Goal: @eq nat (if @pos_eq_dec (S n) (@pos_nxt n p) (@pos_nxt n q) then S O else O) (@vec_pos nat (S n) (@vec_cons nat n O (@vec_set_pos nat n (fun q : pos n => if @pos_eq_dec n p q then S O else O))) (@pos_nxt n q)) *)
  rewrite <- vec_pos_tail.
(* Goal: @eq nat (if @pos_eq_dec (S n) (@pos_nxt n p) (@pos_nxt n q) then S O else O) (@vec_pos nat n (@vec_tail nat n (@vec_cons nat n O (@vec_set_pos nat n (fun q : pos n => if @pos_eq_dec n p q then S O else O)))) q) *)
  simpl vec_tail.
(* Goal: @eq nat (if @pos_eq_dec (S n) (@pos_nxt n p) (@pos_nxt n q) then S O else O) (@vec_pos nat n (@vec_set_pos nat n (fun q : pos n => if @pos_eq_dec n p q then S O else O)) q) *)
  rewrite vec_pos_set.
(* Goal: @eq nat (if @pos_eq_dec (S n) (@pos_nxt n p) (@pos_nxt n q) then S O else O) (if @pos_eq_dec n p q then S O else O) *)
  destruct (pos_eq_dec p q) as [ | C ].
(* Goal: P v *)
  subst.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
  destruct (pos_eq_dec (pos_nxt q) (pos_nxt q)) as [ | [] ]; auto.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
  destruct (pos_eq_dec (pos_nxt p) (pos_nxt q)) as [ | ]; auto.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
  destruct C; apply pos_nxt_inj; auto.
Qed.

Fact vec_plus_cons n x v y w : @vec_plus (S n) (x##v) (y##w) = x+y ## vec_plus v w.
Proof.
(* Goal: @eq (vec nat (S n)) (@vec_plus (S n) (@vec_cons nat n x v) (@vec_cons nat n y w)) (@vec_cons nat n (Init.Nat.add x y) (@vec_plus n v w)) *)
  apply vec_pos_ext; unfold vec_plus.
(* Goal: forall p : pos (S n), @eq nat (@vec_pos nat (S n) (@vec_set_pos nat (S n) (fun p0 : pos (S n) => Init.Nat.add (@vec_pos nat (S n) (@vec_cons nat n x v) p0) (@vec_pos nat (S n) (@vec_cons nat n y w) p0))) p) (@vec_pos nat (S n) (@vec_cons nat n (Init.Nat.add x y) (@vec_set_pos nat n (fun p0 : pos n => Init.Nat.add (@vec_pos nat n v p0) (@vec_pos nat n w p0)))) p) *)
  intros p; pos_inv p; repeat (rewrite vec_pos_set; simpl; auto).
Qed.

Fact vec_change_succ n v p : v[(S (v#>p))/p] = @vec_plus n (vec_one p) v.
Proof.
(* Goal: @eq (vec X n) (fun2vec O n (@vec2fun n v x)) v *)
  apply vec_pos_ext.
(* Goal: forall p0 : pos n, @eq nat (@vec_pos nat n v p0) (@vec_pos nat n (@vec_plus n (@vec_one n p) (@vec_change nat n v p u)) p0) *)
  intros q.
  destruct (pos_eq_dec p q); rew vec;
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
  rewrite vec_pos_plus; rew vec; subst; auto.
Qed.

Fact vec_change_pred n v p u : v#>p = S u -> v = @vec_plus n (vec_one p) (v[u/p]).
Proof.
(* Goal: forall _ : @eq nat (@vec_pos nat n v p) (S u), @eq (vec nat n) v (@vec_plus n (@vec_one n p) (@vec_change nat n v p u)) *)
  intros Hu.
(* Goal: @eq (vec X n) (fun2vec O n (@vec2fun n v x)) v *)
  apply vec_pos_ext.
(* Goal: forall p0 : pos n, @eq nat (@vec_pos nat n v p0) (@vec_pos nat n (@vec_plus n (@vec_one n p) (@vec_change nat n v p u)) p0) *)
  intros q.
  destruct (pos_eq_dec p q); rew vec;
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
  rewrite vec_pos_plus; rew vec; subst; auto.
Qed.

Fixpoint vec_sum n (v : vec nat n) := 
  match v with 
    | vec_nil       => 0
    | vec_cons x w  => x + vec_sum w
  end.
  
Fact vec_sum_plus n v w : @vec_sum n (vec_plus v w) = vec_sum v + vec_sum w.
Proof.
(* Goal: @eq nat (@vec_sum n (@vec_plus n v w)) (Init.Nat.add (@vec_sum n v) (@vec_sum n w)) *)
  revert w; induction v; intros w.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
  rewrite (vec_0_nil (vec_plus _ _)), (vec_0_nil w); auto.
(* Goal: @eq nat (@vec_sum (S n) (@vec_plus (S n) (@vec_cons nat n x v) w)) (Init.Nat.add (@vec_sum (S n) (@vec_cons nat n x v)) (@vec_sum (S n) w)) *)
  rewrite (vec_head_tail w), vec_plus_cons; simpl.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add x (@vec_head nat n w)) (@vec_sum n (@vec_plus n v (@vec_tail nat n w)))) (Init.Nat.add (Init.Nat.add x (@vec_sum n v)) (Init.Nat.add (@vec_head nat n w) (@vec_sum n (@vec_tail nat n w)))) *)
  rewrite IHv; omega.
Qed.

Fact vec_sum_zero n : @vec_sum n vec_zero = 0.
Proof. induction n; simpl; auto. Qed.

Fact vec_sum_one n p : @vec_sum n (vec_one p) = 1.
Proof.
(* Goal: @eq nat (@vec_sum n (@vec_one n p)) (S O) *)
  revert p; induction n; intros p.
(* Goal: @eq nat (@vec_sum (S n) (@vec_one (S n) p)) (S O) *)
  pos_inv p.
(* Goal: @eq nat (@vec_sum (S n) (@vec_one (S n) p)) (S O) *)
  pos_inv p.
(* Goal: @eq nat (@vec_sum (S n) (@vec_one (S n) (@pos_fst n))) (S O) *)
(* Goal: @eq nat (@vec_sum (S n) (@vec_one (S n) (@pos_nxt n p))) (S O) *)
  rewrite vec_one_fst.
(* Goal: @eq nat (@vec_sum (S n) (@vec_cons nat n (S O) (@vec_zero n))) (S O) *)
(* Goal: @eq nat (@vec_sum (S n) (@vec_one (S n) (@pos_nxt n p))) (S O) *)
  simpl; f_equal; apply vec_sum_zero.
(* Goal: @eq nat (@vec_sum (S n) (@vec_one (S n) (@pos_nxt n p))) (S O) *)
  rewrite vec_one_nxt.
(* Goal: @eq nat (@vec_sum (S n) (@vec_cons nat n O (@vec_one n p))) (S O) *)
  unfold vec_sum; fold vec_sum.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
  rewrite IHn; auto.
Qed.
  
Fact vec_sum_is_zero n v : @vec_sum n v = 0 -> v = vec_zero.
Proof.
(* Goal: forall _ : @eq nat (@vec_sum n v) O, @eq (vec nat n) v (@vec_zero n) *)
  induction v; simpl; auto.
(* Goal: forall _ : @eq nat (Init.Nat.add x (@vec_sum n v)) O, @eq (vec nat (S n)) (@vec_cons nat n x v) (@vec_zero (S n)) *)
  simpl; rewrite vec_zero_S; intros; f_equal.
(* Goal: lt O (@vec_sum n v) *)
(* Goal: P v *)
  omega.
(* Goal: lt O (@vec_sum n v) *)
(* Goal: P v *)
  apply IHv; omega.
Qed.

Fact vec_sum_is_nzero n v : 0 < @vec_sum n v -> { p : _ & { w | v = vec_plus (vec_one p) w } }.
Proof.
(* Goal: forall _ : lt O (@vec_sum n v), @sigT (pos n) (fun p : pos n => @sig (vec nat n) (fun w : vec nat n => @eq (vec nat n) v (@vec_plus n (@vec_one n p) w))) *)
  induction v as [ | n x v IHv ]; intros Hv; simpl in Hv.
(* Goal: lt O (@vec_sum n v) *)
(* Goal: P v *)
  omega.
(* Goal: @sigT (pos (S n)) (fun p : pos (S n) => @sig (vec nat (S n)) (fun w : vec nat (S n) => @eq (vec nat (S n)) (@vec_cons nat n x v) (@vec_plus (S n) (@vec_one (S n) p) w))) *)
  destruct x as [ | x ].
(* Goal: @sigT (pos (S n)) (fun p : pos (S n) => @sig (vec nat (S n)) (fun w : vec nat (S n) => @eq (vec nat (S n)) (@vec_cons nat n O v) (@vec_plus (S n) (@vec_one (S n) p) w))) *)
(* Goal: @sigT (pos (S n)) (fun p : pos (S n) => @sig (vec nat (S n)) (fun w : vec nat (S n) => @eq (vec nat (S n)) (@vec_cons nat n (S x) v) (@vec_plus (S n) (@vec_one (S n) p) w))) *)
  apply IHv in Hv.
(* Goal: @sigT (pos (S n)) (fun p : pos (S n) => @sig (vec nat (S n)) (fun w : vec nat (S n) => @eq (vec nat (S n)) (@vec_cons nat n O v) (@vec_plus (S n) (@vec_one (S n) p) w))) *)
(* Goal: @sigT (pos (S n)) (fun p : pos (S n) => @sig (vec nat (S n)) (fun w : vec nat (S n) => @eq (vec nat (S n)) (@vec_cons nat n (S x) v) (@vec_plus (S n) (@vec_one (S n) p) w))) *)
  destruct Hv as (p & w & Hw).
(* Goal: @eq nat (@vec_sum (S n) (@vec_one (S n) (@pos_nxt n p))) (S O) *)
  exists (pos_nxt p), (0##w); rewrite vec_one_nxt.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
  rewrite vec_plus_cons; f_equal; auto.
(* Goal: @sigT (pos (S n)) (fun p : pos (S n) => @sig (vec nat (S n)) (fun w : vec nat (S n) => @eq (vec nat (S n)) (@vec_cons nat n (S x) v) (@vec_plus (S n) (@vec_one (S n) p) w))) *)
  exists pos0, (x##v).
(* Goal: @eq (vec nat (S n)) (@vec_cons nat n (S x) v) (@vec_plus (S n) (@vec_one (S n) (@pos_fst n)) (@vec_cons nat n x v)) *)
  rewrite vec_one_fst, vec_plus_cons; rew vec.
Qed.

Section vec_nat_induction.

  (* Specialized induction on vec nat n, with constant n *)

  Variable (n : nat) (P : vec nat n -> Type).
  
  Hypothesis HP0 : P vec_zero.
  Hypothesis HP1 : forall p, P (vec_one p).
  Hypothesis HP2 : forall v w, P v -> P w -> P (vec_plus v w).
  
  Theorem vec_nat_induction v : P v.
  Proof.
(* Goal: P v *)
    induction v as [ v IHv ] using (measure_rect (@vec_sum n)).
(* Goal: P v *)
    case_eq (vec_sum v).
    
(* Goal: forall _ : @eq nat (@vec_sum n v) O, P v *)
(* Goal: forall (n0 : nat) (_ : @eq nat (@vec_sum n v) (S n0)), P v *)
    intros Hv.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
    apply vec_sum_is_zero in Hv; subst; auto.
    
(* Goal: forall (n0 : nat) (_ : @eq nat (@vec_sum n v) (S n0)), P v *)
    intros x Hx.
(* Goal: P v *)
    destruct (vec_sum_is_nzero v) as (p & w & Hw).
(* Goal: lt O (@vec_sum n v) *)
(* Goal: P v *)
    omega.
(* Goal: P v *)
    subst.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
    apply HP2; auto.
(* Goal: P w *)
    apply IHv.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
    rewrite vec_sum_plus, vec_sum_one; auto.
  Qed.
  
End vec_nat_induction.

Section vec_map_list.

  Variable X : Type.

  (* morphism between vec nat n and (list X)/~p *)

  Fixpoint vec_map_list X n v : (pos n -> X) -> list X :=
    match v in vec _ m return (pos m -> _) -> _ with
      | vec_nil => fun _ => nil
      | a##v    => fun f => list_repeat (f pos0) a ++ vec_map_list v (fun p => f (pos_nxt p))
    end.

  Fact vec_map_list_zero n f : vec_map_list (@vec_zero n) f = @nil X.
  Proof. revert f; induction n; intros f; simpl; auto. Qed.

  Fact vec_map_list_one n p f : vec_map_list (@vec_one n p) f = f p :: @nil X.
  Proof.
(* Goal: @eq (list X) (@vec_map_list X n (@vec_one n p) f) (@cons X (f p) (@nil X)) *)
    revert f; induction p; intro.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
    rewrite vec_one_fst; simpl; rewrite vec_map_list_zero; auto.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
    rewrite vec_one_nxt; simpl; rewrite IHp; auto.
  Qed.

  (* The morphism *)

  Fact vec_map_list_plus n v w f : @vec_map_list X n (vec_plus v w) f ~p vec_map_list v f ++ vec_map_list w f.
  Proof.
(* Goal: @Permutation X (@vec_map_list X n (@vec_plus n v w) f) (@app X (@vec_map_list X n v f) (@vec_map_list X n w f)) *)
    revert v w f; induction n as [ | n IHn ]; intros v w f.
(* Goal: @eq nat (if @pos_eq_dec (S n) (@pos_nxt n p) (@pos_fst n) then S O else O) (@vec_pos nat (S n) (@vec_cons nat n O (@vec_set_pos nat n (fun q : pos n => if @pos_eq_dec n p q then S O else O))) (@pos_fst n)) *)
(* Goal: @eq nat (if @pos_eq_dec (S n) (@pos_nxt n p) (@pos_nxt n q) then S O else O) (@vec_pos nat (S n) (@vec_cons nat n O (@vec_set_pos nat n (fun q : pos n => if @pos_eq_dec n p q then S O else O))) (@pos_nxt n q)) *)
    rewrite (vec_0_nil (vec_plus v w)), (vec_0_nil v), (vec_0_nil w); simpl; auto.
(* Goal: @Permutation X (@vec_map_list X (S n) (@vec_plus (S n) v w) f) (@app X (@vec_map_list X (S n) v f) (@vec_map_list X (S n) w f)) *)
    rewrite (vec_head_tail v), (vec_head_tail w), vec_plus_cons.
(* Goal: @Permutation X (@vec_map_list X (S n) (@vec_cons nat n (Init.Nat.add (@vec_head nat n v) (@vec_head nat n w)) (@vec_plus n (@vec_tail nat n v) (@vec_tail nat n w))) f) (@app X (@vec_map_list X (S n) (@vec_cons nat n (@vec_head nat n v) (@vec_tail nat n v)) f) (@vec_map_list X (S n) (@vec_cons nat n (@vec_head nat n w) (@vec_tail nat n w)) f)) *)
    generalize (vec_head v) (vec_tail v) (vec_head w) (vec_tail w); clear v w; intros x v y w.
(* Goal: @Permutation X (@vec_map_list X (S n) (@vec_cons nat n (Init.Nat.add x y) (@vec_plus n v w)) f) (@app X (@vec_map_list X (S n) (@vec_cons nat n x v) f) (@vec_map_list X (S n) (@vec_cons nat n y w) f)) *)
    simpl.
(* Goal: @Permutation X (@app X (@list_repeat X (f (@pos_fst n)) (Init.Nat.add x y)) (@vec_map_list X n (@vec_plus n v w) (fun p : pos n => f (@pos_nxt n p)))) (@app X (@app X (@list_repeat X (f (@pos_fst n)) x) (@vec_map_list X n v (fun p : pos n => f (@pos_nxt n p)))) (@app X (@list_repeat X (f (@pos_fst n)) y) (@vec_map_list X n w (fun p : pos n => f (@pos_nxt n p))))) *)
    rewrite list_repeat_plus.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
    solve list eq; apply Permutation_app; auto.
    apply Permutation_trans with (list_repeat (f pos0) y 
                               ++ vec_map_list v (fun p => f (pos_nxt p)) 
                               ++ vec_map_list w (fun p => f (pos_nxt p))).
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
    apply Permutation_app; auto.
(* Goal: @Permutation X (@app X (@list_repeat X (f (@pos_fst n)) y) (@app X (@vec_map_list X n v (fun p : pos n => f (@pos_nxt n p))) (@vec_map_list X n w (fun p : pos n => f (@pos_nxt n p))))) (@app X (@vec_map_list X n v (fun p : pos n => f (@pos_nxt n p))) (@app X (@list_repeat X (f (@pos_fst n)) y) (@vec_map_list X n w (fun p : pos n => f (@pos_nxt n p))))) *)
    do 2 rewrite <- app_ass.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
    apply Permutation_app; auto.
(* Goal: @Permutation X (@app X (@list_repeat X (f (@pos_fst n)) y) (@vec_map_list X n v (fun p : pos n => f (@pos_nxt n p)))) (@app X (@vec_map_list X n v (fun p : pos n => f (@pos_nxt n p))) (@list_repeat X (f (@pos_fst n)) y)) *)
    apply Permutation_app_comm.
  Qed.

End vec_map_list.

Fact map_vec_map_list X Y (f : X -> Y) n v g : map f (@vec_map_list _ n v g) = vec_map_list v (fun p => f (g p)).
Proof.
(* Goal: @eq nat (if @pos_eq_dec (S n) (@pos_nxt n p) (@pos_fst n) then S O else O) (@vec_pos nat (S n) (@vec_cons nat n O (@vec_set_pos nat n (fun q : pos n => if @pos_eq_dec n p q then S O else O))) (@pos_fst n)) *)
(* Goal: @eq nat (if @pos_eq_dec (S n) (@pos_nxt n p) (@pos_nxt n q) then S O else O) (@vec_pos nat (S n) (@vec_cons nat n O (@vec_set_pos nat n (fun q : pos n => if @pos_eq_dec n p q then S O else O))) (@pos_nxt n q)) *)
  revert g; induction v; intro; simpl; auto.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
  rewrite map_app; f_equal; auto.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
  rewrite map_list_repeat; auto.
Qed.

Definition list_vec X (l : list X) : { v : vec X (length l) | vec_list v = l }.
Proof.
(* Goal: @Permutation X (@vec_map_list X (S n) (@vec_cons nat n (Init.Nat.add x y) (@vec_plus n v w)) f) (@app X (@vec_map_list X (S n) (@vec_cons nat n x v) f) (@vec_map_list X (S n) (@vec_cons nat n y w) f)) *)
  induction l as [ | x l (v & Hv) ]; simpl.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
  exists vec_nil; auto.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
  exists (x##v); simpl; f_equal; auto.
Qed.

Fact vec_reif X n (R : pos n -> X -> Prop) : (forall p, ex (R p)) -> exists v, forall p, R p (vec_pos v p).
Proof.
(* Goal: forall _ : lt i n, @eq X (@vec2fun n (fun2vec O n f) x i) (f i) *)
  intros H.
(* Goal: @ex (vec X n) (fun v : vec X n => forall p : pos n, R p (@vec_pos X n v p)) *)
  apply pos_reification in H.
(* Goal: @sig (vec X n) (fun v : vec X n => forall p : pos n, R p (@vec_pos X n v p)) *)
  destruct H as (f & Hf).
(* Goal: @sig (vec X n) (fun v : vec X n => forall p : pos n, R p (@vec_pos X n v p)) *)
  exists (vec_set_pos f).
(* Goal: forall p : pos n, R p (@vec_pos X n (@vec_set_pos X n f) p) *)
  intro; rewrite vec_pos_set; trivial.
Qed.

Fact vec_reif_t X n (R : pos n -> X -> Prop) : (forall p, sig (R p)) -> { v | forall p, R p (vec_pos v p) }.
Proof.
(* Goal: forall _ : lt i n, @eq X (@vec2fun n (fun2vec O n f) x i) (f i) *)
  intros H.
(* Goal: @sig (vec X n) (fun v : vec X n => forall p : pos n, R p (@vec_pos X n v p)) *)
  apply pos_reif_t in H.
(* Goal: @sig (vec X n) (fun v : vec X n => forall p : pos n, R p (@vec_pos X n v p)) *)
  destruct H as (f & Hf).
(* Goal: @sig (vec X n) (fun v : vec X n => forall p : pos n, R p (@vec_pos X n v p)) *)
  exists (vec_set_pos f).
(* Goal: forall p : pos n, R p (@vec_pos X n (@vec_set_pos X n f) p) *)
  intro; rewrite vec_pos_set; trivial.
Qed.

Section fun2vec.

  Variable X : Type.

  Fixpoint fun2vec i n f : vec X _ :=
    match n with 
      | 0   => vec_nil
      | S n => f i##fun2vec (S i) n f
    end.

  Fact fun2vec_id i n f : fun2vec i n f = vec_set_pos (fun p => f (i+pos2nat p)).
  Proof.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
    revert i; induction n as [ | n IHn ]; intros i; simpl; f_equal; auto.
(* Goal: @eq (vec X n) (fun2vec (S i) n f) (@vec_set_pos X n (fun p : pos n => f (Init.Nat.add i (@pos2nat (S n) (@pos_nxt n p))))) *)
    rewrite IHn.
(* Goal: @eq (vec X n) (@vec_set_pos X n (fun p : pos n => f (Init.Nat.add (S i) (@pos2nat n p)))) (@vec_set_pos X n (fun p : pos n => f (Init.Nat.add i (@pos2nat (S n) (@pos_nxt n p))))) *)
    apply vec_pos_ext; intros; do 2 rewrite vec_pos_set; f_equal.
(* Goal: lt O (@vec_sum n v) *)
(* Goal: P v *)
    rewrite pos2nat_nxt; omega.
  Qed.

  Fact fun2vec_lift i n f : fun2vec i n (fun j => f (S j)) = fun2vec (S i) n f.
  Proof. revert i f; induction n; intros; simpl; f_equal; auto. Qed.

  Fact vec_pos_fun2vec i n f p : vec_pos (fun2vec i n f) p = f (i+pos2nat p).
  Proof. rewrite fun2vec_id, vec_pos_set; auto. Qed.

  Definition vec2fun n (v : vec X n) x i := 
    match le_lt_dec n i with
      | left  _ => x
      | right H => vec_pos v (nat2pos H)
    end.

  Fact fun2vec_vec2fun n v x : fun2vec 0 n (@vec2fun n v x) = v.
  Proof.
(* Goal: @eq (vec X n) (fun2vec O n (@vec2fun n v x)) v *)
    apply vec_pos_ext.
(* Goal: @Permutation X (@vec_map_list X (S n) (@vec_cons nat n (Init.Nat.add x y) (@vec_plus n v w)) f) (@app X (@vec_map_list X (S n) (@vec_cons nat n x v) f) (@vec_map_list X (S n) (@vec_cons nat n y w) f)) *)
    intros p; rewrite vec_pos_fun2vec; simpl.
(* Goal: @eq X (@vec2fun n (fun2vec O n f) x i) (f i) *)
    unfold vec2fun.
(* Goal: @eq X match le_lt_dec n (@pos2nat n p) with | left l => x | right H => @vec_pos X n v (@nat2pos n (@pos2nat n p) H) end (@vec_pos X n v p) *)
    generalize (pos2nat_prop p).
(* Goal: lt O (@vec_sum n v) *)
(* Goal: P v *)
    destruct (le_lt_dec n (pos2nat p)); try omega. 
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
    rewrite nat2pos_pos2nat; auto.
  Qed.

  Fact vec2fun_fun2vec n f x i : i < n -> @vec2fun n (fun2vec 0 n f) x i = f i.
  Proof.
(* Goal: forall _ : lt i n, @eq X (@vec2fun n (fun2vec O n f) x i) (f i) *)
    intros H.
(* Goal: @eq X (@vec2fun n (fun2vec O n f) x i) (f i) *)
    unfold vec2fun.
(* Goal: lt O (@vec_sum n v) *)
(* Goal: P v *)
    destruct (le_lt_dec n i); try omega.
(* Goal: @eq (vec nat (S n)) (@vec_zero (S n)) (@vec_cons nat n O (@vec_zero n)) *)
    rewrite vec_pos_fun2vec, pos2nat_nat2pos; auto.
  Qed. 

End fun2vec.
