Help with vector proof

Stream: new members

[Timothy Mou]

I am having trouble writing this proof:

lemma tail_plus_commute' (v1 v2 : Vector Bool n) :
  (Vector.map₂ xor v1 v2).tail = Vector.map₂ xor v1.tail v2.tail :=

Here I am using the definition of Vector from Mathlib.Data.Vector. Inducting on the length of the vector does not seem to be working.

[Matt Diamond]

when you say "not working", what do you mean? like you can't prove the base case or the inductive hypothesis isn't helping?

[Matt Diamond]

you actually don't need induction for this... you can just do cases' on n

[Timothy Mou]

Yeah I realized this. Actually I only need the statement for (n+1) so the proof is even simpler:

lemma tail_plus_commute' (v1 v2 : Vector Bool (n + 1)) :
  (Vector.map₂ xor v1 v2).tail = Vector.map₂ xor v1.tail v2.tail :=
    match v1, v2 with
    | ⟨ x :: xs , _ ⟩, ⟨ y :: ys, _ ⟩ =>
        by simp [Vector.map₂, Vector.tail, List.zipWith]

I'm not entirely sure why I was having trouble before. The VSCode UI is a little confusing, sometimes I can't tell if I've actually proved something