From Typonomikon Require Export D5a.

Lemma isEmpty_pmap_false :
  forall (A B : Type) (f : A -> option B) (l : list A),
    isEmpty (pmap f l) = false -> isEmpty l = false.

Lemma isEmpty_pmap_true :
  forall (A B : Type) (f : A -> option B) (l : list A),
    isEmpty l = true -> isEmpty (pmap f l) = true.

Lemma length_pmap :
  forall (A B : Type) (f : A -> option B) (l : list A),
    length (pmap f l) <= length l.

Lemma pmap_snoc :
  forall (A B : Type) (f : A -> option B) (x : A) (l : list A),
    pmap f (snoc x l) =
    match f x with
    | None => pmap f l
    | Some b => snoc b (pmap f l)
    end.

Lemma pmap_app :
  forall (A B : Type) (f : A -> option B) (l1 l2 : list A),
    pmap f (l1 ++ l2) = pmap f l1 ++ pmap f l2.

Lemma pmap_rev :
  forall (A B : Type) (f : A -> option B) (l : list A),
    pmap f (rev l) = rev (pmap f l).

Lemma pmap_map :
  forall (A B C : Type) (f : A -> B) (g : B -> option C) (l : list A),
    pmap g (map f l) = pmap (fun x : A => g (f x)) l.

Lemma pmap_join :
  forall (A B : Type) (f : A -> option B) (l : list (list A)),
    pmap f (join l) = join (map (pmap f) l).

Lemma pmap_bind :
  forall (A B C : Type) (f : A -> list B) (g : B -> option C) (l : list A),
    pmap g (bind f l) = bind (fun x : A => pmap g (f x)) l.

Lemma pmap_replicate :
  forall (A B : Type) (f : A -> option B) (n : nat) (x : A),
    pmap f (replicate n x) =
    match f x with
    | None => []
    | Some y => replicate n y
    end.

Definition isSome {A : Type} (x : option A) : bool :=
match x with
| None => false
| _ => true
end.

Lemma head_pmap :
  forall (A B : Type) (f : A -> option B) (l : list A),
    head (pmap f l) =
    match find isSome (map f l) with
    | None => None
    | Some x => x
    end.

Lemma pmap_zip :
  exists
    (A B C : Type)
    (fa : A -> option C) (fb : B -> option C)
    (la : list A) (lb : list B),
      pmap
        (fun '(a, b) =>
        match fa a, fb b with
        | Some a', Some b' => Some (a', b')
        | _, _ => None
        end)
        (zip la lb) <>
      zip (pmap fa la) (pmap fb lb).

Lemma any_pmap :
  forall (A B : Type) (f : A -> option B) (p : B -> bool) (l : list A),
    any p (pmap f l) =
    any
      (fun x : A =>
      match f x with
      | Some b => p b
      | None => false
      end)
      l.

Lemma all_pmap :
  forall (A B : Type) (f : A -> option B) (p : B -> bool) (l : list A),
    all p (pmap f l) =
    all
      (fun x : A =>
      match f x with
      | Some b => p b
      | None => true
      end)
      l.

Lemma find_pmap :
  forall (A B : Type) (f : A -> option B) (p : B -> bool) (l : list A),
    find p (pmap f l) =
    let oa :=
      find (fun x : A => match f x with Some b => p b | _ => false end) l
    in
    match oa with
    | Some a => f a
    | None => None
    end.

Lemma findLast_pmap :
  forall (A B : Type) (f : A -> option B) (p : B -> bool) (l : list A),
    findLast p (pmap f l) =
    let oa :=
      findLast
        (fun x : A => match f x with Some b => p b | _ => false end) l
    in
    match oa with
    | Some a => f a
    | None => None
    end.

Lemma count_pmap :
  forall (A B : Type) (f : A -> option B) (p : B -> bool) (l : list A),
    count p (pmap f l) =
    count
      (fun x : A =>
      match f x with
      | Some b => p b
      | None => false
      end)
      l.


Definition aux {A B : Type} (p : B -> bool) (f : A -> option B)
  (dflt : bool) (x : A) : bool :=
match f x with
| Some b => p b
| None => dflt
end.

Lemma pmap_filter :
  forall (A B : Type) (p : B -> bool) (f : A -> option B) (l : list A),
    filter p (pmap f l) =
    pmap f (filter (aux p f false) l).

Lemma pmap_takeWhile :
  forall (A B : Type) (p : B -> bool) (f : A -> option B) (l : list A),
    takeWhile p (pmap f l) =
    pmap f
      (takeWhile
        (fun x : A => match f x with | Some b => p b | _ => true end)
        l).

