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
 *)

From Coq Require Import PeanoNat Lia List Wf_nat Utf8 ssreflect ssrfun ssrbool.

Import ListNotations.

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

Lemma nth_error_skipn {X} : ∀ (xs : list X) i d,
    nth_error xs (i + d) = nth_error (skipn d xs) i.
Proof.
  move=> xs i d.
  rewrite -{1}(firstn_skipn d xs).
  case (Compare_dec.le_gt_dec (length xs) d) => [? | ?].
  - rewrite firstn_all2 // skipn_all2 // app_nil_r.
    have ->: (nth_error (@nil X) i) = @None X by elim i => //.
    apply nth_error_None; lia.
  - rewrite nth_error_app2 firstn_length; f_equal; lia.
Qed.

Lemma nth_error_firstn {X : Type} (l : list X) : ∀ d i,
    i < d → nth_error (firstn d l) i = nth_error l i.
Proof.
  move=> d i Hdi.
  case (Compare_dec.le_gt_dec (length l) d) => [? | ?].
  + rewrite firstn_all2 //; lia.
  + rewrite -{2}(firstn_skipn d l) nth_error_app1 // firstn_length; lia.
Qed.

Lemma firstn_in {X : Type} : ∀ (l : list X) n x, In x (firstn n l) → In x l.
Proof.
  move=> l n x H.
  rewrite -(firstn_skipn n l) in_app_iff; auto.
Qed.

Lemma skipn_in {X : Type} : ∀ (l : list X) n x, In x (skipn n l) → In x l.
Proof.
  move=> l n x H.
  rewrite -(firstn_skipn n l) in_app_iff; auto.
Qed.

Lemma hd_error_skipn {X : Type} (l : list X) : ∀ i,
    hd_error (skipn i l) = nth_error l i.
Proof.
  move: l => /[swap].
  elim => [l | n H []] //.
Qed.

Lemma hd_error_nth_error {X : Type} (l : list X) :
  hd_error l = nth_error l 0.
Proof.
  elim: l => //.
Qed.

Lemma nth_error_rev {A : Type} (l : list A) (n : nat) :
  n < length l → nth_error (rev l) n = nth_error l (length l - S n).
