List.map_permutationsAux2
theorem List.map_permutationsAux2 :
∀ {α : Type u_1} {β : Type u_2} (t : α) (ts ys : List α) (f : List α → β),
List.map f (List.permutationsAux2 t ts [] ys id).2 = (List.permutationsAux2 t ts [] ys f).2
This theorem states that for any types `α` and `β`, and for any list `ts` and `ys` of type `α`, any element `t` of type `α`, and any function `f` from a list of `α` to `β`, the act of first applying `List.permutationsAux2` with `t`, `ts`, an empty list, `ys`, and the identity function as arguments, and then mapping the function `f` over the result, is the same as applying `List.permutationsAux2` directly with `f` as the last argument. Essentially, the function `f` can be integrated directly into `List.permutationsAux2` when the input list `r` is empty.
More concisely: For any types `α` and `β`, and any lists `ts` and `ys` of type `α`, any element `t` of type `α`, and any function `f` from `α` to `β`, the application of `List.permutationsAux2` with `t`, `ts`, an empty list, `ys`, and the identity function, then mapping `f` over the result, equals applying `List.permutationsAux2` directly with `f` as the last argument.
|
List.permutationsAux2_snd_cons
theorem List.permutationsAux2_snd_cons :
∀ {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (y : α) (ys : List α) (f : List α → β),
(List.permutationsAux2 t ts r (y :: ys) f).2 =
f (t :: y :: ys ++ ts) :: (List.permutationsAux2 t ts r ys fun x => f (y :: x)).2
This theorem states that for any two types `α` and `β`, an element `t` of type `α`, a list `ts` of elements of type `α`, a list `r` of elements of type `β`, an element `y` of type `α`, a list `ys` of elements of type `α`, and a function `f` that takes a list of elements of type `α` and returns an element of type `β`, the second element of the tuple returned by the function `List.permutationsAux2` applied to `t`, `ts`, `r` and the list with `y` as the first element and `ys` as the rest of the elements, with function `f`, is equal to the list that has `f` applied to the list where `t` is the first element, `y` is the second element, and the rest of the elements are the concatenation of `ys` and `ts`, as the first element, followed by the second element of the tuple returned by `List.permutationsAux2` applied to `t`, `ts`, `r`, `ys` and a function that takes a list `x` and returns `f` applied to the list with `y` as the first element and `x` as the rest of the elements.
More concisely: For any types `α` and `β`, given an element `t` of type `α`, lists `ts` and `ys` of elements of type `α`, a list `r` of elements of type `β`, and a function `f` that maps lists of `α` to `β`, the second element of `List.permutationsAux2` applied to `t`, `ts`, `r`, `[y] :: ys`, and `f` is equal to the list obtained by applying `f` to `[t, y]` followed by the second element of `List.permutationsAux2` applied to `t`, `ts`, `r`, `ys`, and the function `x => f [y] ++ x`.
|
List.permutationsAux_nil
theorem List.permutationsAux_nil : ∀ {α : Type u_1} (is : List α), [].permutationsAux is = []
The theorem `List.permutationsAux_nil` states that for any type `α` and for any list `is` of that type, when we apply the auxiliary function `List.permutationsAux` on an empty list and `is`, the result is always an empty list. This means that there are no permutations of `is` appended with an empty list that do not fix the empty list.
More concisely: For any type `α` and list `is : List α`, the auxiliary function `List.permutationsAux` applied to the empty list and `is` returns an empty list. In other words, there are no non-empty permutations of `is` when appended with the empty list.
|
List.permutationsAux2_comp_append
theorem List.permutationsAux2_comp_append :
∀ {α : Type u_1} {β : Type u_2} {t : α} {ts ys : List α} {r : List β} (f : List α → β),
(List.permutationsAux2 t [] r ys fun x => f (x ++ ts)).2 = (List.permutationsAux2 t ts r ys f).2
The theorem `List.permutationsAux2_comp_append` states that for any types `α` and `β`, any element `t` of type `α`, any lists `ts`, `ys` of type `α`, any list `r` of type `β`, and any function `f` from a list of `α` to `β`, the second component of the result of applying `List.permutationsAux2` with `t`, an empty list, `r`, `ys` and a function that applies `f` to the concatenation of its argument with `ts`, is equal to the second component of the result of applying `List.permutationsAux2` with `t`, `ts`, `r`, `ys` and `f`. In simpler terms, it says that you can fold the list `ts` into the function `f` when using `List.permutationsAux2`.
More concisely: For any types `α` and `β`, lists `ts`, `ys` of type `α`, list `r` of type `β`, function `f` from list of `α` to `β`, and element `t` of type `α`, the second component of `List.permutationsAux2 t [] r ys (λ x => f (x :: ts))` equals the second component of `List.permutationsAux2 t ts r ys f`.
|
List.foldr_permutationsAux2
theorem List.foldr_permutationsAux2 :
∀ {α : Type u_1} (t : α) (ts : List α) (r L : List (List α)),
List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) r L =
(L.bind fun y => (List.permutationsAux2 t ts [] y id).2) ++ r
The theorem `List.foldr_permutationsAux2` states that for any type `α`, and given an element `t` of type `α`, a list `ts` of type `α`, and two lists `r` and `L` of lists of type `α`, the fold operation, which applies the function `(List.permutationsAux2 t ts r y id).2` to all elements `y` of list `L` (from right to left) starting with the initial value `r`, is equal to the concatenation of the list obtained by applying the function `(List.permutationsAux2 t ts [] y id).2` to each element `y` of list `L` (using the list monadic bind operation) and the list `r`. Essentially, this theorem relates the `foldr` operation and the `bind` operation on lists when the function applied generates permutations of the lists.
More concisely: For any type `α` and lists `ts` and `L` of `α`, the right fold operation of applying `List.permutationsAux2 t ts r` to each element `y` in `L` is equal to the concatenation of the lists obtained by applying `List.permutationsAux2 t ts [] y` to each `y` in `L` using list monadic bind and the list `r`.
|
List.permutationsAux_cons
theorem List.permutationsAux_cons :
∀ {α : Type u_1} (t : α) (ts is : List α),
(t :: ts).permutationsAux is =
List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) (ts.permutationsAux (t :: is)) is.permutations
The theorem `List.permutationsAux_cons` states that for any type `α` and any lists `t`, `ts`, and `is` of type `α`, the permutations of the list obtained by prepending `t` to `ts` and not fixing `ts` is equal to the result of applying a fold operation on the permutations of `is`. The fold operation, from right to left, constructs new permutations by inserting `t` into each position of each permutation, and concatenates the resulting list of permutations to the permutations of `ts` that do not fix `t :: ts`. In other words, it describes how to generate all the permutations of a list by picking an element `t` and inserting it into every possible position in all permutations of the remaining elements.
More concisely: The theorem `List.permutationsAux_cons` states that the permutations of a list obtained by prepending `t` to another list `ts` is equal to the fold (from right to left) of the permutations of the suffix of `ts` and the list of permutations obtained by inserting `t` into each position of each permutation of the suffix of `ts`.
|
List.permutationsAux2_snd_eq
theorem List.permutationsAux2_snd_eq :
∀ {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (ys : List α) (f : List α → β),
(List.permutationsAux2 t ts r ys f).2 =
List.map (fun x => f (x ++ ts)) (List.permutationsAux2 t [] [] ys id).2 ++ r
This theorem, `List.permutationsAux2_snd_eq`, states that for any types `α` and `β`, any elements `t` of type `α`, any lists `ts` and `ys` of type `α`, any list `r` of type `β`, and any function `f` mapping a list of `α` to `β`, the second element of the pair resulting from `List.permutationsAux2` with parameters `t`, `ts`, `r`, `ys`, and `f` is equal to the concatenation of `r` and the list produced by mapping `f` over the concatenation of `x` and `ts` for each `x` in the second element of the pair produced by `List.permutationsAux2` with parameters `t`, `[]`, `[]`, `ys`, and the identity function. This means that all of `ts`, `r`, and `f` can be eliminated from `permutationsAux2`. For instance, `(permutationsAux2 1 [] [] [2, 3, 4] id).2` returns a list whose elements are created by inserting `1` into every non-terminal position of `[2, 3, 4]` in order.
More concisely: For any types `α` and `β`, given `t` of type `α`, lists `ts` and `ys` of type `α`, list `r` of type `β`, and function `f : List α → β`, the second component of `List.permutationsAux2 (t : α) [] [] ts f` is equal to the concatenation of `r` with the list obtained by applying `f` to each element and its appended tail of `ts` from the second component of `List.permutationsAux2 (t : α) [] [] ys id`.
|
List.permutationsAux2_append
theorem List.permutationsAux2_append :
∀ {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (ys : List α) (f : List α → β),
(List.permutationsAux2 t ts [] ys f).2 ++ r = (List.permutationsAux2 t ts r ys f).2
The theorem `List.permutationsAux2_append` states that for any types `α` and `β`, and for any given list `ts` of type `α`, list `r` of type `β`, list `ys` of type `α`, element `t` of type `α`, and function `f` from `List α` to `β`, the second component of the result from applying `List.permutationsAux2` to `t`, `ts`, the empty list, `ys`, and `f`, and then appending `r` is the same as the second component of directly applying `List.permutationsAux2` to `t`, `ts`, `r`, `ys`, and `f`. In other words, you can append `r` to the second component of the result either before or after applying `List.permutationsAux2`; the outcome is the same.
More concisely: For any types `α` and `β`, lists `ts` of type `List α`, `r` of type `List β`, `ys` of type `List α`, element `t` of type `α`, and function `f` from `List α` to `β`, the application of `List.permutationsAux2` on `t`, `ts`, the empty list, `ys`, and `f`, followed by appending `r`, is equal to the application of `List.permutationsAux2` on `t`, `ts`, `r`, `ys`, and `f`.
|