Lemma pmap_dropWhile :
  forall (A B : Type) (p : B -> bool) (f : A -> option B) (l : list A),
    dropWhile p (pmap f l) =
    pmap f
      (dropWhile
        (fun x : A => match f x with | Some b => p b | _ => true end)
        l).

Lemma pmap_span :
  forall (A B : Type) (f : A -> option B) (p : B -> bool) (l : list A),
    match
      span
        (fun x : A => match f x with None => false | Some b => p b end)
        l
    with
    | None => True
    | Some (b, x, e) =>
        exists y : B, f x = Some y /\
          span p (pmap f l) = Some (pmap f b, y, pmap f e)
    end.

Lemma pmap_nth_findIndices :
  forall (A : Type) (p : A -> bool) (l : list A),
    pmap (fun n : nat => nth n l) (findIndices p l) =
    filter p l.

Lemma mask_nil :
  forall {A : Type} (f : A -> A) (bs : list bool),
    mask f bs [] = [].

Lemma isEmpty_mask :
  forall {A : Type} (f : A -> A) (bs : list bool) (l : list A),
    isEmpty (mask f bs l) = isEmpty l.

Lemma length_mask :
  forall {A : Type} (f : A -> A) (bs : list bool) (l : list A),
    length (mask f bs l) = length l.

Lemma mask_app_r :
  forall {A : Type} (f : A -> A) (bs : list bool) (l1 l2 : list A),
    mask f bs (l1 ++ l2) = mask f bs l1 ++ mask f (drop (length l1) bs) l2.

Lemma mask_app_l :
  forall {A : Type} (f : A -> A) (bs1 bs2 : list bool) (l : list A),
    mask f (bs1 ++ bs2) l = mask f (replicate (length bs1) false ++ bs2) (mask f bs1 l).

Lemma mask_app_l' :
  forall {A : Type} (f : A -> A) (bs1 bs2 : list bool) (l : list A),
    mask f (bs1 ++ bs2) l
      =
    mask f bs1 (take (length bs1) l) ++ mask f bs2 (drop (length bs1) l).

Lemma mask_replicate_true :
  forall {A : Type} (f : A -> A) (n : nat) (l : list A),
    mask f (replicate n true) l = map f (take n l) ++ drop n l.

Lemma mask_replicate_false :
  forall {A : Type} (f : A -> A) (n : nat) (l : list A),
    mask f (replicate n false) l = l.

Lemma take_mask :
  forall {A : Type} (n : nat) (f : A -> A) (bs : list bool) (l : list A),
    take n (mask f bs l) = mask f bs (take n l).

Lemma take_mask' :
  forall {A : Type} (n : nat) (f : A -> A) (bs : list bool) (l : list A),
    take n (mask f bs l) = mask f (take n bs) (take n l).

Lemma drop_mask :
  forall {A : Type} (n : nat) (f : A -> A) (bs : list bool) (l : list A),
    drop n (mask f bs l) = mask f (drop n bs) (drop n l).

Lemma nth_mask :
  forall {A : Type} (n : nat) (f : A -> A) (bs : list bool) (l : list A),
    nth n (mask f bs l)
      =
    match nth n bs with
    | None => nth n l
    | Some false => nth n l
    | Some true =>
      match nth n l with
      | None => None
      | Some x => Some (f x)
      end
    end.

Lemma mask_zipWith :
  forall {A : Type} (f : A -> A) (bs : list bool) (l : list A),
    mask f bs l = zipWith (fun (b : bool) (x : A) => if b then f x else x) bs l.

