## Stream: Is there code for X?

### Topic: take pairs

#### Alex J. Best (Nov 15 2020 at 21:50):

Does this have a name or is it already developed somewhere in mathlib, I guess it is really a combination of "pair up" and map

def take_pairs {α β : Type*} (f : α → α → β) : list α → list β
| [] := []
| [a] := []
| (a :: b :: l) := f a b :: take_pairs (b :: l)


#### Yakov Pechersky (Nov 15 2020 at 21:51):

Sorry, misunderstood

#### Yakov Pechersky (Nov 15 2020 at 21:54):

import data.list.zip

def take_pairs {α β : Type*} (f : α → α → β) : list α → list β
| [] := []
| [a] := []
| (a :: b :: l) := f a b :: take_pairs (b :: l)

def take_pairs' {α β : Type*} (f : α → α → β) (l : list α) : list β :=
list.zip_with f l l.tail


#### Yakov Pechersky (Nov 15 2020 at 21:57):

import data.list.zip

def take_pairs {α β : Type*} (f : α → α → β) : list α → list β
| [] := []
| [a] := []
| (a :: b :: l) := f a b :: take_pairs (b :: l)

def take_pairs' {α β : Type*} (f : α → α → β) (l : list α) : list β :=
list.zip_with f l l.tail

lemma tp_eq {α β : Type*} {f : α → α → β} {l : list α} : take_pairs f l = take_pairs' f l :=
begin
induction l with hd tl IH,
{ refl },
{ cases tl,
{ refl },
{ simpa only [take_pairs, IH] } }
end


#### Yakov Pechersky (Nov 15 2020 at 21:59):

I might define a separate chunk_pairs as such:

def chunk_pairs {α β : Type*} (f : α → α → β) : list α → list β
| [] := []
| [a] := []
| (a :: b :: l) := f a b :: chunk_pairs l


#### Adam Topaz (Nov 15 2020 at 22:04):

What does hoogle say?

#### Bhavik Mehta (Nov 15 2020 at 22:06):

In Haskell I'd use zipWith f <*> tail

#### Alex J. Best (Nov 15 2020 at 22:14):

Awesome, thanks everyone!

#### Eric Wieser (Nov 16 2020 at 10:05):

docs#list.chain looks related but not what you're after

Last updated: May 19 2021 at 00:40 UTC