O(n)
. Partial map. If f : Π a, P a → β
is a partial function defined on
a : α
satisfying P
, then pmap f l h
is essentially the same as map f l
but is defined only when all members of l
satisfy P
, using the proof
to apply f
.
Instances For
O(1)
. "Attach" a proof P x
that holds for all the elements of l
to produce a new list
with the same elements but in the type {x // P x}
.
Instances For
O(1)
. "Attach" the proof that the elements of l
are in l
to produce a new list
with the same elements but in the type {x // x ∈ l}
.
Equations
- l.attach = l.attachWith (Membership.mem l) ⋯
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
If we fold over l.attach
with a function that ignores the membership predicate,
we get the same results as folding over l
directly.
This is useful when we need to use attach
to show termination.
Unfortunately this can't be applied by simp
because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
If we fold over l.attach
with a function that ignores the membership predicate,
we get the same results as folding over l
directly.
This is useful when we need to use attach
to show termination.
Unfortunately this can't be applied by simp
because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
unattach #
List.unattach
is the (one-sided) inverse of List.attach
. It is a synonym for List.map Subtype.val
.
We use it by providing a simp lemma l.attach.unattach = l
, and simp lemmas which recognize higher order
functions applied to l : List { x // p x }
which only depend on the value, not the predicate, and rewrite these
in terms of a simpler function applied to l.unattach
.
Further, we provide simp lemmas that push unattach
inwards.
A synonym for l.map (·.val)
. Mostly this should not be needed by users.
It is introduced as an intermediate step by lemmas such as map_subtype
,
and is ideally subsequently simplified away by unattach_attach
.
If not, usually the right approach is simp [List.unattach, -List.map_subtype]
to unfold.
Instances For
Recognizing higher order functions on subtypes using a function that only depends on the value. #
This lemma identifies folds over lists of subtypes, where the function only depends on the value, not the proposition, and simplifies these to the function directly taking the value.
This lemma identifies folds over lists of subtypes, where the function only depends on the value, not the proposition, and simplifies these to the function directly taking the value.
This lemma identifies maps over lists of subtypes, where the function only depends on the value, not the proposition, and simplifies these to the function directly taking the value.