Open Alizter opened 2 months ago
I've managed to prove the existence of factorizations, however the proof does not compute efficiently. This means you cannot do say Eval cbv in ...
to see what the factorisation should be. This leaves the following concrete things to do in the future for this issue:
<=
are contractible.
We should prove the fundamental theorem of arithmetic for
nat
andIsPrime
. The basic statement says that any givennat
has a factorisation and any two factorisations are unique up to a permutation of factors. There is also a generalisation to unique factorisation domains with a possible semiring variant.Another way to modify the statement for
nat
is to force uniqueness by enforcing an order of the prime factors of a given factorisation. Then the fundamental theorem of arithmetic essentially says that the type of factorisations of anat
is contractible.In our calculations in homotopy theory, it's not apparent how useful this theorem actually is given that we can always manually factor a concrete number. So I wouldn't say this issue is a top priority.
One place to draw inspiration from is the following: https://github.com/coq-contribs/fundamental-arithmetics/blob/master/primes.v