Zulip Chat Archive

Stream: maths

Topic: functoriality of lists and zip_with


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

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 19:31):

Tidy?

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

view this post on Zulip Yakov Pechersky (Apr 05 2021 at 20:10):

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

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

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

view this post on Zulip Eric Wieser (Apr 05 2021 at 21:23):

Ah, import! import data.list

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

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

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