## Definitions on lists #

This file contains various definitions on lists. It does not contain
proofs about these definitions, those are contained in other files in `Data.List`

## Equations

- List.instSDiffList = { sdiff := List.diff }

"Inhabited" `take`

function: Take `n`

elements from a list `l`

. If `l`

has less than `n`

elements, append `n - length l`

elements `default`

.

## Equations

- List.takeI n l = List.takeD n l default

The alternating sum of a list.

## Equations

- List.alternatingSum [] = 0
- List.alternatingSum [g] = g
- List.alternatingSum (g :: h :: t) = g + -h + List.alternatingSum t

The alternating product of a list.

## Equations

- List.alternatingProd [] = 1
- List.alternatingProd [g] = g
- List.alternatingProd (g :: h :: t) = g * h⁻¹ * List.alternatingProd t

`findM tac l`

returns the first element of `l`

on which `tac`

succeeds, and
fails otherwise.

## Equations

- List.findM tac = List.firstM fun a => tac a $> a

`findM? p l`

returns the first element `a`

of `l`

for which `p a`

returns
true. `findM?`

short-circuits, so `p`

is not necessarily run on every `a`

in
`l`

. This is a monadic version of `List.find`

.

## Equations

- List.findM?' p [] = pure none
- List.findM?' p (x_1 :: xs) = do let __discr ← p x_1 match __discr with | { down := px } => if px = true then pure (some x_1) else List.findM?' p xs

Monadic variant of `foldlIdx`

.

## Equations

- List.foldlIdxM f b as = List.foldlIdx (fun i ma b => do let a ← ma f i a b) (pure b) as

Monadic variant of `foldrIdx`

.

## Equations

- List.foldrIdxM f b as = List.foldrIdx (fun i a mb => do let b ← mb f i a b) (pure b) as

Auxiliary definition for `mapIdxM'`

.

## Equations

- List.mapIdxMAux' f x [] = pure PUnit.unit
- List.mapIdxMAux' f x (a :: as) = SeqRight.seqRight (f x a) fun x => List.mapIdxMAux' f (x + 1) as

A variant of `mapIdxM`

specialised to applicative actions which
return `unit`

.

## Equations

- List.mapIdxM' f as = List.mapIdxMAux' f 0 as

`l.all₂ p`

is equivalent to `∀ a ∈ l, p a∀ a ∈ l, p a∈ l, p a`

, but unfolds directly to a conjunction, i.e.
`list.all₂ p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2∧ p 1 ∧ p 2∧ p 2`

.

An auxiliary function for defining `permutations`

. `permutationsAux2 t ts r ys f`

is equal to
`(ys ++ ts, (insert_left ys t ts).map f ++ r)`

, where `insert_left ys t ts`

(not explicitly
defined) is the list of lists of the form `insert_nth n t (ys ++ ts)`

for `0 ≤ n < length ys≤ n < length ys`

.

```
permutations_aux2 10 [4, 5, 6] [] [1, 2, 3] id =
([1, 2, 3, 4, 5, 6],
[[10, 1, 2, 3, 4, 5, 6],
[1, 10, 2, 3, 4, 5, 6],
[1, 2, 10, 3, 4, 5, 6]])
```

## Equations

- List.permutationsAux2 t ts r [] x = (ts, r)
- List.permutationsAux2 t ts r (y :: ys) x = match List.permutationsAux2 t ts r ys fun x => x (y :: x) with | (us, zs) => (y :: us, x (t :: y :: us) :: zs)

A recursor for pairs of lists. To have `C l₁ l₂`

for all `l₁`

, `l₂`

, it suffices to have it for
`l₂ = []`

and to be able to pour the elements of `l₁`

into `l₂`

.

## Equations

- List.permutationsAux.rec H0 H1 [] x = H0 x
- List.permutationsAux.rec H0 H1 (t :: ts) x = H1 t ts x (List.permutationsAux.rec H0 H1 ts (t :: x)) (List.permutationsAux.rec H0 H1 x [])

An auxiliary function for defining `permutations`

. `permutationsAux ts is`

is the set of all
permutations of `is ++ ts`

that do not fix `ts`

.

## Equations

- List.permutationsAux = List.permutationsAux.rec (fun x => []) fun t ts is IH1 IH2 => List.foldr (fun y r => (List.permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)

List of all permutations of `l`

.

permutations [1, 2, 3] = [[1, 2, 3], [2, 1, 3], [3, 2, 1], [2, 3, 1], [3, 1, 2], [1, 3, 2]]

## Equations

- List.permutations l = l :: List.permutationsAux l []

`permutations'Aux t ts`

inserts `t`

into every position in `ts`

, including the last.
This function is intended for use in specifications, so it is simpler than `permutationsAux2`

,
which plays roughly the same role in `permutations`

.

Note that `(permutationsAux2 t [] [] ts id).2`

is similar to this function, but skips the last
position:

```
permutations'Aux 10 [1, 2, 3] =
[[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3], [1, 2, 3, 10]]
(permutationsAux2 10 [] [] [1, 2, 3] id).2 =
[[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3]]
```

## Equations

- List.permutations'Aux t [] = [[t]]
- List.permutations'Aux t (x_1 :: xs) = (t :: x_1 :: xs) :: List.map (List.cons x_1) (List.permutations'Aux t xs)

