Prime factorisation and decomposition

[siddhartha-gadgil]

The overall goal is the existence and uniqueness (up to permutation) of the prime decomposition. But there are many steps along the way.

Primes and Composites

• One can define two types :
  • Factorization n = (a, b, n = a * b, a > 1, b > 1)
  • Prime n = (n > 1, (n= a * b) -> (a = 1) | (b = 1))
• Define a function that given n either gives a factorisation of n or a proof that it is a prime.
  • this involves a lot of steps and helpers, including decidability of divisibility.

Existence of prime factorisation

• One should output
  • a list/vector
  • proofs that all entries are prime: can have a list of pairs (m : Nat ** Prime m) to combine the values with proofs.
  • a proof that the list/vector folded by multiplication gives the number n

Uniqueness

• It may be convenient to add the property of being ordered to the output of the factorisation, so equality is the usual one, not up to permutation
• The proof of uniqueness involves Bezout's lemma, to show p divides mn => (p divides m) or (p divides n)

[bnag098]

I am having some trouble in using the replace function.
I was trying to substitute $$ 0 $$ using the equality $$ 0 = b \cdot 0 $$ in $$c = 0 + c$$ to hopefully get $$c = b \cdot 0 + c $$.
But in the function call below:

replace (sym (multZeroRightZero b)) (sym (plusZeroLeftNeutral c)),

I am getting an error claiming that in the second variable of replace, idris expects a value of the type P 0. The documentation on thisP function couldn't clarify much. Any inputs here would be much appreciated.