Zulip Chat Archive

Stream: Is there code for X?

Topic: reverse ∘ take = drop ∘ reverse


view this post on Zulip Chris Wong (Jul 28 2020 at 10:50):

Do we have this anywhere?

lemma reverse_take :  {α} n (l : list α), reverse (take n l) = drop (length l - n) (reverse l) :=
by sorry

Context – I'm trying to prove the following statement:

theorem to_append_reverse {l : list α} (p : palindrome l) (h : 2  length l) :
  take (length l / 2) l ++ reverse (take (length l / 2) l) = l

and it's pretty straightforward except for swapping the reverse and take.

view this post on Zulip Johan Commelin (Jul 28 2020 at 10:52):

Nope, I don't think we have this

view this post on Zulip Mario Carneiro (Jul 28 2020 at 10:59):

You can prove it pretty easily using take_drop

view this post on Zulip Chris Wong (Jul 28 2020 at 11:02):

What do you mean by take_drop? I don't see it in the docs

view this post on Zulip Chris Wong (Jul 28 2020 at 11:13):

(and I'm aware of take_append_drop, that's the "pretty straightforward" part :stuck_out_tongue_wink: )

view this post on Zulip Chris Wong (Jul 28 2020 at 12:16):

Progress:

lemma reverse_take {α} (n) (l : list α) : reverse (take n l) = drop (length l - n) (reverse l) :=
begin
  induction l with a l H generalizing n,
  { simp },
  { cases n,
    { rw [take_zero, nat.sub_zero, length_reverse, drop_length, reverse_nil] },
    { have hₗ : length l - n  length (reverse l), { rw length_reverse, apply nat.sub_le },
      simp [drop_append_of_le_length hₗ],
      rw H n } }
end

view this post on Zulip Mario Carneiro (Jul 28 2020 at 12:17):

lemma reverse_take {α} (n) (l : list α) : reverse (take n l) = drop (length l - n) (reverse l) :=
begin
  rw [ congr_arg reverse (take_append_drop n l), reverse_append, drop_left'],
  simp,
end

view this post on Zulip Simon Hudon (Jul 28 2020 at 13:44):

@Mario Carneiro Why do you need congr_arg reverse in rw here?

view this post on Zulip Mario Carneiro (Jul 28 2020 at 13:45):

the alternative would be conv {to_rhs, to_rhs, rw ← take_append_drop n l}

view this post on Zulip Simon Hudon (Jul 28 2020 at 13:46):

Ok, I see. You're avoiding rewriting all the l. I was worried for a moment it was another instance of the unification issues I had with rw with the QPF project


Last updated: May 07 2021 at 22:14 UTC