BigProd permutations - implementation h.

Stream: mathlib4

[Wrenna Robson]

I am trying to port the following Rust code to Lean4.

    pub fn apply_slice_in_place<T>(&self, a: &mut [T]) {
        let layer = self.layer;
        self.bits.chunks_exact(1 << layer).enumerate().for_each(|(i, ch)| {
            ch.iter().enumerate().for_each(|(j, &b)| {
                let gap = layer - layer.abs_diff(i);
                if b {
                    let pos: usize = j + ((j >> gap) << gap);
                    a.swap(pos, pos + (1 << gap));
                }
            });
        });
    }

Here, self is a structure with two fields, bits and layer. Bits is a bitslice of length (2^layer)(2layer + 1). (It's convenient to have layer pre-computed.)

I've implemented this in Lean as follows:

structure ControlBits (m : Nat) where
  bits : Fin (2*m + 1) → Fin (2^m) → Bool

Essentially the above Rust program is calculating the action of the permutation these bits define. It goes layer by layer (over Fin(2*m + 1)), and for each layer, each set of 2^m bits determines whether or not a swap happens between two specific elements.

Now, I really want to build this as a member of Equiv.Perm on the appropriate type (Fin (2^(m + 1))). But I can't use a naive approach of doing this as a bigprod, because the multiplication isn't commutative. But ultimately this is built out of Equiv.Swaps (conditioned on the appropriate bits).

Any suggestions? I would ideally like this to be actually computable too, though I will also want to reason about it. (This sets up a map from ControlBits m to Equiv.Perm Fin (2^(m + 1)), and there is a map from Equiv.Perm Fin (2^(m + 1)) to ControlBits m: it is not a bijection but one is a section of the other (as in, starting with a permutation, going to the bits, and back to the permutation gives you the same permutation: and I would like to prove this).

[Eric Wieser]

Can you add some more #backticks?

[Yaël Dillies]

Use docs#List.prod

[Wrenna Robson]

Ah, that'll probably work I guess! I suppose I'll need to construct the list but that should be doable.

[Wrenna Robson]

Related to this: there are n + 1 unique embeddingsFin n ↪o Fin (n + 1), right? Do we have a way of enumerating them? In a sense I suppose what I want is a map Fin (n + 1) -> (Fin n ↪o Fin (n + 1)).

[Wrenna Robson]

(This is because as Eric pointed out to me, Fin(2^(m+1)) is isomorphic to Fin(m + 1) -> Bool, and it turns out this might be a better way of thinking about the thing I need here.)

[Matthew Ballard]

There might be useful stuff in docs#SimplexCategory

[Wrenna Robson]

Essentially I think:
Let s: Fin (n +1) -> (Fin n ↪o Fin (n + 1)) be the set of embeddings from Fin n to Fin (n + 1) indexed by, essentially, where you do the insertion.
Let t : Fin(2*n + 1) -> Fin (n + 1) be the "fold in half" map which sends 0 to 0, 1 to 1, ..., n to n, n + 1 to n - 1, n + 2 to n - 2, ..., 2*n to 0.

if I define ControlBits m := Fin (2*m + 1) -> (Fin m -> Bool) -> Bool, then, for a c : ControlBits m, for each i in Fin (2*m + 1), I have a permutation
p_ion Fin (m + 1) -> Bool.

This is defined as follows. Take k : Fin (m + 1) -> Bool. Define (p_i)(k)(j) as c i (s (t i) ∘ k) ^ k (t(i)). I claim this p_i is indeed a permutation!

We then define p as the product (...((1 * p 0) * p1) * ... p_n) * p_(n+1) ) * ... *p_(2n -1)) * p_(2n). This p is the permutation that corresponds with c.

[Wrenna Robson]

Which is quite neat. And feels like it might even have a nice representation! It's quite different from the imperative approach I take in Rust.

[Eric Wieser]

Wrenna Robson said:

Related to this: there are n + 1 unique embeddingsFin n ↪o Fin (n + 1), right? Do we have a way of enumerating them? In a sense I suppose what I want is a map Fin (n + 1) -> (Fin n ↪o Fin (n + 1)).

docs#Fin.succAbove