List of all permutations of `l`

. This version of `permutations`

is less efficient but has
simpler definitional equations. The permutations are in a different order,
but are equal up to permutation, as shown by `list.permutations_perm_permutations'`

.

```
permutations [1, 2, 3] =
[[1, 2, 3], [2, 1, 3], [2, 3, 1],
[1, 3, 2], [3, 1, 2], [3, 2, 1]]
```

## Equations

- List.permutations' [] = [[]]
- List.permutations' (x_1 :: xs) = List.bind (List.permutations' xs) (List.permutations'Aux x_1)

`extractp p l`

returns a pair of an element `a`

of `l`

satisfying the predicate
`p`

, and `l`

, with `a`

removed. If there is no such element `a`

it returns `(none, l)`

.

## Equations

- List.extractp p [] = (none, [])
- List.extractp p (x_1 :: xs) = if p x_1 then (some x_1, xs) else match List.extractp p xs with | (a', l') => (a', x_1 :: l')

Notation for calculating the product of a `List`

## Equations

- List.«term_×ˢ_» = Lean.ParserDescr.trailingNode `List.term_×ˢ_ 82 83 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ˢ ") (Lean.ParserDescr.cat `term 82))

## Equations

- One or more equations did not get rendered due to their size.

## Equations

- One or more equations did not get rendered due to their size.

`dedup l`

removes duplicates from `l`

(taking only the last occurrence).
Defined as `pwFilter (≠)≠)`

.

dedup [1, 0, 2, 2, 1] = [0, 2, 1]

## Equations

- List.dedup = List.pwFilter fun x x_1 => x ≠ x_1

Greedily create a sublist of `a :: l`

such that, for every two adjacent elements `a, b`

,
`R a b`

holds. Mostly used with ≠; for example, `destutter' (≠) 1 [2, 2, 1, 1] = [1, 2, 1]≠) 1 [2, 2, 1, 1] = [1, 2, 1]`

,
`destutter' (≠) 1, [2, 3, 3] = [1, 2, 3]≠) 1, [2, 3, 3] = [1, 2, 3]`

, `destutter' (<) 1 [2, 5, 2, 3, 4, 9] = [1, 2, 5, 9]`

.

## Equations

- List.destutter' R x [] = [x]
- List.destutter' R x (h :: l) = if R x h then x :: List.destutter' R h l else List.destutter' R x l

Greedily create a sublist of `l`

such that, for every two adjacent elements `a, b ∈ l∈ l`

,
`R a b`

holds. Mostly used with ≠; for example, `destutter (≠) [1, 2, 2, 1, 1] = [1, 2, 1]≠) [1, 2, 2, 1, 1] = [1, 2, 1]`

,
`destutter (≠) [1, 2, 3, 3] = [1, 2, 3]≠) [1, 2, 3, 3] = [1, 2, 3]`

, `destutter (<) [1, 2, 5, 2, 3, 4, 9] = [1, 2, 5, 9]`

.

## Equations

- List.destutter R x = match x with | h :: l => List.destutter' R h l | [] => []

Given a decidable predicate `p`

and a proof of existence of `a ∈ l∈ l`

such that `p a`

,
choose the first element with this property. This version returns both `a`

and proofs
of `a ∈ l∈ l`

and `p a`

.

## Equations

- One or more equations did not get rendered due to their size.
- List.chooseX p [] hp = False.elim (_ : False)

Given a decidable predicate `p`

and a proof of existence of `a ∈ l∈ l`

such that `p a`

,
choose the first element with this property. This version returns `a : α`

, and properties
are given by `choose_mem`

and `choose_property`

.

## Equations

- List.choose p l hp = ↑(List.chooseX p l hp)

`mapDiagM' f l`

calls `f`

on all elements in the upper triangular part of `l × l× l`

.
That is, for each `e ∈ l∈ l`

, it will run `f e e`

and then `f e e'`

for each `e'`

that appears after `e`

in `l`

.

Example: suppose `l = [1, 2, 3]`

. `mapDiagM' f l`

will evaluate, in this order,
`f 1 1`

, `f 1 2`

, `f 1 3`

, `f 2 2`

, `f 2 3`

, `f 3 3`

.

## Equations

