Zulip Chat Archive

Stream: Is there code for X?

Topic: take pairs


view this post on Zulip 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)

view this post on Zulip Yakov Pechersky (Nov 15 2020 at 21:51):

Sorry, misunderstood

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Nov 15 2020 at 22:04):

What does hoogle say?

view this post on Zulip Adam Topaz (Nov 15 2020 at 22:06):

Looks like
https://hackage.haskell.org/package/utility-ht-0.0.15/docs/Data-List-HT.html#v:mapAdjacent

view this post on Zulip Bhavik Mehta (Nov 15 2020 at 22:06):

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

view this post on Zulip Alex J. Best (Nov 15 2020 at 22:14):

Awesome, thanks everyone!

view this post on Zulip 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