## Stream: Coq users

### Topic: ✔ Factorisation of natural number

#### Lessness (May 03 2022 at 19:39):

What would be the best way to make a function that factorizes `nat` (lists all prime factors, probably in increasing order). For example, 60 becomes list [2, 2, 3, 5]. Any hints? Meanwhile I will try my luck myself, too.

#### Pierre Roux (May 03 2022 at 19:54):

You can have a look at `prime_decomp` in MathComp: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/prime.v

#### Lessness (May 03 2022 at 20:36):

Another question... I'm trying to write such function:

``````Function all_factors_geq_limit (n k: nat) (H: (k > 1)%nat) { measure id n }: list nat :=
if Nat.eq_dec n 0%nat
then 0%nat :: nil
else if Nat.eq_dec n 1%nat
then nil
else if le_dec n k
then n :: nil
else if nat_divide_dec k n
then k :: all_factors_geq_limit (Nat.div n k) k H
else all_factors_geq_limit n (S k) (le_S _ _ H).
``````

But I am not successful in writing the correct measure... I tried to write smth like `{ measure id (n - k) } but that fails with error.

#### Li-yao (May 03 2022 at 21:25):

What error? Do you have `From Coq Require Import Recdef`?

#### Lessness (May 03 2022 at 21:41):

`Decreasing argument must be specified in measure clause.`
Yes, i have imported Recdef.

#### Lessness (May 03 2022 at 21:50):

Does the following work for you? It doesn't for me. :(

``````Require Import ZArith Znumtheory.
Open Scope Z.

Eval compute in (if prime_dec 4 then true else false).
(* Does not return false (or true, for that matter). *)
``````

#### Lessness (May 03 2022 at 21:53):

It seems that `natlike_rec` is opaque or smth like that.

#### Li-yao (May 03 2022 at 22:25):

Oh I see, you get an error when you try `n-k` as a measure, because it can only be defined on one of the arguments. In that case you could try bundling it up in one argument. It's also better to drop the precondition `H` and to just check for it in the definition because it seems `Function` doesn't like dependent types too much:

``````Function all_factors_geq_limit (nk : nat * nat) { measure (fun '(n,k) => n - k) }: list nat :=
let '(n,k) := nk in
if Nat.eq_dec k 0%nat then nil else
if Nat.eq_dec k 1%nat then nil else
if Nat.eq_dec n 0%nat
then 0%nat :: nil
else if Nat.eq_dec n 1%nat
then nil
else if le_dec n k
then n :: nil
else if nat_divide_dec k n
then k :: all_factors_geq_limit (Nat.div n k, k)
else all_factors_geq_limit (n, S k).
``````

#### Karl Palmskog (May 04 2022 at 06:44):

for big numbers, we recommend CoqPrime and associated tools for factoring into primes, all part of the Coq Platform

#### Lessness (May 04 2022 at 18:15):

Can someone help to solve `prime_dec` problem? :thinking:

#### Paolo Giarrusso (May 04 2022 at 20:31):

vm_compute might help: it bypasses Opaque. But it does not bypass Qed. Yes, those two are very different kinds of opacity.

#### Lessness (May 04 2022 at 20:33):

`vm_compute` doesn't help, but thanks anyway.

#### Lessness (May 04 2022 at 20:34):

Should I make a bug report? Or am I too hasty?

#### Lessness (May 04 2022 at 21:04):

I have another problem. I made a `Function` that removes given factor from the number by repeated division.
Sadly it takes forever even for such small numbers as 4 and 2. :( What am I doing wrong here?

``````Require Import VST.floyd.proofauto.
Require Import FunInd.
Require Import Znumtheory.

Open Scope Z.

Function remove_factor (n k: Z) {measure Z.to_nat n}: Z :=
if Z_le_lt_dec k 1
then n
else
if Z_le_lt_dec n 1
then n
else
if Zdivide_dec k n
then remove_factor (Z.div n k) k
else n.
Proof.
intros. clear teq teq0 teq1. destruct anonymous1. subst. rewrite Z.div_mul; try abstract lia. abstract nia.
Defined.

Eval compute in remove_factor 4 2.
``````

#### Kenji Maillard (May 04 2022 at 21:16):

As a rule of thumb, any definition/lemma that returns a proof (such as `prime_dec` or `Z_le_lt_dec`) is probably not well suited for computations. In order to write functions that do compute it is often better to use boolean valued decision procedure (and specification lemmas relating the result fo such procedure to the property of interest). For instance, in the mathcomp file prime.v linked before in this thread you can find a boolean predicate `prime` indicated as geared towards computing in the comments, plus lemmas `primeP` and `primePn` specifying this function for reasoning on the result.

#### Lessness (May 04 2022 at 21:20):

I agree and I'm not going to use them for computation. I just wanted to test them with tiny numbers and it seems that they both don't compute somehow even for miniscule input. At least for me, and it looks like a problem.

Computations will be done using C program. (Which is going to be formally verified solution to Project Euler problem #3... in some far future.)

#### Paolo Giarrusso (May 04 2022 at 21:26):

Functions returning proofs often need some Qed, in which case they won't compute, even for small inputs.

#### Lessness (May 04 2022 at 21:33):

`remove_factor` doesn't have any visible `Qed`, but it's not computing anyway. :/
And `prime_dec` should compute at least for some small inputs in reasonable time, in my opinion, otherwise I can only call it a bug.

#### Gaëtan Gilbert (May 04 2022 at 21:34):

I don't have vst installed so can't test that exact code, but on coq master

``````Require Import FunInd Recdef.
Require Import ZArith.
Require Import Lia.

Open Scope Z.

Function remove_factor (n k: Z) {measure Z.to_nat n}: Z :=
if Z_le_gt_dec k 1
then n
else
if Z_le_gt_dec n 1
then n
else
if Zdivide_dec k n
then remove_factor (Z.div n k) k
else n.
Proof.
intros. clear teq teq0 teq1. destruct anonymous1. subst. rewrite Z.div_mul; try abstract lia. abstract nia.
Defined.

Eval compute in remove_factor 4 2.
``````

is fast

#### Gaëtan Gilbert (May 04 2022 at 21:35):

Is Z_le_lt_dec a qed definition?

#### Gaëtan Gilbert (May 04 2022 at 21:36):

for instance

``````Require Import FunInd Recdef.
Require Import Znumtheory ZArith.
Require Import Lia.

Open Scope Z.

Lemma Z_le_gt_dec' : ltac:(let t := type of Z_le_gt_dec in exact t).
Proof. exact Z_le_gt_dec. Qed.

Function remove_factor (n k: Z) {measure Z.to_nat n}: Z :=
if Z_le_gt_dec' k 1
then n
else
if Z_le_gt_dec' n 1
then n
else
if Zdivide_dec k n
then remove_factor (Z.div n k) k
else n.
Proof.
intros. clear teq teq0 teq1. destruct anonymous1. subst. rewrite Z.div_mul; try abstract lia. abstract nia.
Defined.

Eval compute in remove_factor 4 2.
``````

is slow

#### Lessness (May 04 2022 at 21:38):

Yes, big thank you! :)

Z_le_lt_dec comes from VST (https://github.com/PrincetonUniversity/VST/blob/d1687ef4d9e503f1cea674058b4b1d415a674302/zlist/list_solver.v), as I found out right now, and it is indeed a Qed definition.

My mistake.

#### Lessness (May 04 2022 at 21:40):

I changed `Z_le_lt_dec` to `Z_le_gt_dec` and now it computes. Thank you very much!

#### Lessness (May 05 2022 at 08:24):

Any hints how to prove the theorem `remove_factor_decreasing`? I am stuck with the proof and am doing something wrong, I believe.

``````Require Import FunInd Recdef ZArith Znumtheory Lia.
Open Scope Z.

Function remove_factor (n k: Z) {measure Z.to_nat n}: Z :=
if Z_le_gt_dec k 1 then n else
if Z_le_gt_dec n 1 then n else
if Zdivide_dec k n
then remove_factor (Z.div n k) k
else n.
Proof.
intros. clear teq teq0 teq1. destruct anonymous1. subst. rewrite Z.div_mul; try lia. nia.
Defined.

Theorem remove_factor_decreasing (n k: Z) (H: k > 1) (H0: n > 1) (H1: Z.divide k n): remove_factor n k < n.
Proof.
assert (0 <= n) by lia. revert H0 H1. pattern n. apply Z_lt_induction.
+ intros. destruct H3. subst. rewrite remove_factor_equation.
repeat destruct Z_le_gt_dec; try lia.
destruct Zdivide_dec.
- rewrite Z.div_mul; try lia. clear d g g0.
assert (0 <= x0 < x0 * k) by nia.
- exfalso. apply n0. exists x0. auto.
+ lia.
``````

#### Lessness (May 05 2022 at 08:37):

Ok, I managed to prove that.

``````Theorem remove_factor_decreasing (n k: Z) (H: k > 1) (H0: n > 1) (H1: Z.divide k n): remove_factor n k < n.
Proof.
assert (0 <= n) by lia. revert H0 H1. pattern n. apply Z_lt_induction.
+ intros. destruct H3. subst. rewrite remove_factor_equation.
repeat destruct Z_le_gt_dec; try lia.
destruct Zdivide_dec.
- rewrite Z.div_mul; try lia. clear d g g0.
assert (0 <= x0 < x0 * k) by nia.
destruct (Z_le_gt_dec x0 1).
* assert (x0 = 0 \/ x0 = 1) by lia. destruct H4.
++ subst. lia.
++ subst. rewrite remove_factor_equation. destruct Z_le_gt_dec.
-- lia.
-- destruct Z_le_gt_dec. lia. lia.
* destruct (Zdivide_dec k x0).
++ pose (H0 _ H3 g d). nia.
++ rewrite remove_factor_equation.
destruct Z_le_gt_dec; try lia.
destruct Z_le_gt_dec; try lia.
destruct Zdivide_dec; intuition.
- exfalso. apply n0. exists x0. auto.
+ lia.
Qed.
``````

#### Notification Bot (May 05 2022 at 20:43):

Lessness has marked this topic as resolved.

Last updated: Sep 30 2023 at 06:01 UTC