prime factorization

[Alizter]

In this PR we prove the first part of the fundamental theorem of arithmetic outlined in #2059. We show that any natural number has a factorisation into primes.

In order to do this we define IsComposite which checks if a natural number has a proper divisor. Now this allows us to partition nat into 4 parts, zero, one (unit), primes and composites.

I noticed that in the classical setting, the line between being not prime and composite is blurred due to classical logic. This means texts on elementary number theory rarely distinguish between these two concepts. In the constructive setting, it can be shown that they are equivalent since we can apply classical reasoning to IsComposite and IsPrime precisely because they are decidable.

This allows us to show that any natural has a prime divisor which can be iterated to provide a prime factorisation of any natural number.

Decidability of IsComposite required me to introduce a new list_exists predicate on lists which checks for a witness in a list satisfying a given predicate, analogous to for_all. This allows us to show decidability of certain existential statements as long as witnesses can be collected in a list (related to enumerability).

Unfortunately, I needed to tweak a lot of universe levels for example in Sum.v as the default Coq ones introduced too many "phantom" universes which didn't appear to have any bearing on the terms but caused proofs to be left hanging.

Hopefully, this PR can be improved a bit, but I will be slightly less active over the coming days.

As mentioned in #2059, showing that any two factorisations are unique upto permutation will be left to future work. We are missing a lot of material on permutations of lists so this will have to wait.

[jdchristensen]

I'm partway through reviewing this, but will have to come back and finish later. I'll push a commit that removes some universe annotations that aren't needed, but there is more that could be done like that. That commit also reduces universe variables in prod_empty_l.

[jdchristensen]

I'll look into the build failures later today. It builds for me locally.

[jdchristensen]

The error was in the tests, which I hadn't built locally. decidable_for_all had changed to having three universe variables, instead of two. But with an improvement to decidable_prod, this goes away.

[jdchristensen]

My last commit simplifies the proof of the prime factorization, in part by factoring out some things, but in part but using some shorter arguments. Probably some things could be cleaned up further.

[jdchristensen]

I still need a bit more time to finish reviewing this, but I'll do it soon.

[jdchristensen]

This doesn't really belong in Types/Sum.v. Maybe we need a Types/Iff.v file for everything involving iff? (Or Basics/Iff.v, if dependencies allow it.)

[Alizter]

Yes, I thought this was a bit funny too. It could perhaps go in Empty.v?

[jdchristensen]

I'd lean towards a separate file gathering results about iff, since that would make it easy to find what one needs when reasoning about iff results. And most results involve more than one operation (product, sum, negation, etc), so there is no obvious file to choose.

[jdchristensen]

Ok, this LGTM modulo gathering most iff results to one spot. I'd say that the results that are about iff itself would make sense in their own file, whereas results where iff is simply a hypothesis should stay where they are (like decidable_iff).

[Alizter]

I'm having a bit of trouble with the dependencies of Iff.v and Decidable.v. Some of the De Morgan laws require decidability as an assumption, however the decidability file requires some facts about Iff.v. For now, I will put the laws requiring decidability in Decidable. I don't see a clear way to make this separation currently.

[Alizter]

@jdchristensen Is this what you had in mind?

[jdchristensen]

Yes, that looks like a fine way to organize it. Alternatively, the Decidable class could be defined in Overture.v. In many cases, that's the only thing needed for users of Decidable.v, and it would follow the pattern of putting some of the very basic definitions in Overture.v. But I also think it's fine like this.

I noticed that the dual De Morgan's law only needs A to be decidable with the existing proof, so I dropped the assumption that B is decidable, and also added the symmetrical version.