Library Beroal.TakeDrop

Here we consider take and drop from Haskell.Data.List. For laws see Conal Elliott. Sequences, streams, and segments., “Segment laws”.

Require Import Coq.Lists.List.
Require Coq.Arith.Plus.
Require Coq.Arith.Le.
Require Import Beroal.Init.


Section element.
Variable e : Type.

a head as a list
Definition single_head := fun xs : list e => match xs with
        | nil => nil
        | x :: _ => x :: nil
        end.

Prefix. Returns first n elements of a list
Definition take := fix rec (n : nat) (xs : list e) {struct n} : list e
        := match n with
        | O => nil
        | S pn => match xs with
                | nil => nil
                | x :: xss => x :: (rec pn xss)
                end
        end.

removes first n elements from a list
Definition drop := reptr (@tail e).

obvious simplifications
Check fun n x xss => (refl_equal _) : take (S n) (x :: xss) = x :: take n xss.
Check fun n x xss => (refl_equal _) : drop (S n) (x :: xss) = drop n xss.

singleton versions
Check (refl_equal _) : single_head = take 1.
Check (refl_equal _) : (@tail e) = drop 1.

Definition tail_length (xs : list e)
        : length (tail xs) = pred (length xs).

Definition take_nil n
        : nil = take n nil.

Definition drop_nil n
        : nil = drop n nil.

permuting take and tail
Definition take_perm_tail n xs
        : take n (tail xs) = tail (take (S n) xs).

length of take
Definition take_length n xs
        : n <= length xs -> n = length (take n xs).

length of drop
Definition drop_length n0 n1 xs
        : n0 + n1 = length xs -> n1 = length (drop n0 xs).

Taking the whole list. An alternative definition: forall n, take (length xs + n) xs = xs.
Definition take_degen n (xs : list e)
        : length xs <= n -> xs = take n xs.

Dropping the whole list. An alternative definition: forall n, drop (length xs + n) xs = nil.
Definition drop_degen (n:nat) (xs:list e)
        : length xs <= n -> nil = drop n xs.

Definition take_app_drop n xs
        : xs = take n xs ++ drop n xs.

Definition take_plus n1 n0 xs
        : take (n0 + n1) xs = take n0 xs ++ take n1 (drop n0 xs).

Definition drop_plus n1 n0 xs
        : drop n0 xs = take n1 (drop n0 xs) ++ drop (n0+n1) xs.

take and drop of a concatenation


take removes the second list in a concatenation
Definition take_app_degen ys (n:nat) (xs:list e)
        : n <= length xs -> take n xs = take n (xs++ys).

drop does not change the second list in a concatenation
Definition drop_app_degen ys (n:nat) (xs:list e)
        : n <= length xs -> (drop n xs) ++ ys = drop n (xs++ys).

take takes the whole first list in a concatenation
Definition take_app_part n ys xs
        : xs ++ take n ys = take (n + (length xs)) (xs++ys).

drop drops the whole first list in a concatenation
Definition drop_app_part n ys xs
        : drop n ys = drop (n+(length xs)) (xs++ys).

Definition take_app_exact xs ys
        : xs = take (length xs) (xs ++ ys).

Definition drop_app_exact xs ys
        : ys = drop (length xs) (xs ++ ys).

End element.