Zulip Chat Archive

Stream: new members

Topic: Accessing properties of list elements while mapping them

Michael Stoll (Mar 13 2022 at 21:12):

I'm a bit stuck with the following problem. I want to convert the list of prime factors of a nonzero natural number a, a.factors : list ℕ, into a list of primes, say prime_factors a : list nat.primes. The obvious way to do this seems to be to use list.map to convert the elements from type to type nat.primes:

list.map (λ p, p, _⟩) a.factors

Now the underscore needs to be a proof of the fact that p is a prime. I know that p is a prime, from

((nat.mem_factors ha).mp _).left

where ha : a ≠ 0 and the underscore is a proof of p ∈ a.factors.

Now my question is, how I can introduce this knowledge into the function I want to use in list.map above?

Michael Stoll (Mar 13 2022 at 21:24):

Or maybe a different approach should be used?

Jakub Kądziołka (Mar 13 2022 at 21:30):

I think you need to find, or write, a function like map that gives you this as an assumption

Alex J. Best (Mar 13 2022 at 21:42):

Michael Stoll said:

Or maybe a different approach should be used?

I'm curious what you need a list of dosc#nat.primes for, its not used so much, people instead just tend to use docs#nat.prime_of_mem_factors when needed

Michael Stoll (Mar 13 2022 at 21:53):

OK, maybe this is an XY problem. What I really would like to have is something like

def prime_factors_as_finset_of_primes (a : ) : finset nat.primes := ...

that gives me the prime factors of a as a finset. The idea was to first convert the list of factors to a list of primes and then to turn the list into a finset.

Michael Stoll (Mar 13 2022 at 21:54):

But in any case, there should be a reasonable way of changing the type of the list elements to a subtype if we know that all the elements satisfy the relevant property?

Last updated: Dec 20 2023 at 11:08 UTC