## Stream: Is there code for X?

### Topic: reverse ∘ take = drop ∘ reverse

#### 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.

#### Johan Commelin (Jul 28 2020 at 10:52):

Nope, I don't think we have this

#### Mario Carneiro (Jul 28 2020 at 10:59):

You can prove it pretty easily using take_drop

#### Chris Wong (Jul 28 2020 at 11:02):

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

#### 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: )

#### 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


#### 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


#### Simon Hudon (Jul 28 2020 at 13:44):

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

#### Mario Carneiro (Jul 28 2020 at 13:45):

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

#### 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