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