reverse ∘ take = drop ∘ reverse

Stream: Is there code for X?

[Chris Wong]

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]

Nope, I don't think we have this

[Mario Carneiro]

You can prove it pretty easily using take_drop

[Chris Wong]

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

[Chris Wong]

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

[Chris Wong]

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]

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]

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

[Mario Carneiro]

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

[Simon Hudon]

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