Working with Array.foldr

Stream: lean4

[Wrenna Robson]

I have the following definition (actually mine is somewhat more complicated but not in a way that matters for my question).

def foobar (as : Array α) (c : Array Bool) : Array α :=
  c.zipWithIndex.foldr (fun bp as => as.swap! (2 * bp.2) (2 * bp.2 + bp.1.toNat)) as

Effectively what this does is that it goes along the array, performing swaps on adjacent pairs if the corresponding bit is set in c, for each bit in c.

I am struggling to work with this definition - even proving it doesn't change the size is proving difficult, let alone describing the values I end up with. Can anyone suggest a route forward or a way I might change my definition?

[Kim Morrison]

If the list is notionally organised as pairs, and you're operating on these pairs, why are you not just working with an Array (α × α) at this point?

I think you might need to #xy a bit to get good advice.

[Wrenna Robson]

Kim Morrison said:

If the list is notionally organised as pairs, and you're operating on these pairs, why are you not just working with an Array (α × α) at this point?

I think you might need to #xy a bit to get good advice.

It isn't organised as pairs, or rather the strategy here is to manipulate different sets of pairs.

[Wrenna Robson]

(in fact I also look at pairs of "every fourth element" etc. too.)

[Wrenna Robson]

What do you mean by #xy?

[Kevin Buzzard]

"explain not just the question, but the question behind the question" (or "why you're interested in the question in the first place")

[Wrenna Robson]

Right! So essentially I have a list of natural numbers, some permutation of 0-n-1 - in fact actually n will be some power of two. I could shuffle these by conditionally flipping every pair (0-1, 2-3, etc.), every four (0-2, 1-3, etc.). I can do this via a map on values (that is, literally sending 0 to 1, 1 to 0, etc.) which is just an array map. Or I could operate on indices - send the 0th member of the list to the first and the first to the 0th, etc.: effectively a set of conditional swaps. I want to precisely show that doing the latter is like doing the operation of the former to the index