The checked adjacent-swap planner

The planner fixes one requested axis at a time. Its processed prefix agrees with the requested permutation, and its recorded swaps reproduce its current axis list.

theorem NN.MLTheory.CROWN.Graph.swapAdjacentAxes_perm (axes : List ℕ) (depth : ℕ) : (Spec.Shape.swapAdjacentAxes axes depth).Perm axes

theorem NN.MLTheory.CROWN.Graph.swapAdjacentAxes_map (axes : List ℕ) (depth : ℕ) (f : ℕ → ℕ) : Spec.Shape.swapAdjacentAxes (List.map f axes) depth = List.map f (Spec.Shape.swapAdjacentAxes axes depth)

theorem NN.MLTheory.CROWN.Graph.swapFold_perm (depths axes : List ℕ) : (List.foldl Spec.Shape.swapAdjacentAxes axes depths).Perm axes

theorem NN.MLTheory.CROWN.Graph.swapFold_map (depths axes : List ℕ) (f : ℕ → ℕ) : List.foldl Spec.Shape.swapAdjacentAxes (List.map f axes) depths = List.map f (List.foldl Spec.Shape.swapAdjacentAxes axes depths)

theorem NN.MLTheory.CROWN.Graph.swapFold_reverse (depths axes : List ℕ) : List.foldl Spec.Shape.swapAdjacentAxes (List.foldl Spec.Shape.swapAdjacentAxes axes depths) depths.reverse = axes

theorem NN.MLTheory.CROWN.Graph.swapDepthsForPerm_realizes (perm : Array ℕ) (rank : ℕ) (hlen : perm.size = rank) (hnodup : perm.toList.Nodup) (swaps : Array ℕ) (hplan : IR.Graph.swapDepthsForPerm perm rank = Except.ok swaps) : List.foldl Spec.Shape.swapAdjacentAxes (List.range rank) swaps.toList = perm.toList

Every successful checked plan realizes the entire requested axis ordering.