HyPre.util.VectorList

(* CLN C *)
From HyPre Require Export VectorExtra.
From Coq Require Import Lists.List.
Require Import Tac.
Import ListNotations.
From Coq Require Import Program.Equality.

(* TODO Prove all VectorList lemmas *)
Fixpoint try_t_combine_cons {k : nat} {X : Type} (xl : list (Vector.t X k)) (yl : list X)
  : option (list (Vector.t X (S k)))
  := match xl, yl with
     | nil, nil
       => Some nil
     | x :: xl, y :: yl
       => let xyl := try_t_combine_cons xl yl in
         match xyl with
         | Some xyl => Some ((Vector.cons _ y _ x) :: xyl)
         | None => None
         end
     | _, _ => None
     end.

Fixpoint try_t_combine {k : nat} {X : Type} (xt : Vector.t (list X) k) : option (list (Vector.t X k))
  := match xt with
     | Vector.nil _ => Some nil
     | Vector.cons _ yl n xt
       => let bt_o := try_t_combine xt in
         match bt_o with
         | Some bt
           => try_t_combine_cons bt yl
         | None => None
         end
     end.

Definition veclist_cons {X : Type} {n : nat}
  : Vector.t X n -> Vector.t (list X) n -> Vector.t (list X) n
  := Vector.map2 (fun y x => y :: x).

Definition veclist_app {X : Type} {n : nat}
  : Vector.t (list X) n -> Vector.t (list X) n -> Vector.t (list X) n
  := Vector.map2 (fun y x => y ++ x).

Definition sum_len {X : Type} {k : nat} : Vector.t (list X) k -> nat
  := Vector.fold_left (fun n x => n + length x) 0.

Fixpoint veclist_empty (X : Type) (k : nat) : Vector.t (list X) k
  := match k with
     | O => Vector.nil _
     | S k' => Vector.cons _ [] _ (veclist_empty X k')
     end.

Definition veclist_indexCons {X : Type} {k : nat} (xt : Vector.t (list X) k) (i : Fin.t k) (x : X)
  : Vector.t (list X) k
  := Vector.replace xt i (x :: Vector.nth xt i).

Module VectorListNotations.

  Infix ":vl:" := veclist_cons (at level 69).
  Infix "+vl+" := veclist_app (at level 69).

  Notation "x :i: xt 'at' i" := (veclist_indexCons xt i x) (at level 40).

End VectorListNotations.
(*
Section with_kX.
  Context {X : Type}.
  Context {k : nat}.
 *)
Import VectorListNotations.

Inductive Veclist {X : Type} {n : nat} : Vector.t (list X) n -> Prop :=
| VLnil : Veclist (veclist_empty X n)
| VLcons : forall xt yt i x, Veclist xt -> yt = (x :i: xt at i) -> Veclist yt.

Inductive VeclistO {X : Type} {n : nat} (Orcl : Vector.t (list X) n -> Fin.t n)
  : Vector.t (list X) n -> Prop
  :=
  | VLOnil : VeclistO Orcl (veclist_empty X n)
  | VLOcons : forall xt yt i x, VeclistO Orcl xt -> Orcl xt = i -> yt = (x :i: xt at i) -> VeclistO Orcl yt.

Inductive VeclistP {X : Type} {n : nat} (Orcl : Vector.t (list X) n -> Prop)
  : Vector.t (list X) n -> Prop
  :=
  | VLPnil : VeclistP Orcl (veclist_empty X n)
  | VLPcons : forall xt yt i x, VeclistP Orcl xt -> Orcl yt -> yt = (x :i: xt at i) -> VeclistP Orcl yt.

Definition fair_oracle {X : Type} {n : nat} (Orcl : Vector.t (list X) n -> Fin.t n)
  := forall v, VeclistO Orcl v -> forall i, exists e, VeclistO Orcl (e +vl+ v) /\ Orcl e = i.

Definition vl_len {X : Type} {k : nat} (v : Vector.t (list X) k) : Vector.t nat k
  := Vector.map (fun w => length w) v.

