functoriality of lists and zip_with

Stream: maths

[Yakov Pechersky]

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]

Tidy?

[Adam Topaz]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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]

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]

Ah, import! import data.list

[Eric Wieser]

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]

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]

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