Accessing properties of list elements while mapping them

Stream: new members

[Michael Stoll]

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]

Or maybe a different approach should be used?

[Jakub Kądziołka]

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

[Alex J. Best]

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]

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]

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?