Lemma vec_map2_map2_assoc {X Y Z : Type} {k} (f : X -> Y -> Y) (g : Y -> Z -> Y)
      (Hassoc : forall x y z, g (f x y) z = f x (g y z))
  : forall (xt yt zt : Vector.t _ k), Vector.map2 g (Vector.map2 f xt yt) zt = Vector.map2 f xt (Vector.map2 g yt zt).
Proof.
  intros.
  dependent induction xt;dependent destruction yt;dependent destruction zt.
  - cbn.
    reflexivity.
  - cbn.
    rewrite Hassoc.
    rewrite IHxt.
    reflexivity.
Qed.

Lemma vl_cons_app {X : Type} {k : nat} (x : Vector.t X k) (yt zt : Vector.t (list X) k)
  : (x :vl: yt) +vl+ zt = x :vl: (yt +vl+ zt).
Proof.
  unfold veclist_cons, veclist_app.
  eapply vec_map2_map2_assoc.
  intros.
  eapply app_comm_cons.
Qed.

Lemma veclist_cons_nth {X : Type} {k : nat} (b : Vector.t X k) a i
  : (b :vl: a) [[i]] = b[[i]] :: a[[i]].
Proof.
  dependent induction b;dependent destruction a;dependent destruction i.
  - cbn.
    reflexivity.
  - cbn.
    eauto.
Qed.

Lemma veclist_app_nth {X : Type} k (b : Vector.t (list X) k) a i
  : (b +vl+ a) [[i]] = b[[i]] ++ a[[i]].
Proof.
  dependent induction b; dependent destruction a; dependent destruction i.
  - cbn.
    reflexivity.
  - cbn.
    eauto.
Qed.

From HyPre Require Import PreSuffix.

Lemma Forall2_vl_app22 {k} {A B : Type} (P : _ -> _ -> Prop) (a : Vector.t A k) (b c : Vector.t (list B) k)
      (Hpc : forall i x y, prefix x y -> P i y -> P i x)
  : Vector.Forall2 P a (b +vl+ c) -> Vector.Forall2 P a c.
Proof.
  intros.
  eapply Vec_Forall2_forall2.
  intros i.
  eapply Vec_Forall2_forall2 with (i:=i) in H.
  setoid_rewrite veclist_app_nth in H.
  eapply Hpc.
  2: eapply H.
  eapply prefix_app_r.
  econstructor.
Qed.

Definition vl_tl {k : nat} {X : Type} (xl : Vector.t (list X) k) : Vector.t (list X) k
  := Vector.map (@tl _) xl.

Lemma vl_zero_vl_app {X : Type} {k : nat}
  : @vl_zero X k = vl_zero +vl+ vl_zero.
Proof.
  clear.
  induction k.
  - cbn;eauto.
  - cbn.
    f_equal.
    assumption.
Qed.

Lemma vl_Forall_Forall_vl_app {k : nat} {X : Type} (xt yt : Vector.t (list X) k) (P : X -> Prop)
  : Vector.Forall (Forall P) xt
    -> Vector.Forall (Forall P) yt
    -> Vector.Forall (Forall P) (xt +vl+ yt).
Proof using.
  clear.
  intros Hx Hy.
  dependent induction Hx;
    dependent destruction Hy.
  - cbn.
    econstructor.
  - revert v v0 Hy Hx IHHx.
    revert x0 H0.
    induction H;
      intros x0 Hx0;
      induction Hx0;
      intros;cbn.
    + econstructor;eauto.
    + econstructor;eauto.
    + rewrite app_nil_r.
      econstructor;eauto.
    + econstructor;eauto.
      specialize (Forall_app P (x::l) (x0::l0)) as Q.
      destruct Q as [_ Q].
      eapply Q.
      split;eauto.
Qed.

Definition veclist_infix {k : nat} {X : Type} : Vector.t (list X) k -> Vector.t (list X) k -> Prop
  := Vector.Forall2 (fun l1 l2 => infix l1 l2).