(** Here we consider [take] and [drop] from Haskell.Data.List. For laws see #<a href="http://conal.net/blog/posts/sequences-streams-and-segments/">Conal Elliott. Sequences, streams, and segments.</a>#, “Segment laws”. *)

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

Set Implicit Arguments.

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).
Proof.
refine (fun xs => _).
destruct xs as [|x xss].
refine (refl_equal _).
refine (refl_equal _).
Qed.

Definition take_nil n
	: nil = take n nil.
Proof.
refine (fun n => _).
destruct n as [|pn].
refine (refl_equal _).
refine (refl_equal _).
Qed.

Definition drop_nil n
	: nil = drop n nil.
Proof.
refine (fix rec (n:nat) := _).
destruct n as [|pn].
refine (refl_equal _).
refine (rec pn).
Qed.

(** permuting take and tail *)
Definition take_perm_tail n xs
	: take n (tail xs) = tail (take (S n) xs).
Proof.
refine (fun n xs => _).
destruct xs as [|x xss].
refine (trans_eq (sym_eq (take_nil _)) (f_equal _ (take_nil _))).
destruct n as [|pn].
	refine (refl_equal _).
	refine (refl_equal _).
Qed.

(** length of [take] *)
Definition take_length n xs
	: n <= length xs -> n = length (take n xs).
Proof.
refine (fix rec (n : nat) xs {struct n} := _).
destruct n as [|pn].
refine (fun _ => refl_equal _).
destruct xs as [|x xss].
	refine (fun x => match Coq.Arith.Le.le_Sn_O _ x with end).
	simpl.
		refine (fun le0 => f_equal _
			(rec _ _ (Coq.Arith.Le.le_S_n _ _ le0))).
Qed.

(** length of [drop] *)
Definition drop_length n0 n1 xs
	: n0 + n1 = length xs -> n1 = length (drop n0 xs).
Proof.
refine (fix rec (n0 n1 : nat) xs {struct n0} := _).
destruct n0 as [|pn0].
refine (fun x => x).
destruct xs as [|x xss].
	refine (fun S_eq_O => match
		(eq_ind _ IsSucc (I : IsSucc (S _)) _ S_eq_O)
		with end).
	simpl.
		refine (fun eq0 => rec _ _ _ (eq_add_S _ _ eq0)).
Qed.

(** 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.
Proof.
refine (fix rec n (xs : list e) := _).
destruct xs as [|x xss].
refine (fun _ => take_nil _).
destruct n as [|pn].
	refine (fun lt0 => match Coq.Arith.Le.le_Sn_O _ lt0 with end).
	refine (fun lt0 => f_equal (cons x)
		(rec pn xss (Coq.Arith.Le.le_S_n _ _ lt0))).
Qed.

(** 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.
Proof.
refine (fix rec (n:nat) (xs:list e) {struct n} := _).
destruct xs as [|x xss].
refine (fun _ => drop_nil _).
destruct n as [|pn].
	refine (fun lt0 => match Coq.Arith.Le.le_Sn_O _ lt0 with end).
	refine (fun lt0 => (rec pn xss (Coq.Arith.Le.le_S_n _ _ lt0))).
Qed.

Definition take_app_drop n xs
	: xs = take n xs ++ drop n xs.
Proof.
refine (fix rec (n : nat) (xs : list e) {struct n} := _).
destruct n as [|pn].
simpl.
	refine (refl_equal _).
destruct xs as [|x xss].
	simpl.
		refine (drop_nil _).
	simpl.
		refine (f_equal _ (rec _ xss)).
Qed.

Definition take_plus n1 n0 xs
	: take (n0 + n1) xs = take n0 xs ++ take n1 (drop n0 xs).
Proof.
refine (fix rec (n1 n0 : nat) (xs : list e) {struct n0} := _).
destruct n0 as [|pn0].
simpl.
	refine (refl_equal _).
destruct xs as [|x xss].
	simpl.
		refine (eq_ind _ (fun dep => nil = take n1 dep) _ _
			(drop_nil _)).
		refine (take_nil _).
	simpl.
		refine (f_equal _ (rec _ _ xss)).
Qed.

Definition drop_plus n1 n0 xs
	: drop n0 xs = take n1 (drop n0 xs) ++ drop (n0+n1) xs.
Proof.
refine (fix rec (n1 n0 : nat) (xs : list e) {struct n0} := _).
destruct n0 as [|pn0].
simpl.
	refine (take_app_drop _ _).
destruct xs as [|x xss].
	simpl.
		refine (eq_ind _ (fun dep => _ = _ ++ dep) _ _ (drop_nil _)).
		refine (eq_ind _ (fun dep => _ = dep) _ _ (app_nil_end _)).
		refine (eq_ind _ (fun dep => _ = take _ dep) _ _ (drop_nil _)).
		refine (eq_ind _ (fun dep => dep = _) _ _ (drop_nil _)).
		refine (take_nil _).
	simpl.
		refine (rec _ _ xss).
Qed.



(** ** [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).
Proof.
refine (fun ys => fix rec (n:nat) (xs:list e) {struct n} := _).
destruct xs as [|x xss].
refine (fun le0 => _).
	rewrite <- (Coq.Arith.Le.le_n_O_eq n le0).
	refine (refl_equal _).
destruct n as [|pn].
	refine (fun _ => refl_equal _).
	refine (fun le0 => f_equal (cons x)
		(rec pn xss (Coq.Arith.Le.le_S_n _ _ le0))).
Qed.

(** [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).
Proof.
refine (fun ys => fix rec (n:nat) (xs:list e) {struct n} := _).
destruct xs as [|x xss].
refine (fun le0 => _).
	rewrite <- (Coq.Arith.Le.le_n_O_eq n le0).
	refine (refl_equal _).
destruct n as [|pn].
	refine (fun _ => refl_equal _).
	refine (fun le0 => rec pn xss (Coq.Arith.Le.le_S_n _ _ le0)).
Qed.

(** [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).
Proof.
refine (fun n ys => fix rec (xs:list e) {struct xs} := _).
destruct xs as [|x xss].
simpl.
	refine (eq_ind _ (fun dep => _ = take dep _) (refl_equal _) _
		(sym_eq (Coq.Arith.Plus.plus_0_r _))).
simpl.
	refine (eq_ind _ (fun dep => _ = take dep _) _ _
		(Coq.Arith.Plus.plus_Snm_nSm _ _)).
	simpl.
	refine (f_equal _ (rec xss)).
Qed.

(** [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).
Proof.
refine (fun n ys => fix rec (xs:list e) {struct xs} := _).
destruct xs as [|x xss].
simpl.
	refine (eq_ind _ (fun dep => _ = drop dep _) (refl_equal _) _
		(sym_eq (Coq.Arith.Plus.plus_0_r _))).
simpl.
	refine (eq_ind _ (fun dep => _ = drop dep _) _ _
		(Coq.Arith.Plus.plus_Snm_nSm _ _)).
	simpl.
	refine (rec xss).
Qed.

Definition take_app_exact xs ys
	: xs = take (length xs) (xs ++ ys).
Proof.
refine (fun xs ys => _).
refine (eq_ind _ (fun xs => xs = _) _ _ (sym_eq (app_nil_end _))).
refine (take_app_part 0 ys xs).
Qed.

Definition drop_app_exact xs ys
	: ys = drop (length xs) (xs ++ ys).
Proof. refine (fun xs ys => drop_app_part 0 _ _). Qed.

End element.