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