Awesome List Lemmas

AwesomeListLemmas.v

(* 
  
  Some lemmas that can be used in conjunction with those in Coq.Lists.List
  
  See https://coq.inria.fr/library/Coq.Lists.List.html
 
 *)

Require Import Lia.
Require Import Coq.Lists.List.
Require Import Coq.Arith.Wf_nat.


Import ListNotations.

(* firstn / skipn / nth_error / map / combine *)

Lemma skipn_skipn {B : Type}: forall n m (l : list B),
  skipn n (skipn m l) = skipn (n + m) l.
Proof.
    intros n m l. generalize dependent n. generalize dependent l. 
    induction m as [|m' IHm'].
    - simpl. intros. replace (n + 0) with n by lia. reflexivity.
    - intros l n. destruct l as [|h t].
      + simpl. repeat rewrite skipn_nil. reflexivity.
      + simpl. destruct n as [|n'].
        * reflexivity.
        * rewrite IHm'. simpl plus.
          replace (n' + S m') with (S (n' + m')) by lia.
          reflexivity.
Qed.


Lemma nth_error_skipn {X} : forall (xs : list X) i d,
  nth_error xs (i + d) = nth_error (skipn d xs) i.
Proof.
  intros.
  rewrite <- firstn_skipn with (n := d) (l := xs) at 1.
  assert (d < length xs \/ d >= length xs) as Hxs by lia.
  destruct Hxs.
  - rewrite nth_error_app2.
    + rewrite firstn_length.
      f_equal. lia.
    + rewrite firstn_length.
      lia.
  - rewrite firstn_all2 by lia.
    rewrite skipn_all2 by lia.
    rewrite app_nil_r.
    replace (nth_error (@nil X) i) with (@None X)
      by now destruct i.
    replace (nth_error xs (i + d)) with (@None X).
    auto.
    symmetry. apply nth_error_None. lia.
Qed.

Lemma nth_error_firstn {X : Type} (l : list X) : forall d i,
  i < d
  -> nth_error (firstn d l) i = nth_error l i.
Proof.
  intros d i Hdi.
  assert (d <= length l \/ d > length l) as [Hdl | Hdl] by lia.
  + rewrite <- firstn_skipn with (l := l) (n := d) at 2.
  rewrite nth_error_app1. auto.
  rewrite firstn_length. lia.
  + now rewrite firstn_all2 by lia.
Qed.

Lemma firstn_in {X : Type} : forall (l : list X) n,
  forall x, In x (firstn n l) -> In x l.
Proof.
  intros.
  rewrite <- (firstn_skipn n l) at 1.
  apply in_or_app. auto.
Qed.

Lemma skipn_in {X : Type} : forall (l : list X) n,
  forall x, In x (skipn n l) -> In x l.
Proof.
  intros.
  rewrite <- (firstn_skipn n l) at 1.
  apply in_or_app. auto.
Qed.

Lemma hd_error_skipn {X : Type} (l : list X) : forall i,
  hd_error (skipn i l) = nth_error l i.
Proof.
  intro i.
  generalize dependent l. induction i.
  - intro. rewrite skipn_O. destruct l; auto.
  - intro. destruct l; auto.
    simpl. auto.
Qed.

Lemma hd_error_nth_error {X : Type} (l : list X) :
  hd_error l = nth_error l 0.
Proof.
  destruct l; auto.
Qed.

Lemma nth_error_rev {X : Type} (l : list X) (n : nat) :
  n < length l ->
  nth_error (rev l) n = nth_error l (length l - S n).
Proof.
  destruct l.
  - simpl. destruct n; reflexivity.
  - intros. remember (x :: l) as l'.
    rewrite nth_error_nth' with (d := x).
    rewrite nth_error_nth' with (d := x).
    f_equal. apply rev_nth.
    auto. lia. auto.
    rewrite rev_length. auto.
Qed.

Lemma nth_error_Some_ex {X : Type} (l : list X) (n : nat) :
  n < length l <->
  exists x, nth_error l n = Some x.
Proof.
  split.
  - intros. destruct (nth_error l n) eqn:Hnth.
    + exists x. auto.
    + apply nth_error_None in Hnth. lia.
  - intros [x Hnth]. apply nth_error_Some. congruence.
Qed.

Lemma map_id {X} : forall (xs : list X),
  map id xs = xs.
Proof.
  induction xs; auto.
  simpl. rewrite IHxs. auto.
Qed.

Lemma combine_map {X Y M N} : forall (f : X -> M) (g : Y -> N) xs ys,
  combine (map f xs) (map g ys) = map (fun '(x, y) => (f x, g y)) (combine xs ys).
Proof.
  induction xs.
  - auto.
  - intros. destruct ys.
    + simpl. auto.
    + simpl. rewrite IHxs. auto.
Qed.

Lemma combine_app {X Y} : forall (xs1 xs2 : list X) (ys1 ys2 : list Y),
  length xs1 = length ys1
  -> combine (xs1 ++ xs2) (ys1 ++ ys2) = combine xs1 ys1 ++ combine xs2 ys2.
Proof.
  intros.
  revert ys1 H.
  induction xs1.
  - intros. destruct ys1. auto. simpl in H. discriminate.
  - intros. destruct ys1. simpl in H. discriminate.
    simpl. rewrite IHxs1. auto.
    simpl in H. inversion H. auto.
Qed.

Lemma combine_rev {X Y} : forall (xs : list X) (ys : list Y),
  length xs = length ys
  -> combine (rev xs) (rev ys) = rev (combine xs ys).
Proof.
  intros.
  revert ys H.
  induction xs.
  - intros. destruct ys. auto. simpl in H. discriminate.
  - intros. destruct ys. simpl in H. discriminate.
    simpl. simpl in H. inversion H.
    rewrite combine_app. simpl. rewrite IHxs. auto.
    auto.
    repeat rewrite rev_length. auto.
Qed. 

Lemma map_repeat {X Y : Type} (f : X -> Y) (x : X) n :
  map f (repeat x n) = repeat (f x) n.
Proof.
  induction n; auto.
  simpl. rewrite IHn. auto.
Qed.

Lemma repeat_iff {X : Type} (x : X) l:
  l = repeat x (length l) <-> (forall y, In y l -> y = x).
Proof.
  split.
  - intros. rewrite H in H0.
    apply repeat_spec in H0. auto.
  - intros. apply Forall_eq_repeat.
    apply Forall_forall. firstorder.
Qed.

(* zipWith *)

Definition zipWith {X Y Z} (f : X -> Y -> Z) (xs : list X) (ys : list Y) : list Z :=
  map (fun '(x, y) => f x y) (combine xs ys).

Lemma zipWith_length {X Y Z} : forall (f : X -> Y -> Z) xs ys,
  length (zipWith f xs ys) = min (length xs) (length ys).
Proof.
  intros. unfold zipWith.
  now rewrite map_length, combine_length.
Qed.

Lemma zipWith_in {X Y Z} : forall (P : X -> Prop) (Q : Y -> Prop) (R : Z -> Prop) (f : X -> Y -> Z) xs ys,
  (forall x, In x xs -> P x)
  -> (forall y, In y ys -> Q y)
  -> (forall x y, P x -> Q y -> R (f x y))
  -> forall z, In z (zipWith f xs ys) -> R z.
Proof.
  intros P Q R f.
  induction xs; intros ys Hxs Hys Hf z Hz.
  - simpl in Hz. inversion Hz.
  - simpl in Hz. destruct ys.
    + inversion Hz.
    + destruct Hz.
      * subst. apply Hf.
        apply Hxs. now left.
        apply Hys. now left.
      * rewrite in_map_iff in H.
        destruct H as [[xx yy] [H1 H2]].
        subst. apply Hf.
        apply Hxs. right.
        now apply in_combine_l in H2.
        apply Hys. right.
        now apply in_combine_r in H2.
Qed.

Lemma nth_error_zipWith {X Y Z} : forall (f : X -> Y -> Z) xs ys n,
  nth_error (zipWith f xs ys) n = 
  match nth_error xs n, nth_error ys n with
  | Some x, Some y => Some (f x y)
  | _, _ => None
  end.
Proof.
  intros f. induction xs.
  - intros ys n.
    assert (zipWith f [] ys = []). {
      unfold zipWith. destruct ys; auto.
    }
    rewrite H.
    remember (nth_error [] n) as nz.
    assert (nz = None). {
      subst. destruct n; auto.
    }
    remember (nth_error (@nil X) n) as nx.
    assert (nx = None). {
      subst. destruct n; auto.
    }
    rewrite H0, H1. auto.
  - intros. destruct n.
    + simpl. destruct ys.
      * auto.
      * simpl. auto.
    + destruct ys.
      * simpl. destruct (nth_error xs n); auto.
      * simpl.
        rewrite <- IHxs.
        auto.
Qed.

Lemma zipWith_cons {X Y Z} : forall (f : X -> Y -> Z) x xs y ys,
  zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys.
Proof.
  auto.
Qed.

Lemma zipWith_repeat_l {X Y Z} : forall n (f : X -> Y -> Z) x ys,
  n >= length ys
  -> zipWith f (repeat x n) ys = map (f x) ys.
Proof.
  induction n.
  - intros. simpl. destruct ys; [auto | simpl in H; lia].
  - intros. destruct ys.
    + simpl. auto.
    + simpl. rewrite zipWith_cons.
      rewrite IHn. auto.
      simpl in H. lia.
Qed.

Lemma zipWith_repeat_r {X Y Z} : forall n (f : X -> Y -> Z) xs y,
  n >= length xs
  -> zipWith f xs (repeat y n) = map (fun x => f x y) xs.
Proof.
  induction n.
  - intros. simpl. destruct xs; [auto | simpl in H; lia].
  - intros. destruct xs.
    + simpl. auto.
    + simpl. rewrite zipWith_cons.
      rewrite IHn. auto.
      simpl in H. lia.
Qed.

Lemma zipWith_firstn_l {X Y Z} : forall (f : X -> Y -> Z) xs ys,
  zipWith f xs ys = zipWith f xs (firstn (length xs) ys).
Proof.
  unfold zipWith. intros. rewrite combine_firstn_l. auto.
Qed.

Lemma zipWith_firstn_r {X Y Z} : forall (f : X -> Y -> Z) xs ys,
  zipWith f xs ys = zipWith f (firstn (length ys) xs) ys.
Proof.
  unfold zipWith. intros. rewrite combine_firstn_r. auto.
Qed.

Lemma zipWith_firstn {X Y Z} : forall (f : X -> Y -> Z) xs ys,
  zipWith f xs ys = 
    let n := (min (length xs) (length ys)) in 
    zipWith f (firstn n xs) (firstn n ys).
Proof.
  intros. 
  assert (length xs <= length ys \/ length xs > length ys) as [H | H] by lia.
  - replace (min (length xs) (length ys)) with (length xs) by lia.
    simpl.
    assert (zipWith f xs ys = zipWith f xs (firstn (length xs) ys)) as H1.
    { apply zipWith_firstn_l. }
    assert (zipWith f xs (firstn (length xs) ys) = 
            zipWith f (firstn (length xs) xs) (firstn (length xs) ys)) as H3.
    { f_equal. now rewrite firstn_all. }
    congruence.
  - replace (min (length xs) (length ys)) with (length ys) by lia.
    simpl.
    assert (zipWith f xs ys = zipWith f (firstn (length ys) xs) ys) as H1.
    { apply zipWith_firstn_r. }
    assert (zipWith f (firstn (length ys) xs) ys = 
            zipWith f (firstn (length ys) xs) (firstn (length ys) ys)) as H3.
    { f_equal. now rewrite firstn_all. }
    congruence.
Qed.

Lemma zipWith_map { M N X Y Z }: forall (f : M -> N -> Z) (g : X -> M) (h : Y -> N) (xs : list X) (ys : list Y),
  zipWith f (map g xs) (map h ys) = map (fun '(x, y) => f (g x) (h y)) (combine xs ys).
Proof.
  intros. unfold zipWith.
  rewrite combine_map. rewrite map_map.
  apply map_ext. intros. destruct a. auto.
Qed.

Lemma zipWith_assoc {X}: forall (f : X -> X -> X) xs ys zs,
  (forall x y z, f x (f y z) = f (f x y) z)
  -> zipWith f xs (zipWith f ys zs) = zipWith f (zipWith f xs ys) zs.
Proof.
  intros f xs.
  remember (length xs) as len.
  generalize dependent xs.
  induction len. 
  - intros. destruct xs. auto. simpl in Heqlen. discriminate.
  - intros. destruct xs.
    + auto. 
    + destruct ys.
      * auto.
      * destruct zs.
        -- auto.
        -- simpl. repeat rewrite zipWith_cons.
           rewrite H. rewrite IHlen.
           ++ auto.
           ++ simpl in Heqlen. inversion Heqlen. auto.
           ++ apply H. 
Qed.

Lemma zipWith_ext { X Y Z M N } : forall (f : X -> Y -> Z) (g : M -> N -> Z) xs ys ms ns,
  (forall x y m n, In ((x, y), (m, n)) (combine (combine xs ys) (combine ms ns)) -> f x y = g m n)
  -> length xs = length ms
  -> length ys = length ns
  -> zipWith f xs ys = zipWith g ms ns.
Proof.
  intros f g xs.
  remember (length xs) as len.
  generalize dependent xs.
  induction len. 
  - intros. destruct xs. destruct ms. auto.
    simpl in H0. discriminate. simpl in H0. discriminate.
  - intros. destruct xs. {
    simpl in Heqlen. discriminate.
  } destruct ms. {
    simpl in Heqlen. discriminate.
  } destruct ys. {
    simpl in H1. simpl in H0.
    destruct ns. auto. simpl in H1. discriminate.
  } destruct ns. {
    simpl in H1. discriminate.
  }
  rewrite zipWith_cons. rewrite zipWith_cons.
  simpl in H. f_equal.
  + apply H. auto.
  + apply IHlen.
    1 : { simpl in Heqlen. inversion Heqlen. auto. }
    3 : { simpl in H1. inversion H1. auto. }    
    2 : { simpl in H. firstorder. }
    firstorder.
Qed.

Lemma zipWith_cons_singleton {X} : forall (xs : list X) (xss : list (list X)),
  zipWith cons xs xss = zipWith (@app X) (map (fun x => [x]) xs) xss.
Proof.
  intros.
  apply zipWith_ext.
  2 : { now rewrite map_length. }
  2 : { auto. }
  revert xss.
  induction xs.
  - intros. simpl in H. tauto.
  - intros. destruct xss.
    + simpl in H. tauto.
    + simpl in H. destruct H.
      * inversion H. auto.
      * eapply IHxs. eauto.
Qed. 

Lemma zipWith_rev {X Y Z} : forall (f : X -> Y -> Z) xs ys,
  length xs = length ys
  -> zipWith f (rev xs) (rev ys) = rev (zipWith f xs ys).
Proof.
  intros. unfold zipWith.
  rewrite combine_rev by assumption.
  apply map_rev.
Qed.

Lemma zipWith_map2 {X Y Z W : Type} (f : X -> Y -> Z) (g : Z -> W) (xs : list X) (ys : list Y) :
  map g (zipWith f xs ys) = zipWith (fun x y => g (f x y)) xs ys.
Proof.
  unfold zipWith at 2.
  replace (map (fun '(x, y) => g (f x y)) (combine xs ys))
    with (map g (map (fun '(x, y) => f x y) (combine xs ys))). 2: {
    rewrite map_map. apply map_ext_in. intros [x y]. auto.
  } 
  auto.
Qed.

Lemma zipWith_ext_id_l {X Y : Type} (f : X -> Y -> X) (xs : list X) (ys : list Y) :
  (forall x y, In (x, y) (combine xs ys) -> f x y = x)
  -> length xs <= length ys
  -> zipWith f xs ys = xs.
Proof.
  remember (length xs) as len.
  generalize dependent xs.
  generalize dependent ys.
  induction len.
  - intros. destruct xs; destruct ys; auto.
    simpl in Heqlen. discriminate.
    simpl in H0. discriminate.
  - intros. destruct xs; destruct ys; auto.
    + simpl in H0. lia.
    + simpl in H. rewrite zipWith_cons.
      f_equal.
      * specialize (H x y). auto.
      * apply IHlen. 
        simpl in Heqlen. lia.
        intros. apply H. auto. 
        simpl in H0. lia.
Qed.

Lemma zipWith_ext_id_r {X Y : Type} (f : X -> Y -> Y) (xs : list X) (ys : list Y) :
  (forall x y, In (x, y) (combine xs ys) -> f x y = y)
  -> length xs >= length ys
  -> zipWith f xs ys = ys.
Proof.
  remember (length xs) as len.
  generalize dependent xs.
  generalize dependent ys.
  induction len.
  - intros. destruct xs; destruct ys; auto.
    simpl in H0. lia.
    simpl in H0. discriminate.
  - intros. destruct xs; destruct ys; auto.
    + simpl in H0. discriminate.
    + simpl in H. rewrite zipWith_cons.
      f_equal.
      * specialize (H x y). auto.
      * apply IHlen. 
        simpl in Heqlen. lia.
        intros. apply H. auto. 
        simpl in H0. lia.
Qed.

(* transpose *)

Fixpoint transpose {X : Type} (len : nat) (tapes : list (list X)) : list (list X) :=
  match tapes with
  | [] => repeat [] len
  | t :: ts => zipWith cons t (transpose len ts)
  end.

  Lemma transpose_length {X : Type} : forall len (tapes : list (list X)),
  (forall t, 
    In t tapes -> length t >= len)
  -> length (transpose len tapes) = len.
Proof.
  intros len tapes. revert len.
  induction tapes; intros len Hlen.
  - simpl. now rewrite repeat_length.
  - simpl. rewrite zipWith_length.
    rewrite IHtapes.
    + simpl in Hlen. specialize (Hlen a).
      assert (length a >= len) by auto.
      lia.
    + intros t Ht. apply Hlen. now right.
Qed.

Lemma transpose_inner_length {X : Type}: forall len (tapes : list (list X)),
  forall u,
    In u (transpose len tapes)
    -> length u = length tapes.
Proof.
  intros len tapes. revert len.
  induction tapes; intros len u Hu.
  - simpl in *. apply repeat_spec in Hu.
    subst. auto.
  - simpl in *.
    unfold zipWith in Hu.
    rewrite in_map_iff in Hu.
    destruct Hu as [[u1 us] [Hu Hus]].
    apply in_combine_r in Hus.
    subst. simpl. f_equal.
    firstorder.
Qed.

Lemma transpose_inner_length_eq {X : Type} : forall len (tapes : list (list X)),
  forall u v,
    In u (transpose len tapes)
    -> In v (transpose len tapes)
    -> length u = length v.
Proof.
  intros.
  apply transpose_inner_length in H.
  apply transpose_inner_length in H0.
  congruence.
Qed.

Lemma transpose_app {X : Type} : forall len (tapes1 tapes2 : list (list X)),
  (forall t, In t tapes1 -> length t >= len)
  -> (forall t, In t tapes2 -> length t >= len)
  -> transpose len (tapes1 ++ tapes2) = 
  zipWith (@app X) (transpose len tapes1) (transpose len tapes2).
Proof.
  intros len tapes1 tapes2 Ht1 Ht2.
  induction tapes1.
  - simpl.
    rewrite zipWith_repeat_l.
    rewrite <- map_id with (xs := transpose _ _) at 1.
    apply map_ext. auto.
    rewrite transpose_length. auto. auto.
  - simpl. rewrite IHtapes1.
    + rewrite zipWith_cons_singleton.
      rewrite zipWith_cons_singleton.
      rewrite zipWith_assoc by apply app_assoc.
      auto.
    + simpl in Ht1. firstorder.  
Qed.

Lemma transpose_singleton {X : Type} : forall (t : list X),
  transpose (length t) [t] = map (fun x => [x]) t.
Proof.
  intros. unfold transpose. 
  now rewrite zipWith_repeat_r by lia.
Qed.

Lemma transpose_rev_aux {X : Type} : forall (xss : list (list X)) (l : list X),
  (forall t u, In t xss -> In u xss -> length t = length u)
  -> zipWith (@app X) (map (@rev X) xss) (map (fun x => [x]) l) 
    = map (@rev X) (zipWith (@app X) (map (fun x => [x]) l) xss).
Proof.
  induction xss as [ | xs xss].
  - intros. simpl.
    destruct l.
    + auto.
    + simpl. unfold zipWith. auto.
  - intros. destruct l.
    + simpl. unfold zipWith. auto.
    + simpl map at 1 2. rewrite zipWith_cons.
      simpl map at 3. f_equal.
      rewrite IHxss. auto.
      simpl in H. firstorder.
Qed.

Lemma transpose_rev {X : Type} : forall len (tapes : list (list X)),
  (forall t, In t tapes -> length t = len)
  -> transpose len (rev tapes) = map (@rev X) (transpose len tapes).
Proof.
  intros len tapes Hlen.
  induction tapes.
  - simpl. rewrite <- map_id with (xs := repeat [] len) at 1.
    apply map_ext_in. intros.
    apply repeat_spec in H. subst. auto.
  - simpl. simpl in Hlen.
    assert (length a = len) as Ha. {
      apply Hlen. auto.
    }
    rewrite transpose_app.
    rewrite IHtapes.
    rewrite zipWith_cons_singleton.
    rewrite <- Ha.
    rewrite transpose_singleton.
    rewrite transpose_rev_aux. auto.
    + apply transpose_inner_length_eq.
    + auto.
    + intros. rewrite <- in_rev in H.
      enough (length t = len) by lia. auto.
    + simpl. intros. 
      enough (length t = len) by lia. firstorder.
Qed.

Lemma transpose_zipWith_cons {X : Type} : forall len (mat : list (list X)) t,
    (forall u, In u mat -> length u >= len) 
  -> length t = length mat
  -> transpose (S len) (zipWith cons t mat) = t :: transpose len mat.
Proof.
  intros len mat. revert len. induction mat as [ | t1 mat1 IHmat].
  - intros. simpl. destruct t; auto. simpl in H0. discriminate.
  - intros. simpl. destruct t.
    + simpl in H0. discriminate.
    + rewrite zipWith_cons.
      simpl transpose. rewrite IHmat.
      * now rewrite zipWith_cons.
      * simpl in H. firstorder.
      * simpl in H0. now inversion H0.
Qed.


Lemma transpose_involutive {X : Type} : forall len (tapes : list (list X)),
  (forall t, In t tapes -> length t = len)
  -> transpose (length tapes) (transpose len tapes) = tapes.
Proof.
  intros len tapes. revert len.
  induction tapes as [ | t tapes1 IHtapes].
  - simpl. intros.
    destruct len; auto.
  - intros. simpl. rewrite transpose_zipWith_cons.
    + rewrite IHtapes. auto.
      simpl in H. firstorder.
    + simpl in H. intros.
      enough (length u = length tapes1) by lia.
      apply transpose_inner_length with (len := len).
      auto.
    + rewrite transpose_length.
      * simpl in H. apply H. auto.
      * simpl in H. intros.
        enough (length t0 = len) by lia.
        apply H. auto.
Qed.

Lemma transpose_rev2 {X : Type} : forall len (tapes : list (list X)),
  (forall t, In t tapes -> length t = len)
  -> rev (transpose len tapes) = transpose len (map (@rev X) tapes).
Proof.
  intros len tapes Hlen.
  pose proof (@transpose_rev X (length tapes) (transpose len tapes)).
  assert (forall t, In t (transpose len tapes) -> length t = length tapes) as Hlen2. {
    intros; now apply transpose_inner_length in H0.
  }
  specialize (H Hlen2).
  rewrite transpose_involutive in H.
  apply (f_equal (fun x => transpose len x)) in H.
  replace len with (length (rev (transpose len tapes))) in H at 1. 2 :{
    rewrite rev_length. rewrite transpose_length. auto.
    intros. enough (length t = len) by lia. auto.
  }
  rewrite transpose_involutive in H. auto.
  - intros. rewrite <- in_rev in H0.
    now apply transpose_inner_length with (len := len).
  - auto.  
  (* (1) from transpose_rev: transpose (rev tapes) = map rev (transpose tapes)
     (2) plugin (tapes := transpose tapes): 
            transpose (rev (transpose tapes)) 
          = map rev (transpose (transpose tapes)) 
          = map rev tapes 
      (3) apply transpose to both sides.
  *)
Qed.

Lemma transpose_firstn {X : Type} : forall len (tapes : list (list X)) n,
  (forall t, In t tapes -> length t >= len)
  -> transpose len (firstn n tapes) = map (firstn n) (transpose len tapes).
Proof.
  intros len tapes n Hlen.
  assert (n > length tapes \/ n <= length tapes) as [Hn | Hn] by lia. {
    rewrite firstn_all2 by lia.
    rewrite map_ext_in with (g := id).
    now rewrite map_id.
    intros. simpl.
    rewrite firstn_all2.
    auto. apply transpose_inner_length in H. lia.
  }
  rewrite <- firstn_skipn with (l := tapes) (n := n) at 2.
  rewrite transpose_app. rewrite zipWith_map2.
  rewrite zipWith_ext_id_l. auto.
  - intros. rewrite firstn_app.
    enough (n = length x). {
      rewrite H0.
      replace (length x - length x) with 0 by lia.
      rewrite firstn_O. rewrite firstn_all. apply app_nil_r.
    }
    apply in_combine_l in H.
    apply transpose_inner_length in H.
    rewrite firstn_length in H.
    lia.
  - repeat rewrite transpose_length. auto.
    * intros. apply skipn_in in H. auto.
    * intros. apply firstn_in in H. auto.
  - intros. apply firstn_in in H. auto.
  - intros. apply skipn_in in H. auto.
Qed.

Lemma transpose_skipn {X : Type} : forall len (tapes : list (list X)) n,
  (forall t, In t tapes -> length t >= len)
  -> transpose len (skipn n tapes) = map (skipn n) (transpose len tapes).
Proof.
  intros len tapes n Hlen.
  assert (n > length tapes \/ n <= length tapes) as [Hn | Hn] by lia. {
    rewrite skipn_all2 by lia.
    simpl. revert Hn.
    induction tapes.
    - simpl. rewrite map_repeat. destruct n; auto.
    - simpl. intros. rewrite zipWith_map2. unfold zipWith.
      rewrite map_ext_in with (g := (fun x => [])). 2 : {
        intros. destruct a0. 
        pose proof H as H0.
        apply in_combine_l in H.
        apply in_combine_r in H0.
        apply skipn_all2.
        simpl. apply transpose_inner_length in H0.
        lia.
      } 
      assert (length (combine a (transpose len tapes)) = len). {
        rewrite combine_length. simpl in Hlen.
        rewrite transpose_length. specialize (Hlen a ltac:(auto)). lia.
        auto.
      }
      remember (map _ (combine _ _)) as rhs.
      assert (rhs = repeat [] (length rhs)). {
        rewrite repeat_iff. subst rhs. intros.
        apply in_map_iff in H0. destruct H0 as [? [? ?]].
        auto.
      }
      rewrite Heqrhs in H0 at 2. rewrite map_length in H0.
      rewrite H in H0. auto.
  }
  rewrite <- firstn_skipn with (l := tapes) (n := n) at 2.
  rewrite transpose_app. rewrite zipWith_map2.
  rewrite zipWith_ext_id_r. auto.
  - intros. rewrite skipn_app.
    enough (n = length x). {
      rewrite H0.
      replace (length x - length x) with 0 by lia.
      rewrite skipn_O. rewrite skipn_all. auto.
    }
    apply in_combine_l in H.
    apply transpose_inner_length in H.
    rewrite firstn_length in H.
    lia.
  - repeat rewrite transpose_length. auto.
    * intros. apply skipn_in in H. auto.
    * intros. apply firstn_in in H. auto.
  - intros. apply firstn_in in H. auto.
  - intros. apply skipn_in in H. auto.
Qed.

Lemma skipn_zipWith_cons {X : Type} (xs : list X) (xss : list (list X)) :
 length xs >= length xss
  -> map (skipn 1) (zipWith cons xs xss) = xss.
Proof.
  generalize dependent xs.
  induction xss; intros.
  - destruct xs; auto.
  - destruct xs.
    + simpl in H. lia.
    + rewrite zipWith_cons.
      rewrite map_cons.
      simpl skipn at 1.
      f_equal. apply IHxss. 
      simpl in H. lia.
Qed.

(* augmentVString *)

Definition augmentVString {X : Type} (vstring : list (list X)) (tape : list X) : list (list X) :=
  zipWith (@app X) vstring (map (fun x => [x]) tape).

Lemma augmentVString_length {X : Type} : forall (vstring : list (list X)) (tape : list X),
  length tape >= length vstring
  -> length (augmentVString vstring tape) = length vstring.
Proof.
  intros. unfold augmentVString.
  rewrite zipWith_length. rewrite map_length. 
  lia.
Qed.

Lemma augmentVString_inner_length {X : Type} : forall (vstring : list (list X)) (tape : list X) i,
  i < length vstring
  -> forall val, nth_error (augmentVString vstring tape) i = Some val
  -> exists val', nth_error vstring i = Some val' /\ length val = S (length val').
Proof.
  intros.
  unfold augmentVString in H0.
  rewrite nth_error_zipWith in H0.
  destruct (nth_error vstring i) eqn:Heq; try discriminate.
  destruct (nth_error (map (fun x : X => [x]) tape) i) eqn:Heq2; try discriminate.
  inversion H0.
  exists l. split; [auto | ].
  rewrite app_length. enough (length l0 = 1) by lia.
  rewrite nth_error_map in Heq2.
  unfold option_map in Heq2.
  destruct (nth_error tape i); try discriminate.
  inversion Heq2. auto.
Qed.

Lemma augmentVString_inner_length_eq {X : Type} : forall (vstring : list (list X)) (tape : list X),
  length tape >= length vstring
  -> (forall u v, In u vstring -> In v vstring -> length u = length v)
  -> (forall u v, In u (augmentVString vstring tape) -> In v (augmentVString vstring tape) -> length u = length v).
Proof.
  intros.
  apply In_nth_error in H1, H2.
  destruct H1 as [i1 Hi1], H2 as [i2 Hi2].
  assert (i1 < length vstring). {
    rewrite <- augmentVString_length with (tape := tape) by auto.
    apply nth_error_Some. congruence.
  }
  assert (i2 < length vstring). {
    rewrite <- augmentVString_length with (tape := tape) by auto.
    apply nth_error_Some. congruence.
  }
  apply augmentVString_inner_length in Hi1; [ | auto].
  apply augmentVString_inner_length in Hi2; [ | auto].
  destruct Hi1 as [u1 [Hu1 Hu1len]].
  destruct Hi2 as [u2 [Hu2 Hu2len]].
  rewrite Hu1len, Hu2len. f_equal.
  apply nth_error_In in Hu1.
  apply nth_error_In in Hu2.
  apply H0; auto.
Qed.

Lemma augmentVString_transpose {X : Type} : forall (vstring : list (list X)) (tape : list X) len,
  (forall val, In val vstring -> length val = len)
  -> length tape = length vstring
  -> transpose (length tape) (transpose len vstring ++ [tape]) = augmentVString vstring tape.
Proof.
  intros.
  rewrite transpose_app. 2 : {
    intros. apply transpose_inner_length in H1.
    lia.
  } 2 : {
    simpl. firstorder. subst. auto.
  }
  rewrite transpose_singleton.
  rewrite H0.
  rewrite transpose_involutive by assumption.
  unfold augmentVString.
  reflexivity.
Qed.

Lemma augmentVString_transpose_1 {X : Type} : forall (vstring : list (list X)) (tape : list X) len,
(forall val, In val vstring -> length val = len)
-> length tape = length vstring
-> transpose (S len) (augmentVString vstring tape) = transpose len vstring ++ [tape].
Proof.
  intros.
  rewrite <- augmentVString_transpose with (len := len) by auto.
  assert (S len = length (transpose len vstring ++ [tape])) as Hlen. {
    rewrite app_length. rewrite transpose_length. simpl. lia.
    intros t Hx. apply H in Hx. lia. 
  }
  rewrite Hlen. rewrite transpose_involutive. auto.
  intros. apply in_app_iff in H1. destruct H1.
  - apply transpose_inner_length in H1. congruence.
  - simpl in H1. firstorder. congruence.
Qed. 

(* ij_error *)

Definition ij_error {X : Type} (i j : nat) (l : list (list X)) : option X :=
  match nth_error l i with
  | Some l' => nth_error l' j
  | None => None
  end.

Lemma ij_error_remove_rows {X : Type} (i j d : nat) (l : list (list X)) :
  ij_error (i + d) j l = ij_error i j (skipn d l).
Proof.
  unfold ij_error.
  rewrite nth_error_skipn.
  auto.
Qed.

Lemma ij_error_remove_cols {X : Type} (i j d : nat) (l : list (list X)) :
  ij_error i (j + d) l = ij_error i j (map (skipn d) l).
Proof.
  unfold ij_error.
  remember (nth_error l i) as row_i.
  destruct row_i.
  2 : {
    symmetry in Heqrow_i. 
    rewrite nth_error_None in Heqrow_i.
    assert (nth_error (map (skipn d) l) i = None). {
      rewrite nth_error_None.
      now rewrite map_length.
    }
    rewrite H. auto.
  }
  assert (length l > i) as Hlen. {
    symmetry in Heqrow_i.
    assert (nth_error l i <> None) by congruence.
    rewrite nth_error_Some in H.
    lia.
  }
  remember (nth_error (map (skipn d) l) i) as row_i'.
  destruct row_i'.
  2 : {
    symmetry in Heqrow_i'.
    rewrite nth_error_None in Heqrow_i'.
    rewrite map_length in Heqrow_i'. lia.
  }
  rewrite nth_error_map in Heqrow_i'.
  rewrite <- Heqrow_i in Heqrow_i'. simpl in Heqrow_i'.
  inversion Heqrow_i'. subst.
  now rewrite nth_error_skipn.
Qed.

Lemma transpose_spec_0 {X : Type} : forall (xs : list X) (xss : list (list X)) i,
  length xss = length xs
  -> nth_error xs i = ij_error i 0 (zipWith cons xs xss).
Proof.
  induction xs.
  - intros. simpl. destruct i; auto.
  - intros xss. destruct i.
    + intros. simpl. unfold ij_error.
      destruct xss.
      * simpl in H. lia.
      * simpl. auto.
    + intros. simpl. unfold ij_error.
      destruct xss.
      * simpl in H. lia.
      * rewrite zipWith_cons.
        simpl nth_error. 
        rewrite IHxs with (xss := xss).
        auto. simpl in H. lia.
Qed. 

Lemma transpose_spec {X : Type} : forall len (tapes : list (list X)),
  (forall t,
    In t tapes -> length t = len)
  -> forall i j,
    ij_error i j tapes = ij_error j i (transpose len tapes).
Proof.
  induction tapes as [|l tapes IHt]; simpl; intros H.
- (* when the matrix is empty *)
  intros i j.
  destruct i.
  + unfold ij_error at 1. simpl.
    unfold ij_error. 
    assert (j < len \/ j >= len) by lia.
    destruct H0.
    ++ rewrite nth_error_repeat by apply H0.
       auto.
    ++ assert (nth_error (repeat (@nil X) len) j = None). {
         rewrite nth_error_None by lia.
         rewrite repeat_length.
         auto.
       }
       rewrite H1. auto.
  + unfold ij_error at 1. simpl.
    unfold ij_error. 
    assert (j < len \/ j >= len) by lia.
    destruct H0.
    ++ rewrite nth_error_repeat by apply H0.
       auto.
    ++ assert (nth_error (repeat (@nil X) len) j = None). {
         rewrite nth_error_None by lia.
         rewrite repeat_length.
         auto.
       }
       rewrite H1. auto. 
- destruct i.
  + (* ij_error 0 j and ij_error j 0 *)
    intros j.
    unfold ij_error at 1. simpl.
    apply transpose_spec_0.
    rewrite transpose_length.
    symmetry. apply H. auto.
    intros. enough (length t = len) by lia.
    apply H. auto.
  + (* ij_error (S i) j and ij_error j (S i *)
    replace (S i) with (i + 1) by lia. intros.
    rewrite ij_error_remove_cols.
    rewrite ij_error_remove_rows.
    simpl skipn at 1.
    rewrite IHt. 
    rewrite skipn_zipWith_cons. auto.
    * rewrite transpose_length.
      enough (length l = len) by lia.
      apply H. auto.
      intros.
      enough (length t = len) by lia.
      apply H. auto.
    * intros. 
      enough (length t = len) by lia.
      apply H. auto.
Qed.

(* select *)

Fixpoint select {X} (selector : list nat) (selectee : list X) : option (list X) :=
  match selector with
  | [] => Some []
  | n :: ns =>
    match nth_error selectee n with
    | Some x => 
      match select ns selectee with
      | Some xs => Some (x :: xs)
      | None => None
      end
    | None => None
    end
  end.

Lemma select_app_Some {X : Type} (selector1 selector2 : list nat) (selectee : list X) :
  forall result1 result2,
  select selector1 selectee = Some result1 ->
  select selector2 selectee = Some result2 ->
  select (selector1 ++ selector2) selectee = Some (result1 ++ result2).
Proof.
  revert selector2.
  induction selector1.
  - intros. simpl in *. inversion H. subst. simpl. assumption.
  - intros. simpl in *. destruct (nth_error selectee a) eqn:E.
    + destruct (select selector1 selectee) eqn:E2.
      * inversion H. subst. simpl. 
        rewrite IHselector1 with (selector2 := selector2) (result1 := l) (result2 := result2); auto.
      * inversion H.
    + inversion H.
Qed.

Lemma select_app_None_r {X : Type} (selector1 selector2 : list nat) (selectee : list X) :
  select selector2 selectee = None ->
  select (selector1 ++ selector2) selectee = None.
Proof.
  revert selector2.
  induction selector1.
  + intros. rewrite app_nil_l. assumption.
  + intros. simpl.
    apply IHselector1 in H.
    rewrite H. destruct (nth_error selectee a); auto.
Qed.

Lemma select_defined {X : Type} : forall (selector : list nat) (selectee : list X),
  (forall n, In n selector -> n < length selectee) <->
  exists result, select selector selectee = Some result.
Proof.
  split.
  { induction selector.
  - intros. exists []. auto.
  - intros.
    simpl in H.
    assert (a < length selectee) by (apply H; left; auto).
    assert (forall n, In n selector -> n < length selectee) 
      by (intros; apply H; right; auto).
    clear H.
    specialize (IHselector H1).
    destruct IHselector as [result IH].
    pose proof (nth_error_Some_ex selectee a).
    rewrite H in H0. destruct H0 as [x H0].
    exists (x :: result).
    simpl. rewrite H0. rewrite IH. auto.
  }
  { intros. destruct H as [result H].
    generalize dependent selectee.
    revert result.
    induction selector.
    - simpl in H0. contradiction.
    - intros. simpl in *. destruct H0.
      + subst. destruct (nth_error selectee n) eqn:E.
        * apply nth_error_Some. congruence.
        * congruence.
      + destruct (nth_error selectee a) eqn:E;
        destruct (select selector selectee) eqn:E2; try congruence.
        apply IHselector with (result := l); auto.
  }
Qed.

Lemma select_app_None_l {X : Type} (selector1 selector2 : list nat) (selectee : list X) :
  select selector1 selectee = None ->
  select (selector1 ++ selector2) selectee = None.
Proof.
  intros.
  destruct (select (selector1 ++ selector2) selectee) eqn:E1.
  2 : auto.
  assert (exists result, select (selector1 ++ selector2) selectee = Some result)
    by now exists l.
  rewrite <- select_defined in H0.
  setoid_rewrite in_app_iff in H0.
  assert (forall n, In n selector1 -> n < length selectee) as H1. {
    intros. apply H0. left. auto.
  }
  apply select_defined in H1 as [result1 H1].
  congruence.
Qed.

Lemma select_length {X : Type} : forall (selector : list nat) (selectee : list X) result,
  select selector selectee = Some result ->
  length selector = length result.
Proof.
  induction selector.
  - intros. simpl in *. inversion H. auto.
  - intros. simpl in *. destruct (nth_error selectee a) eqn:E.
    + destruct (select selector selectee) eqn:E2.
      * inversion H. subst. simpl. f_equal. 
        now apply IHselector with (selectee := selectee).
      * inversion H.
    + inversion H.
Qed.

(* collectSome *)

Definition collectSome {X} (l : list (option X)) : list X :=
  flat_map (fun x => match x with Some x => [x] | None => [] end) l.

Lemma collectSome_app {X} : forall (l1 l2 : list (option X)),
  collectSome (l1 ++ l2) = collectSome l1 ++ collectSome l2.
Proof.
  intros. unfold collectSome.
  rewrite flat_map_app. auto.
Qed.

Lemma collectSome_cons {X} : forall (l : list (option X)) (x : option X),
  collectSome (x :: l) = 
    match x with Some x => x :: collectSome l | None => collectSome l end.
Proof.
  intros. unfold collectSome.
  simpl. destruct x; auto.
Qed.

Lemma collectSome_length {X} : forall (l : list (option X)),
  (forall x, In x l -> x <> None)
  -> length (collectSome l) = length l.
Proof.
  intros.
  induction l.
  - auto.
  - simpl. destruct a eqn:E.
    + simpl. f_equal. apply IHl.
      intros. apply H. now right.
    + specialize (H None). simpl in H.
      firstorder.
Qed.

Lemma collectSome_length_le {X} : forall (l : list (option X)),
  length (collectSome l) <= length l.
Proof.
  intros. unfold collectSome.
  induction l.
  - simpl. lia.
  - simpl. destruct a; simpl; lia.
Qed.

Lemma collectSome_in {X} : forall (l : list (option X)) x,
  In x (collectSome l)
  <-> In (Some x) l.
Proof.
  intros.
  split.
  - intros. induction l.
    + simpl in H. tauto.
    + rewrite collectSome_cons in H.
      destruct a eqn:E.
      * simpl in H. destruct H.
        ** subst. constructor. auto.
        ** right. apply IHl. auto.
      * right. apply IHl. auto. 
  - intros. induction l.
    + simpl. tauto.
    + rewrite collectSome_cons.
      destruct a eqn:E.
      * simpl. destruct H.
        ** inversion H. auto.
        ** right. apply IHl. auto.
      * apply IHl. destruct H.
        ** inversion H.
        ** auto.
Qed.

(* maximum *)

Definition maximum (l : list nat) : nat :=
  fold_right max 0 l.

Lemma maximum_app (l1 l2 : list nat) :
  maximum (l1 ++ l2) = max (maximum l1) (maximum l2).
Proof.
  induction l1.
  - auto.
  - simpl. rewrite IHl1. lia.
Qed.

Lemma maximum_in (l : list nat) :
  forall x, In x l -> x <= maximum l.
Proof.
  induction l.
  - intros. simpl in *. tauto.
  - intros. simpl in *. destruct H.
    + subst. lia.
    + specialize (IHl x H). lia.
Qed.

(* unsnoc *)

Fixpoint unsnoc {X : Type} (l : list X) : option (list X * X) :=
  match l with
  | [] => None
  | x :: l' => match unsnoc l' with
    | None => Some ([], x)
    | Some (l'', x') => Some (x :: l'', x')
    end
  end.

Lemma last_inversion {A : Type} : forall (x y : A) xs ys,
    xs ++ [x] = ys ++ [y] -> xs = ys /\ x = y.
Proof.
  intros. apply (f_equal (@rev A)) in H.
  repeat rewrite (rev_app_distr) in H.
  simpl in H. inversion H. apply (f_equal (@rev A)) in H2.
  repeat rewrite rev_involutive in H2.
  auto.
Qed.

Lemma unsnoc_spec {X : Type} : forall (l : list X) (l' : list X),
  (forall x, unsnoc l = Some (l', x) <-> l = l' ++ [x])
  /\ (unsnoc l = None <-> l = []).
Proof.
  induction l.
  - simpl. intros. repeat split. try discriminate.
    intros. destruct l'; discriminate.
  - destruct (unsnoc l) eqn:E.
    + destruct p as [l1 x1].
      intros. split.
      * intros. simpl. rewrite E. 
        specialize (IHl l1).
        destruct IHl as [IHl1 IHl2].
        specialize (IHl1 x1).
        assert (l = l1 ++ [x1]) as H. {
          apply IHl1. auto.
        }
        rewrite H. 
        split. intros.
        ** inversion H0.  auto. 
        ** intros. 
           replace (a :: l1 ++ [x1]) with ((a :: l1) ++ [x1]) in H0 by auto.
           apply last_inversion in H0. destruct H0. subst. auto.
      * intros. split; [ | discriminate].
        simpl. rewrite E. intros. inversion H.
    + simpl.
       assert (l = []) as H. {
        specialize (IHl []) as [IHl1 IHl2].
        apply IHl2. auto.
       }
       subst l. simpl.
       repeat split; try discriminate.
       * intros. inversion H. subst. reflexivity.
       * intros. 
         replace ([a]) with ([] ++ [a]) in H by auto.
         apply last_inversion in H. destruct H. subst. auto.
Qed.

Lemma unsnoc_Some {X : Type} : forall (l : list X) (l' : list X) (x : X),
  (unsnoc l = Some (l', x) <-> l = l' ++ [x]).
Proof.
  intros. apply unsnoc_spec.
Qed.

Lemma unsnoc_None {X : Type} : forall (l : list X),
  (unsnoc l = None <-> l = []).
Proof.
  intros. apply unsnoc_spec. exact [].
Qed.

Lemma unsnoc_Some_ex_ne {X : Type} : forall (l : list X),
  l <> [] -> exists l' x, unsnoc l = Some (l', x).
Proof.
  intros. destruct (unsnoc l) eqn:E.
  - destruct p as [l' x]. exists l', x. auto.
  - rewrite unsnoc_None in E. congruence.
Qed.

Lemma unsonc_Some_ex {X : Type} : forall (x : X) (l : list X),
  exists l' y, unsnoc (x :: l) = Some (l', y).
Proof.
  intros. pose proof (unsnoc_Some_ex_ne (x :: l)) as H.
  specialize (H ltac:(discriminate)).
  auto.
Qed.

Lemma unsnoc_length {X : Type} : forall (l : list X) (l' : list X) (x : X),
  unsnoc l = Some (l', x) -> length l = S (length l').
Proof.
  intros. apply unsnoc_Some in H. subst.
  rewrite app_length. simpl. lia.
Qed.

Definition last_error {X : Type} (l : list X) : option X :=
  match unsnoc l with
  | Some (_, x) => Some x
  | None => None
  end.

Lemma last_error_Some {X : Type} : forall (l : list X) (x : X),
  last_error l = Some x <-> exists l', l = l' ++ [x].
Proof.
  intros. unfold last_error.
  destruct (unsnoc l) eqn:E.
  - destruct p as [l' x'].
    rewrite unsnoc_Some in E. subst.
    split; intros.
    + inversion H. exists l'. auto.
    + destruct H as [l'' H]. 
      apply last_inversion in H. destruct H.
      subst. auto.
  - split.
    + intros. discriminate.
    + intros. destruct H as [l'' H]. subst.
      rewrite unsnoc_None in E. 
      destruct l''; discriminate.
Qed.

(* filter *)

Lemma filter_index : forall {X : Type} (l : list X) (f : X -> bool) (x : X) (i : nat),
  nth_error (filter f l) i = Some x
  -> exists j, 
    nth_error l j = Some x
    /\ i <= j.
Proof.
  induction l.
  { intros. simpl in H. destruct i; inversion H. }
  intros; simpl in H.
  destruct (f a) eqn:Hfa.
  - intros.
    destruct i.
    + simpl in H. inversion H. subst a. clear H.
      exists 0. split; [reflexivity | lia].
    + simpl in H.
      destruct (IHl f x i H) as [j [Hj Hij]].
      exists (S j). split; [assumption | lia].
  - intros.
    destruct (IHl f x i H) as [j [Hj Hij]].
    exists (S j). split; [assumption | lia].
Qed.


Lemma filter_order {X : Type} (l : list X) (f : X -> bool):
  forall x y i j,
    i < j
    -> nth_error (filter f l) i = Some x
    -> nth_error (filter f l) j = Some y
    -> exists i' j',
        i' < j'
     /\ nth_error l i' = Some x
     /\ nth_error l j' = Some y.
Proof.
  induction l.
  { intros. simpl in H0. destruct i; inversion H0. }
  destruct (f a) eqn:Hfa.
  - intros. 
    pose proof (filter_index (a :: l) _ _ _ H0) as [i' [Hi' Hii']].
    pose proof (filter_index (a :: l) _ _ _ H1) as [j' [Hj' Hjj']].
    simpl in H0, H1. rewrite Hfa in H0, H1.
    destruct i.
    + destruct j; [lia | ].
      simpl in H0. inversion H0. subst a. clear H0.
      simpl in H1. exists 0.
      destruct j'; [lia | ].
      exists (S j'). repeat split. lia. assumption. 
    + destruct j; [lia | ].
      simpl in H0, H1.
      destruct (IHl x y i j ltac:(lia) H0 H1) as [i'' [j'' [Hij [Hi'' Hj'']]]].
      exists (S i''). exists (S j''). repeat split.
      lia. assumption. assumption.
  - intros.
    simpl in H0, H1. rewrite Hfa in H0, H1.
    destruct (IHl x y i j ltac:(lia) H0 H1) as [i'' [j'' [Hij [Hi'' Hj'']]]].
    exists (S i''). exists (S j''). repeat split.
    lia. assumption. assumption.
Qed.