Lemma length_mask' :
  forall {A : Type} (f : A -> A) (l : list A) (bs : list bool),
    length (mask' f l bs) = min (length bs) (length l).

Lemma imap_id :
  forall {A : Type} (l : list A),
    imap (fun _ x => x) l = l.

Lemma imap_imp :
  forall {A B C : Type} (f : nat -> A -> B) (g : nat -> B -> C) (l : list A),
    imap g (imap f l) = imap (fun n a => g n (f n a)) l.

Lemma isEmpty_imap :
  forall (A B : Type) (f : nat -> A -> B) (l : list A),
    isEmpty (imap f l) = isEmpty l.

Lemma length_imap :
  forall (A B : Type) (f : nat -> A -> B) (l : list A),
    length (imap f l) = length l.

Lemma imap_snoc :
  forall (A B : Type) (f : nat -> A -> B) (x : A) (l : list A),
    imap f (snoc x l) = snoc (f (length l) x) (imap f l).

Lemma imap_app :
  forall (A B : Type) (f : nat -> A -> B) (l1 l2 : list A),
    imap f (l1 ++ l2) = imap f l1 ++ imap (fun n x => f (length l1 + n) x) l2.

Lemma imap_rev :
  forall (A B : Type) (f : nat -> A -> B) (l : list A),
    imap f (rev l) = rev (imap (fun n x => f (length l - S n) x) l).

Lemma imap_ext :
  forall (A B : Type) (f g : nat -> A -> B) (l : list A),
    (forall (n : nat) (a : A), f n a = g n a) ->
      imap f l = imap g l.

Lemma head_imap :
  forall (A B : Type) (f : nat -> A -> B) (l : list A),
    head (imap f l) =
    match l with
    | [] => None
    | h :: _ => Some (f 0 h)
    end.

Lemma tail_imap :
  forall (A B : Type) (f : nat -> A -> B) (l : list A),
    tail (imap f l) =
    match l with
    | [] => None
    | _ :: t => Some (imap (fun n a => f (S n) a) t)
    end.

Lemma init_imap :
  forall (A B : Type) (f : nat -> A -> B) (l : list A),
    init (imap f l) =
    match l with
    | [] => None
    | h :: t =>
      match init t with
      | None => Some []
      | Some i => Some (imap f (h :: i))
      end
    end.

Lemma nth_imap_Some :
  forall (A B : Type) (f : nat -> A -> B) (l : list A) (n : nat) (x : A),
    nth n l = Some x -> nth n (imap f l) = Some (f n x).

Lemma nth_imap :
  forall (A B : Type) (f : nat -> A -> B) (l : list A) (n : nat),
    nth n (imap f l) =
    match nth n l with
    | None => None
    | Some x => Some (f n x)
    end.

Lemma take_imap :
  forall (A B : Type) (f : nat -> A -> B) (l : list A) (n : nat),
    take n (imap f l) = imap f (take n l).

Lemma zip_imap :
  forall (A B A' B' : Type) (f : nat -> A -> A') (g : nat -> B -> B')
  (la : list A) (lb : list B),
    zip (imap f la) (imap g lb) =
    imap (fun n x => (f n (fst x), g n (snd x))) (zip la lb).

Lemma isEmpty_intersperse :
  forall (A : Type) (x : A) (l : list A),
    isEmpty (intersperse x l) = isEmpty l.

Lemma length_intersperse :
  forall (A : Type) (x : A) (l : list A),
    length (intersperse x l) = 2 * length l - 1.

Lemma intersperse_snoc :
  forall (A : Type) (x y : A) (l : list A),
    intersperse x (snoc y l) =
    if isEmpty l then [y] else snoc y (snoc x (intersperse x l)).

Lemma intersperse_app :
  forall (A : Type) (x : A) (l1 l2 : list A),
    intersperse x (l1 ++ l2) =
    match l1, l2 with
    | [], _ => intersperse x l2
    | _, [] => intersperse x l1
    | h1 :: t1, h2 :: t2 =>
        intersperse x l1 ++ x :: intersperse x l2
    end.

Lemma intersperse_app_cons :
  forall (A : Type) (x : A) (l1 l2 : list A),
    l1 <> [] -> l2 <> [] ->
      intersperse x (l1 ++ l2) = intersperse x l1 ++ x :: intersperse x l2.

Lemma intersperse_rev :
  forall (A : Type) (x : A) (l : list A),
    intersperse x (rev l) = rev (intersperse x l).

Lemma intersperse_map :
  forall (A B : Type) (f : A -> B) (l : list A) (a : A) (b : B),
    f a = b -> intersperse b (map f l) = map f (intersperse a l).

Lemma head_intersperse :
  forall (A : Type) (x : A) (l : list A),
    head (intersperse x l) = head l.

Lemma last_intersperse :
  forall (A : Type) (x : A) (l : list A),
    last (intersperse x l) = last l.

Lemma tail_intersperse :
  forall (A : Type) (x : A) (l : list A),
    tail (intersperse x l) =
    match tail l with
    | None => None
    | Some [] => Some []
    | Some (h :: t) => tail (intersperse x l)
    end.

Lemma nth_intersperse_even :
  forall (A : Type) (x : A) (l : list A) (n : nat),
    n < length l ->
      nth (2 * n) (intersperse x l) = nth n l.

Lemma nth_intersperse_odd :
  forall (A : Type) (x : A) (l : list A) (n : nat),
    0 < n -> n < length l ->
      nth (2 * n - 1) (intersperse x l) = Some x.

Lemma intersperse_take :
  forall (A : Type) (x : A) (l : list A) (n : nat),
    intersperse x (take n l) =
    take (2 * n - 1) (intersperse x l).

Lemma any_intersperse :
  forall (A : Type) (p : A -> bool) (x : A) (l : list A),
    any p (intersperse x l) =
    orb (any p l) (andb (2 <=? length l) (p x)).

Lemma all_intersperse :
  forall (A : Type) (p : A -> bool) (x : A) (l : list A),
    all p (intersperse x l) =
    all p l && ((length l <=? 1) || p x).

Lemma findIndex_intersperse :
  forall (A : Type) (p : A -> bool) (x : A) (l : list A),
    findIndex p (intersperse x l) =
    if p x
    then
      match l with
      | [] => None
      | [h] => if p h then Some 0 else None
      | h :: t => if p h then Some 0 else Some 1
      end
    else
      match findIndex p l with
      | None => None
      | Some n => Some (2 * n)
      end.

Lemma count_intersperse :
  forall (A : Type) (p : A -> bool) (x : A) (l : list A),
    count p (intersperse x l) =
    count p l + if p x then length l - 1 else 0.

Lemma filter_intersperse_false :
  forall (A : Type) (p : A -> bool) (x : A) (l : list A),
    p x = false -> filter p (intersperse x l) = filter p l.

Lemma pmap_intersperse :
  forall (A B : Type) (f : A -> option B) (x : A) (l : list A),
    f x = None -> pmap f (intersperse x l) = pmap f l.

Lemma interleave_nil_r :
  forall {A : Type} (l : list A),
    interleave l [] = l.

Lemma isEmpty_interleave :
  forall {A : Type} (l1 l2 : list A),
    isEmpty (interleave l1 l2) = isEmpty l1 && isEmpty l2.

Lemma len_interleave :
  forall {A : Type} (l1 l2 : list A),
    length (interleave l1 l2) = length l1 + length l2.

Lemma map_interleave :
  forall {A B : Type} (f : A -> B) (l1 l2 : list A),
    map f (interleave l1 l2) = interleave (map f l1) (map f l2).

Lemma any_interleave :
  forall {A : Type} (p : A -> bool) (l1 l2 : list A),
    any p (interleave l1 l2) = any p l1 || any p l2.

Lemma all_interleave :
  forall {A : Type} (p : A -> bool) (l1 l2 : list A),
    all p (interleave l1 l2) = all p l1 && all p l2.

Lemma count_interleave :
  forall {A : Type} (p : A -> bool) (l1 l2 : list A),
    count p (interleave l1 l2) = count p l1 + count p l2.

Lemma head_groupBy :
  forall (A : Type) (p : A -> A -> bool) (l : list A),
    ~ head (groupBy p l) = Some [].

Lemma head_groupBy' :
  forall (A : Type) (p : A -> A -> bool) (l : list A),
    head (groupBy p l) = None
    \/
    exists (h : A) (t : list A),
      head (groupBy p l) = Some (h :: t).

Lemma groupBy_is_nil :
  forall (A : Type) (p : A -> A -> bool) (l : list A),
    groupBy p l = [] -> l = [].

Lemma isEmpty_groupBy :
  forall (A : Type) (p : A -> A -> bool) (l : list A),
    isEmpty (groupBy p l) = isEmpty l.

Lemma length_groupBy :
  forall (A : Type) (p : A -> A -> bool) (l : list A),
    length (groupBy p l) <= length l.

Ltac gb :=
match goal with
| H : groupBy _ ?l = [] |- _ =>
  apply (f_equal isEmpty) in H;
  rewrite isEmpty_groupBy in H;
  destruct l; inversion H; subst
| H : groupBy _ _ = [] :: _ |- _ =>
  apply (f_equal head), head_groupBy in H; contradiction
end; cbn; try congruence.

Require Import Arith.

Lemma groupBy_decomposition :
  forall (A : Type) (p : A -> A -> bool) (l : list A),
    l = [] \/ exists n : nat,
      groupBy p l = take n l :: groupBy p (drop n l).

Lemma groupBy_cons :
  forall (A : Type) (p : A -> A -> bool) (l h : list A) (t : list (list A)),
    groupBy p l = h :: t -> groupBy p h = [h].

Lemma groupBy_app_decomposition :
  forall (A : Type) (p : A -> A -> bool) (l : list A),
    groupBy p l = [] \/
    groupBy p l = [l] \/
    exists l1 l2 : list A,
      l = l1 ++ l2 /\
      groupBy p l = groupBy p l1 ++ groupBy p l2.

Lemma groupBy_middle :
  forall (A : Type) (p : A -> A -> bool) (l1 l2 : list A) (x y : A),
    p x y = false ->
      groupBy p (l1 ++ x :: y :: l2) =
      groupBy p (l1 ++ [x]) ++ groupBy p (y :: l2).

Lemma groupBy_app :
  forall (A : Type) (p : A -> A -> bool) (l1 l2 : list A) (x y : A),
    last l1 = Some x -> head l2 = Some y -> p x y = false ->
      groupBy p (l1 ++ l2) = groupBy p l1 ++ groupBy p l2.

Lemma groupBy_app' :
  forall (A : Type) (p : A -> A -> bool) (l1 l2 : list A),
    groupBy p (l1 ++ l2) =
    match last l1, head l2 with
    | None, _ => groupBy p l2
    | _, None => groupBy p l1
    | Some x, Some y =>
      if p x y
      then groupBy p (l1 ++ l2)
      else groupBy p l1 ++ groupBy p l2
    end.

Lemma groupBy_singl :
  forall (A : Type) (p : A -> A -> bool) (x : A) (l : list A),
    groupBy p l = [[x]] -> l = [x].

Lemma groupBy_rev_aux :
  forall (A : Type) (p : A -> A -> bool) (l : list A),
    (forall x y : A, p x y = p y x) ->
      groupBy p l = rev (map rev (groupBy p (rev l))).

Lemma rev_groupBy :
  forall (A : Type) (p : A -> A -> bool) (l : list A),
    (forall x y : A, p x y = p y x) ->
      rev (groupBy p l) = map rev (groupBy p (rev l)).

Lemma groupBy_rev :
  forall (A : Type) (p : A -> A -> bool) (l : list A),
    (forall x y : A, p x y = p y x) ->
      groupBy p (rev l) = rev (map rev (groupBy p l)).

Lemma groupBy_map :
  forall (A B : Type) (f : A -> B) (p : B -> B -> bool) (l : list A),
    groupBy p (map f l) =
    map (map f) (groupBy (fun x y => p (f x) (f y)) l).

Lemma map_groupBy_groupBy :
  forall (A : Type) (p : A -> A -> bool) (l : list A),
    map (groupBy p) (groupBy p l) =
    map (fun x => [x]) (groupBy p l).

Lemma join_groupBy :
  forall (A : Type) (p : A -> A -> bool) (l : list A),
    join (groupBy p l) = l.

Lemma groupBy_replicate :
  forall (A : Type) (p : A -> A -> bool) (n : nat) (x : A),
    groupBy p (replicate n x) =
    if isZero n
    then []
    else if p x x then [replicate n x] else replicate n [x].

Lemma groupBy_take :
  exists (A : Type) (p : A -> A -> bool) (l : list A) (n : nat),
    forall m : nat,
      groupBy p (take n l) <> take m (groupBy p l).

Lemma any_groupBy :
  forall (A : Type) (q : A -> bool) (p : A -> A -> bool) (l : list A),
    any (any q) (groupBy p l) = any q l.

Lemma all_groupBy :
  forall (A : Type) (q : A -> bool) (p : A -> A -> bool) (l : list A),
    all (all q) (groupBy p l) = all q l.

Lemma find_groupBy :
  forall (A : Type) (q : A -> bool) (p : A -> A -> bool) (l : list A),
    find q l =
    match find (any q) (groupBy p l) with
    | None => None
    | Some g => find q g
    end.

Module insertBefore.

Fixpoint insertBefore {A : Type} (n : nat) (l1 l2 : list A) : list A :=
match n with
| 0 => l2 ++ l1
| S n' =>
  match l1 with
  | [] => l2
  | h :: t => h :: insertBefore n' t l2
  end
end.

Notation "'insert' l2 'before' n 'in' l1" :=
  (insertBefore n l1 l2) (at level 40).

Lemma insert_nil_before :
  forall (A : Type) (n : nat) (l : list A),
    (insert [] before n in l) = l.

Lemma insert_before_in_nil:
  forall (A : Type) (n : nat) (l : list A),
    (insert l before n in []) = l.

Lemma insert_before_in_char :
  forall (A : Type) (l1 l2 : list A) (n : nat),
    insert l2 before n in l1 =
    take n l1 ++ l2 ++ drop n l1.

Lemma isEmpty_insertBefore :
  forall (A : Type) (n : nat) (l1 l2 : list A),
    isEmpty (insert l2 before n in l1) =
    andb (isEmpty l1) (isEmpty l2).

Lemma length_insertBefore :
  forall (A : Type) (n : nat) (l1 l2 : list A),
    length (insert l2 before n in l1) =
    length l1 + length l2.

Lemma insert_before_0 :
  forall (A : Type) (l1 l2 : list A),
    insert l2 before 0 in l1 = l2 ++ l1.

Lemma insert_before_gt :
  forall (A : Type) (n : nat) (l1 l2 : list A),
    length l1 <= n -> insert l2 before n in l1 = l1 ++ l2.

Lemma insert_before_length :
  forall (A : Type) (l1 l2 : list A),
    insert l2 before length l1 in l1 = l1 ++ l2.

Lemma insert_before_length_in_app :
  forall (A : Type) (l1 l2 l : list A),
    insert l before length l1 in (l1 ++ l2) =
    l1 ++ l ++ l2.

Lemma insert_before_le_in_app :
  forall (A : Type) (n : nat) (l1 l2 l3 : list A),
    n <= length l1 ->
      insert l3 before n in (l1 ++ l2) =
      (insert l3 before n in l1) ++ l2.

Lemma insert_app_before :
  forall (A : Type) (n : nat) (l1 l2 l : list A),
    insert l1 ++ l2 before n in l =
    insert l2 before (n + length l1) in (insert l1 before n in l).

Lemma insert_before_plus_in_app :
  forall (A : Type) (l1 l2 l3 : list A) (n : nat),
    insert l3 before (length l1 + n) in (l1 ++ l2) =
    l1 ++ insert l3 before n in l2.

Lemma rev_insert_before :
  forall (A : Type) (n : nat) (l1 l2 : list A),
    rev (insert l2 before n in l1) =
    insert (rev l2) before (length l1 - n) in rev l1.

Lemma insert_before_in_rev :
  forall (A : Type) (n : nat) (l1 l2 : list A),
    insert l2 before n in rev l1 =
    rev (insert rev l2 before (length l1 - n) in l1).

Lemma insert_rev_before :
  forall (A : Type) (n : nat) (l1 l2 : list A),
    insert (rev l2) before n in l1 =
    rev (insert l2 before (length l1 - n) in (rev l1)).

Lemma map_insert_before_in :
  forall (A B : Type) (f : A -> B) (n : nat) (l1 l2 : list A),
    map f (insert l2 before n in l1) =
    insert (map f l2) before n in (map f l1).

Lemma join_insert_before_in :
  forall (A : Type) (l1 l2 : list (list A)) (n : nat),
    join (insert l2 before n in l1) =
    insert (join l2) before (length (join (take n l1))) in (join l1).

Lemma insert_before_in_replicate :
  forall (A : Type) (m n : nat) (x : A) (l : list A),
    insert l before n in replicate m x =
    replicate (min n m) x ++ l ++ replicate (m - n) x.

Lemma nth_insert_before_in :
  forall (A : Type) (n m : nat) (l1 l2 : list A),
    nth n (insert l2 before m in l1) =
    if leb (S n) m
    then nth n l1
    else nth (n - m) (l2 ++ drop m l1).

Lemma head_insert_before_in :
  forall (A : Type) (n : nat) (l1 l2 : list A),
    head (insert l2 before n in l1) =
    match l1 with
    | [] => head l2
    | h1 :: _ =>
      match n with
      | 0 =>
        match l2 with
        | [] => Some h1
        | h2 :: _ => Some h2
        end
      | _ => Some h1
      end
    end.

Lemma any_insert_before_in :
  forall (A : Type) (p : A -> bool) (l1 l2 : list A) (n : nat),
    any p (insert l2 before n in l1) =
    orb (any p l1) (any p l2).

Lemma all_insert_before_in :
  forall (A : Type) (p : A -> bool) (l1 l2 : list A) (n : nat),
    all p (insert l2 before n in l1) =
    andb (all p l1) (all p l2).

Lemma count_insert_before_in :
  forall (A : Type) (p : A -> bool) (l1 l2 : list A) (n : nat),
    count p (insert l2 before n in l1) =
    count p l1 + count p l2.

End insertBefore.