Reasoning about vectors

Stream: new members

[chris477]

Hi! As a training exercise, I'm trying to prove some basic facts about Turing Machines (my own definition, not the one in mathlib). One technical difficulty is that I want to keep the number of tapes as a parameter, so I'm using a Vector Tape k for the tapes of a Turing Machine. Now a movement of the heads on the tape is implemented as maping a moves : Vector Movement k to a new configuration via (tapes.zip moves).map (fun (tape, m) => tape.move m).
Then I have a statement about the move function, namely that the occupied space on a tape is at most one larger after applying move. Now I want to lift this to the Turing Machine's move function to state that the sum of occupied space after move is at most k plus the sum of occupied space before.

And now to the actual question (sorry for the long introduction): I'm having a hard time dealing with all the zip and map functions, and I was wondering if I'm missing some functions or if it would be better to use indices instead of zip and map.

[Eric Wieser]

I think things will be much easier with indices

[Eric Wieser]

That is, tapes : Fin k -> Tape

[Eric Wieser]

Then you have new_tapes := fun i => (tapes i).move (moves i)

[chris477]

Oh you are saying you wouldn't even use List?

[chris477]

Thanks, I'll try!