- List.mapDiagM' f [] = pure ()
- List.mapDiagM' f (x_1 :: xs) = do let __discr ← f x_1 x_1 let x : Unit := __discr let __discr ← mapM' (f x_1) xs let x : List Unit := __discr List.mapDiagM' f xs

Map each element of a `List`

to an action, evaluate these actions in order,
and collect the results.

## Equations

- List.traverse f [] = pure []
- List.traverse f (x_1 :: xs) = Seq.seq (List.cons <$> f x_1) fun x => List.traverse f xs

Left-biased version of `List.map₂`

. `map₂Left' f as bs`

applies `f`

to each
pair of elements `aᵢ ∈ as∈ as`

and `bᵢ ∈ bs∈ bs`

. If `bs`

is shorter than `as`

, `f`

is
applied to `none`

for the remaining `aᵢ`

. Returns the results of the `f`

applications and the remaining `bs`

.

```
map₂Left' prod.mk [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])
map₂Left' prod.mk [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
```

## Equations

- List.map₂Left' f [] x = ([], x)
- List.map₂Left' f (a :: as) [] = (List.map (fun a => f a none) (a :: as), [])
- List.map₂Left' f (a :: as) (b :: bs) = let rec' := List.map₂Left' f as bs; (f a (some b) :: rec'.fst, rec'.snd)

Right-biased version of `List.map₂`

. `map₂Right' f as bs`

applies `f`

to each
pair of elements `aᵢ ∈ as∈ as`

and `bᵢ ∈ bs∈ bs`

. If `as`

is shorter than `bs`

, `f`

is
applied to `none`

for the remaining `bᵢ`

. Returns the results of the `f`

applications and the remaining `as`

.

```
map₂Right' prod.mk [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])
map₂Right' prod.mk [1, 2] ['a'] = ([(some 1, 'a')], [2])
```

## Equations

- List.map₂Right' f as bs = List.map₂Left' (flip f) bs as

Left-biased version of `List.map₂`

. `map₂Left f as bs`

applies `f`

to each pair
`aᵢ ∈ as∈ as`

and `bᵢ ∈ bs∈ bs∈ bs`

. If `bs`

is shorter than `as`

, `f`

is applied to `none`

for the remaining `aᵢ`

.

```
map₂Left Prod.mk [1, 2] ['a'] = [(1, some 'a'), (2, none)]
map₂Left Prod.mk [1] ['a', 'b'] = [(1, some 'a')]
map₂Left f as bs = (map₂Left' f as bs).fst
```

## Equations

- List.map₂Left f [] x = []
- List.map₂Left f (a :: as) [] = List.map (fun a => f a none) (a :: as)
- List.map₂Left f (a :: as) (b :: bs) = f a (some b) :: List.map₂Left f as bs

Right-biased version of `List.map₂`

. `map₂Right f as bs`

applies `f`

to each
pair `aᵢ ∈ as∈ as`

and `bᵢ ∈ bs∈ bs∈ bs`

. If `as`

is shorter than `bs`

, `f`

is applied to
`none`

for the remaining `bᵢ`

.

```
map₂Right Prod.mk [1, 2] ['a'] = [(some 1, 'a')]
map₂Right Prod.mk [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]
map₂Right f as bs = (map₂Right' f as bs).fst
```

## Equations

- List.map₂Right f as bs = List.map₂Left (flip f) bs as

Asynchronous version of `List.map`

.

## Equations

- List.mapAsyncChunked f xs chunk_size = List.bind (List.map (fun xs => Task.spawn fun x => List.map f xs) (List.toChunks chunk_size xs)) Task.get

We add some n-ary versions of `List.zipWith`

for functions with more than two arguments.
These can also be written in terms of `List.zip`

or `List.zipWith`

.
For example, `zipWith3 f xs ys zs`

could also be written as
`zipWith id (zipWith f xs ys) zs`

or as
`(zip xs $ zip ys zs).map $ λ ⟨x, y, z⟩, f x y z`

.

Ternary version of `List.zipWith`

.

## Equations

- List.zipWith3 f (x_3 :: xs) (y :: ys) (z :: zs) = f x_3 y z :: List.zipWith3 f xs ys zs
- List.zipWith3 f x x x = []

Quaternary version of `list.zipWith`

.

## Equations

- List.zipWith4 f (x_4 :: xs) (y :: ys) (z :: zs) (u :: us) = f x_4 y z u :: List.zipWith4 f xs ys zs us
- List.zipWith4 f x x x x = []

Quinary version of `list.zipWith`

.

## Equations

- List.zipWith5 f (x_5 :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) = f x_5 y z u v :: List.zipWith5 f xs ys zs us vs
- List.zipWith5 f x x x x x = []

Given a starting list `old`

, a list of booleans and a replacement list `new`

,
read the items in `old`

in succession and either replace them with the next element of `new`

or
not, according as to whether the corresponding boolean is `true`

or `false`

.