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
The head of a list, or the default element of the type is the list is nil
.
Equations
Instances For
The last element of a list, with the default if list empty
Equations
Instances For
findM tac l
returns the first element of l
on which tac
succeeds, and
fails otherwise.
Equations
Instances For
l.Forall p
is equivalent to ∀ a ∈ l, p a
, but unfolds directly to a conjunction, i.e.
List.Forall p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2
.
Equations
Instances For
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
.
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
Instances For
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
Instances For
An auxiliary function for defining permutations
. permutationsAux ts is
is the set of all
permutations of is ++ ts
that do not fix ts
.
Equations
Instances For
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
Instances For
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
Instances For
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
Instances For
Equations
Equations
dedup l
removes duplicates from l
(taking only the last occurrence).
Defined as pwFilter (≠)
.
dedup [1, 0, 2, 2, 1] = [0, 2, 1]
Equations
Instances For
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]
,
destutter' (≠) 1, [2, 3, 3] = [1, 2, 3]
, destutter' (<) 1 [2, 5, 2, 3, 4, 9] = [1, 2, 5, 9]
.
Equations
Instances For
Given a decidable predicate p
and a proof of existence of a ∈ l
such that p a
,
choose the first element with this property. This version returns both a
and proofs
of a ∈ l
and p a
.
Equations
Instances For
Given a decidable predicate p
and a proof of existence of a ∈ 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
Instances For
mapDiagM' f l
calls f
on all elements in the upper triangular part of l × l
.
That is, for each e ∈ 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
Instances For
Left-biased version of List.map₂
. map₂Left' f as bs
applies f
to each
pair of elements aᵢ ∈ as
and bᵢ ∈ 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
Instances For
Right-biased version of List.map₂
. map₂Right' f as bs
applies f
to each
pair of elements aᵢ ∈ as
and bᵢ ∈ 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
Instances For
Left-biased version of List.map₂
. map₂Left f as bs
applies f
to each pair
aᵢ ∈ as
and bᵢ ∈ 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
Instances For
Right-biased version of List.map₂
. map₂Right f as bs
applies f
to each
pair aᵢ ∈ as
and bᵢ ∈ 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
Instances For
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 <| fun ⟨x, y, z⟩ ↦ f x y z
.
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
.