# Zulip Chat Archive

## Stream: maths

### Topic: functoriality of lists and zip_with

#### Yakov Pechersky (Apr 05 2021 at 17:48):

I have a need for some lemmas about `list.zip_with`

and they all basically follow the same exact proof. The common aspect is, `zip_with`

distributes a permutation of the resulting list onto the input lists, if the inputs are of the same length, or a subset of the list ... ditto. What's the better generalized way to prove the following lemmas:

```
lemma zip_with_distrib_take :
(zip_with f l l').take n = zip_with f (l.take n) (l'.take n) := sorry
lemma zip_with_distrib_drop :
(zip_with f l l').drop n = zip_with f (l.drop n) (l'.drop n) := sorry
lemma zip_with_distrib_tail :
(zip_with f l l').tail = zip_with f l.tail l'.tail := sorry
lemma zip_with_append (f : α → β → γ) (l la : list α) (l' lb : list β) (h : l.length = l'.length) :
zip_with f (l ++ la) (l' ++ lb) = zip_with f l l' ++ zip_with f la lb := sorry
lemma zip_with_distrib_reverse (h : l.length = l'.length) :
(zip_with f l l').reverse = zip_with f l.reverse l'.reverse := sorry
lemma zip_with_rotate_distrib (h : l.length = l'.length) :
(zip_with f l l').rotate n = zip_with f (l.rotate n) (l'.rotate n) := sorry
```

instead of repeating proofs that basically look like

```
induction l with hd tl hl generalizing l' n,
{ simp },
{ cases l',
{ simp },
{ cases n,
{ simp },
{ simp [hl] } } }
```

#### Kevin Buzzard (Apr 05 2021 at 19:31):

Tidy?

#### Adam Topaz (Apr 05 2021 at 19:46):

If tidy doesn't work by itself, you can add the tidy attribute to the appropriate tactics locally

#### Yakov Pechersky (Apr 05 2021 at 20:10):

I guess it would be more correct to say the "applicative nature" instead of "functoriality"

#### Yakov Pechersky (Apr 05 2021 at 20:12):

For something like

```
lemma zip_with_distrib_drop' {α β γ : Type*} (f : α → β → γ) (l : list α) (l' : list β) (n : ℕ) :
(zip_with f l l').drop n = zip_with f (l.drop n) (l'.drop n) :=
begin
tidy,
end
```

tidy chugs chugs chugs but doesn't prove it

#### Eric Wieser (Apr 05 2021 at 21:22):

Your suggested induction proof doesn't seem to work for that lemma - are there some lemmas you have locally that fill in the gaps?

#### Eric Wieser (Apr 05 2021 at 21:23):

Ah, import! `import data.list`

#### Eric Wieser (Apr 05 2021 at 21:24):

I fall at the very first hurdle at attempting to generalize that; `drop`

is universe-polymorphic, so can't be replaced with a function argument to the lemma

#### Bhavik Mehta (Apr 05 2021 at 21:51):

Yakov Pechersky said:

I guess it would be more correct to say the "applicative nature" instead of "functoriality"

Yeah I'm inclined to say this is expressing that `drop n`

is an applicative transformation, possibly with the zipping applicative on lists rather than the usual monadic one

#### Yakov Pechersky (Apr 05 2021 at 22:55):

Here's the property of such functions, to first pass:

```
def distrib_over_zip_with (e : ∀ {α : Type*}, list α → list α) : Prop :=
∀ {α β γ : Type*} (f : α → β → γ) (l : list α) (l' : list β), e (zip_with f l l') = zip_with f (e l) (e l')
lemma ex_drop (n : ℕ) : distrib_over_zip_with (λ _, drop n) :=
begin
intros _ _ _ _ l l',
exact zip_with_distrib_drop _ _ _ _
end
```

Last updated: May 11 2021 at 16:22 UTC