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.

You can have a look at `prime_decomp`

in MathComp: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/prime.v

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.

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

?

`Decreasing argument must be specified in measure clause.`

Yes, i have imported Recdef.

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). *)
```

It seems that `natlike_rec`

is opaque or smth like that.

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).
```

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

Can someone help to solve `prime_dec`

problem? :thinking:

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

`vm_compute`

doesn't help, but thanks anyway.

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

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.
```

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.

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.)

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

`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.

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

Is Z_le_lt_dec a qed definition?

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

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.

I changed `Z_le_lt_dec`

to `Z_le_gt_dec`

and now it computes. Thank you very much!

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.
admit.
- exfalso. apply n0. exists x0. auto.
+ lia.
Admitted.
```

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.
```

Lessness has marked this topic as resolved.

Last updated: Sep 30 2023 at 06:01 UTC