# 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

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.

:= 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

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.

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.

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

length of take

length of drop

Taking the whole list. An alternative definition: forall n, take (length xs + n) xs = 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.

: 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 removes the second list in a concatenation

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

: n <= length xs -> (drop n xs) ++ ys = drop n (xs++ys).

take takes the whole first list in a concatenation

drop drops the whole first list in a concatenation