(** 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.
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.