✔ Factorisation of natural number · Coq users

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

Lessness (May 03 2022 at 20:36):

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

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

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

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

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

Lessness (May 04 2022 at 20:34):

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

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.

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

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

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.

Lessness (May 04 2022 at 21:38):

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

Lessness (May 05 2022 at 08:37):

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.

Stream: Coq users

Topic: ✔ Factorisation of natural number

Lessness (May 03 2022 at 19:39):