Maps a partially defined function (defined on those terms of α that satisfy a predicate P) over
a list l : List α, given a proof that every element of l in fact satisfies P.
O(|l|). List.pmap, named for “partial map,” is the equivalent of List.map for such partial
functions.
“Attaches” individual proofs to a list of values that satisfy a predicate P, returning a list of
elements in the corresponding subtype { x // P x }.
O(1).
Equations
- l.attachWith P H = List.pmap Subtype.mk l H
“Attaches” the proof that the elements of l are in fact elements of l, producing a new list with
the same elements but in the subtype { x // x ∈ l }.
O(1).
This function is primarily used to allow definitions by well-founded
recursion that use higher-order functions (such as
List.map) to prove that an value taken from a list is smaller than the list. This allows the
well-founded recursion mechanism to prove that the function terminates.
Equations
- l.attach = l.attachWith (Membership.mem l) ⋯
Equations
Equations
Equations
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.
See however foldl_subtype below.
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.
See however foldr_subtype below.
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.
Maps a list of terms in a subtype to the corresponding terms in the type by forgetting that they satisfy the predicate.
This is the inverse of List.attachWith and 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.
This function is usually inserted automatically by Lean as an intermediate step while proving
termination. It is rarely used explicitly in code. It is introduced as an intermediate step during
the elaboration of definitions by well-founded
recursion. If this function is encountered in a proof
state, the right approach is usually the tactic simp [List.unattach, -List.map_subtype].
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.