Proof.
  elim: l => // [/Nat.nlt_0_r | a l H H0] //.
  rewrite ? (nth_error_nth' _ a) ? rev_length ? rev_nth //; lia.
Qed.

Lemma map_id {X} : ∀ (xs : list X), map id xs = xs.
Proof.
  elim => //= a l -> //.
Qed.

Lemma combine_map {X Y M N} : ∀ (f : X → M) (g : Y → N) xs ys,
    combine (map f xs) (map g ys) = map (λ '(x, y), (f x, g y)) (combine xs ys).
Proof.
  move=> f g.
  elim => // a l /[swap] [[]] //= a' l' -> //.
Qed.

Lemma combine_app {X Y} : ∀ (xs1 xs2 : list X) (ys1 ys2 : list Y),
    length xs1 = length ys1
    → combine (xs1 ++ xs2) (ys1 ++ ys2) = combine xs1 ys1 ++ combine xs2 ys2.
Proof.
  elim => [? [] // | ? ? /[swap] ? /[swap] [[]] //=
                       ? ? /[swap] ? /[swap] ? -> //]; auto.
Qed.

Lemma combine_rev {X Y} : ∀ (xs : list X) (ys : list Y),
    length xs = length ys → combine (rev xs) (rev ys) = rev (combine xs ys).
Proof.
  elim => [? // | ? ? /[swap] [[]] //= ? ? /[swap] ?].
  rewrite combine_app ? rev_length //; auto => ->; auto.
Qed.

Lemma map_repeat {X Y : Type} (f : X → Y) (x : X) n :
  map f (repeat x n) = repeat (f x) n.
Proof.
  elim: n => // ? /= -> //.
Qed.

Lemma repeat_iff {X : Type} (x : X) l:
  l = repeat x (length l) ↔ (∀ y, In y l → y = x).
Proof.
  split => [-> y /(repeat_spec _ _ y) | ] // H.
  apply Forall_eq_repeat, Forall_forall => y /H -> //.
Qed.

(* zipWith *)

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

Lemma zipWith_length {X Y Z} : ∀ (f : X → Y → Z) xs ys,
    length (zipWith f xs ys) = min (length xs) (length ys).
Proof.
  rewrite /zipWith => *.
  by rewrite map_length combine_length.
Qed.

Lemma zipWith_in {X Y Z} :
  ∀ (P : X → Prop) (Q : Y → Prop) (R : Z → Prop) (f : X → Y → Z) xs ys,
    (∀ x, In x xs → P x) → (∀ y, In y ys → Q y)
    → (∀ x y, P x → Q y → R (f x y)) → ∀ z, In z (zipWith f xs ys) → R z.
Proof.
  move=> ? ? ? ?.
  elim => // ? x ? [] // ? y ? ? ? ?
            [<- | /in_map_iff [[? ?] [<- /[dup] /(in_combine_l x y) ?
                                           /(in_combine_r x y)]]]; intuition.
Qed.

Lemma nth_error_zipWith {X Y Z} : ∀ (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.
  move=> f.
  elim => [ys n | a l H ys n].
  - rewrite /zipWith /=.
    (have: nth_error [] n = None by elim: n) => /[dup] -> -> //.
  - elim: n ys => // [[] | n H0 [ | y l0]] //=.
    + by elim: (nth_error l n).
    + rewrite -H //.
Qed.

Lemma zipWith_cons {X Y Z} : ∀ (f : X → Y → Z) x xs y ys,
    zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys.
Proof.
  reflexivity.
Qed.

Lemma zipWith_repeat_l {X Y Z} : ∀ n (f : X → Y → Z) x ys,
    n >= length ys → zipWith f (repeat x n) ys = map (f x) ys.
Proof.
  elim => [f x [] | n H f x [ | *]] //=; first lia.
  rewrite -H; intuition.
Qed.

Lemma zipWith_repeat_r {X Y Z} : ∀ n (f : X → Y → Z) xs y,
    n >= length xs → zipWith f xs (repeat y n) = map (fun x => f x y) xs.
Proof.
  elim => [f [] | n H f [ | *]] //=; first lia.
  rewrite -H //; intuition.
Qed.

Lemma zipWith_firstn_l {X Y Z} : ∀ (f : X → Y → Z) xs ys,
    zipWith f xs ys = zipWith f xs (firstn (length xs) ys).
Proof.
  rewrite /zipWith => *.
  rewrite combine_firstn_l //.
Qed.

Lemma zipWith_firstn_r {X Y Z} : ∀ (f : X → Y → Z) xs ys,
    zipWith f xs ys = zipWith f (firstn (length ys) xs) ys.
Proof.
  rewrite /zipWith => *.
  rewrite combine_firstn_r //.
Qed.

Lemma zipWith_firstn {X Y Z} : ∀ (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.
  move=> f xs ys.
  case (Nat.le_ge_cases (length xs) (length ys)) =>
         [/Nat.min_l | /Nat.min_r] ->;
           rewrite /= firstn_all -? zipWith_firstn_l -? zipWith_firstn_r //.
Qed.

Lemma zipWith_map {M N X Y Z}:
  ∀ (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 (λ '(x, y), f (g x) (h y)) (combine xs ys).
Proof.
  rewrite /zipWith => *.
  rewrite combine_map map_map.
  apply map_ext => [[]] //.
Qed.

Lemma zipWith_assoc {X}: ∀ (f : X → X → X) xs ys zs,
    (∀ 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.
  move=> f.
  elim/(induction_ltof1 _ (@length X)); rewrite /ltof => [[]] =>
        [? | ? ? H [ | ? ? [ | ? ? H0]]] //=.
  rewrite ? zipWith_cons H0 H //.
Qed.

Lemma zipWith_ext { X Y Z M N } : ∀ (f : X → Y → Z) (g : M → N → Z) xs ys ms ns,
    (∀ 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.
  move=> f g.
  elim/(induction_ltof1 _ (@length X)); rewrite /ltof => [[]] =>
        [? ? [] | ? ? H /[swap] [[ | ? ? [[] | ? ? [] ? ? H0]]]] //= *.
  rewrite ? zipWith_cons.
  f_equal; try (apply H; intuition); apply H0; firstorder.
Qed.

Lemma zipWith_cons_singleton {X} : ∀ (xs : list X) (xss : list (list X)),
    zipWith cons xs xss = zipWith (@app X) (map (fun x => [x]) xs) xss.
Proof.
  move=> xs xss.
  apply zipWith_ext; rewrite ? map_length //.
  elim: xs xss => [? | ? ? H [ | ? ? ? ? ? ? [[] -> -> <- -> | ]]] //.
  apply H.
Qed.

Lemma zipWith_rev {X Y Z} : ∀ (f : X → Y → Z) xs ys,
    length xs = length ys → zipWith f (rev xs) (rev ys) = rev (zipWith f xs ys).
Proof.
  rewrite /zipWith => f xs ys H.
  rewrite combine_rev // 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 (λ x y, g (f x y)) xs ys.
Proof.
  rewrite {2}/zipWith map_map.
  apply map_ext_in => [[x y]] //.
Qed.

Lemma zipWith_ext_id_l {X Y} (f : X → Y → X) (xs : list X) (ys : list Y) :
  (∀ x y, In (x, y) (combine xs ys) → f x y = x)
  → length xs <= length ys → zipWith f xs ys = xs.
Proof.
  elim/(induction_ltof1 _ (@length X)): xs ys; rewrite /ltof =>
        [[]] // ? ? H [ | ? ? H0 ?] //=; first lia.
  rewrite zipWith_cons.
  f_equal; try (apply H; intuition); apply H0; firstorder.
Qed.

Lemma zipWith_ext_id_r {X Y} (f : X → Y → Y) (xs : list X) (ys : list Y) :
  (∀ x y, In (x, y) (combine xs ys) → f x y = y)
  → length xs >= length ys → zipWith f xs ys = ys.
Proof.
  elim/(induction_ltof1 _ (@length X)): xs ys; rewrite /ltof =>
        [[? [] | ? ? H [ | ? ? H0 ?]]] //=; first lia.
  rewrite zipWith_cons.
  f_equal; try (apply H; intuition); apply H0; firstorder.
Qed.

(* transpose *)

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

Lemma transpose_length {X : Type} : ∀ len (tapes : list (list X)),
    (∀ t, In t tapes → length t >= len)
    → length (transpose len tapes) = len.
Proof.
  move=> /[swap].
  elim => [len H | ]; rewrite ? repeat_length //= => a l H len H0.
  rewrite zipWith_length H; try apply Nat.min_r; firstorder.
Qed.

Lemma transpose_inner_length {X : Type}: ∀ len (tapes : list (list X)),
  ∀ u, In u (transpose len tapes) → length u = length tapes.
Proof.
  move=> /[swap].
  elim => [len u /= /(repeat_spec _ []) -> | ] // a l ? len ?.
  rewrite /zipWith in_map_iff =>
            [[[? ?] [<- /(in_combine_r a (transpose len l))]]] /=.
  firstorder.
Qed.

Lemma transpose_inner_length_eq {X : Type} : ∀ len (tapes : list (list X)),
  ∀ u v, In u (transpose len tapes) → In v (transpose len tapes)
         → length u = length v.
Proof.
  move=> ? ? ? ? /transpose_inner_length -> /transpose_inner_length //.
Qed.

Lemma transpose_app {X : Type} : ∀ len (tapes1 tapes2 : list (list X)),
    (∀ t, In t tapes1 → length t >= len) → (∀ t, In t tapes2 → length t >= len)
    → transpose len (tapes1 ++ tapes2) =
        zipWith (@app X) (transpose len tapes1) (transpose len tapes2).
Proof.
  move=> len.
  elim => [? ? ? | ? ? H ? ? ?] //=.
  - rewrite zipWith_repeat_l ? transpose_length // -{1}(map_id (transpose _ _)).
    auto using map_ext.
  - rewrite H ? zipWith_cons_singleton ? zipWith_assoc; intuition.
Qed.

Lemma transpose_singleton {X : Type} : ∀ (t : list X),
    transpose (length t) [t] = map (fun x => [x]) t.
Proof.
  rewrite /transpose => t.
  rewrite zipWith_repeat_r //.
Qed.

Lemma transpose_rev_aux {X : Type} : ∀ (xss : list (list X)) (l : list X),
    (∀ 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.
  elim => [[] ? | ? ? H [ | ? ? /= ?]] //.
  rewrite zipWith_cons H; firstorder.
Qed.

Lemma transpose_rev {X : Type} : ∀ len (tapes : list (list X)),
    (∀ t, In t tapes → length t = len)
    → transpose len (rev tapes) = map (@rev X) (transpose len tapes).
Proof.
  move=> len.
  elim => [H | a l H /[dup] H0 /(_ a) H1] /=.
  - rewrite -{1}(map_id (repeat [] len)).
    apply map_ext_in => a /(repeat_spec len []) -> //.
  - (rewrite transpose_app => [t /(in_rev l) H2 | t /= [<- | ] | ] //);
    rewrite ? H0 ? H ? zipWith_cons_singleton; intuition.
    rewrite -H1 ? transpose_singleton ? transpose_rev_aux //; intuition.
    eauto using transpose_inner_length_eq.
Qed.

Lemma transpose_zipWith_cons {X : Type} : ∀ len (mat : list (list X)) t,
    (∀ u, In u mat → length u >= len) → length t = length mat
    → transpose (S len) (zipWith cons t mat) = t :: transpose len mat.
Proof.
  move=> /[swap].
  elim => [len [] | ? ? H ? [ | ? ? /= ? ?]] //.
  rewrite H; intuition.
Qed.


Lemma transpose_involutive {X : Type} : ∀ len (tapes : list (list X)),
    (∀ t, In t tapes → length t = len)
    → transpose (length tapes) (transpose len tapes) = tapes.
Proof.
  move=> /[swap].
  elim => [[] | a l H len H0] //=.
  rewrite transpose_zipWith_cons /= ? transpose_length =>
            [u /transpose_inner_length -> | t ? | | ] //;
              rewrite ? H0 ? H; intuition.
Qed.

Lemma transpose_rev2 {X : Type} : ∀ len (tapes : list (list X)),
    (∀ t, In t tapes → length t = len)
    → rev (transpose len tapes) = transpose len (map (@rev X) tapes).
Proof.
  move=> len tapes H.
  move: (@transpose_rev X _ _ (transpose_inner_length len tapes)).
  rewrite transpose_involutive // => /(f_equal (λ x, transpose len x)).
  rewrite -{1}(transpose_length len tapes) => [? /H -> | ] //.
  rewrite -rev_length transpose_involutive // => ?.
  rewrite -in_rev => /transpose_inner_length //.
Qed.

Lemma transpose_firstn {X : Type} : ∀ len (tapes : list (list X)) n,
    (∀ t, In t tapes → length t >= len)
    → transpose len (firstn n tapes) = map (firstn n) (transpose len tapes).
Proof.
  move=> ? tapes n H.
  case (Compare_dec.le_gt_dec n (length tapes)) => [? | ?].
  - rewrite -{2}(firstn_skipn n tapes) transpose_app ? zipWith_map2
               ? zipWith_ext_id_l ? transpose_length // =>
              [? /(firstn_in tapes) /H | ? /(skipn_in tapes) /H |
                ? ? /(in_combine_l (transpose _ _) (transpose _ _))
                  /transpose_inner_length |
                ? /(firstn_in tapes) /H | ? /(skipn_in tapes) /H] //.
    rewrite firstn_app firstn_length Nat.min_l // => <-.
    rewrite Nat.sub_diag firstn_O firstn_all app_nil_r //.
  - rewrite firstn_all2; intuition.
    rewrite (map_ext_in _ id) ? map_id // => a /transpose_inner_length ?.
    rewrite firstn_all2; intuition lia.
Qed.

Lemma transpose_skipn {X : Type} : ∀ len (tapes : list (list X)) n,
    (∀ t, In t tapes → length t >= len)
    → transpose len (skipn n tapes) = map (skipn n) (transpose len tapes).
Proof.
  move=> len tapes n Hlen.
  case (Compare_dec.le_gt_dec n (length tapes)) => [? | Hn].
  - rewrite -{2}(firstn_skipn n tapes) transpose_app ? zipWith_map2
               ? zipWith_ext_id_r ? transpose_length // =>
              [t /(firstn_in tapes) /Hlen | t /(skipn_in tapes) /Hlen |
                x y /(in_combine_l (transpose _ _) (transpose _ _))
                  /transpose_inner_length |
                t /(firstn_in tapes) /Hlen | t /(skipn_in tapes) /Hlen] //.
    rewrite skipn_app firstn_length Nat.min_l // => <-.
    rewrite Nat.sub_diag skipn_O skipn_all app_nil_l //.
  - rewrite skipn_all2; intuition.
    elim: tapes Hlen Hn => /= [ | a l ? ? ?];
                           first (rewrite map_repeat; by elim: n).
    rewrite zipWith_map2 /zipWith (map_ext_in _ (λ x, [])) =>
              [[] ? ? /[dup] /(in_combine_l a (transpose _ _)) ?
                 /(in_combine_r a (transpose _ _)) /transpose_inner_length ?
              | ]; first (apply skipn_all2 => /=; lia).
    set (rhs := (map _ (combine _ _))).
    (have ->: rhs = repeat [] (length rhs); rewrite ? repeat_iff ? map_length)
    => [y /in_map_iff [? []] // | ].
    have {1}<-: (length (combine a (transpose len l)) = len);
      rewrite ? combine_length ? transpose_length ? Nat.min_r //; firstorder.
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.
  elim: xss xs => [[] | ? ? H [/= /Nat.nle_succ_0 | ? ? /= /le_S_n /H ->]] //.
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.
  rewrite /ij_error nth_error_skipn //.
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.
  rewrite /ij_error.
  remember (nth_error l i) as row_i.
  destruct row_i.
  - remember (nth_error (map (skipn d) l) i) as row_i'.
    (destruct row_i'; move: Heqrow_i') =>
      [ | /(@eq_sym (option (list X))) /nth_error_None];
      last rewrite nth_error_None map_length => /Gt.le_not_gt [].
    + rewrite nth_error_map -Heqrow_i /= => [[]] ->.
      rewrite nth_error_skipn //.
    + apply nth_error_Some.
      rewrite -Heqrow_i //.
  - move: Heqrow_i => /(@eq_sym (option (list X))) /nth_error_None.
    rewrite -(map_length (skipn d) l) => /nth_error_None -> //.
Qed.

Lemma transpose_spec_0 {X : Type} : ∀ (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.
  elim => [? [] | ? ? H xss [ | ?]] //; rewrite /ij_error;
          case: xss => [/(@eq_sym nat) /Nat.neq_succ_0 | ? l ?] //.
  rewrite zipWith_cons /= (H l); intuition.
Qed.

Lemma transpose_spec {X : Type} : ∀ len (tapes : list (list X)),
    (∀ t, In t tapes → length t = len)
    → ∀ i j, ij_error i j tapes = ij_error j i (transpose len tapes).
Proof.
  move=> len.
  elim => [? | ? ? IHt H [ | ?] ?].
  - (case => [ | ?] j; rewrite /ij_error; case (Compare_dec.le_gt_dec len j));
      by [rewrite -{1}(@repeat_length (list X) [] len) => /nth_error_None -> //
         | move=> /(nth_error_repeat []) -> //].
  - rewrite -transpose_spec_0 ? transpose_length =>
              [? ? | | ]; rewrite ? H; intuition.
  - rewrite -Nat.add_1_r ij_error_remove_cols ij_error_remove_rows /=
               IHt ? skipn_zipWith_cons ? transpose_length // =>
              [? ? | ? ? | ]; rewrite H; intuition.
Qed.