Stream: Coq users

Topic: ✔ Factorisation of natural number


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Li-yao (May 03 2022 at 21:25):

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

view this post on Zulip Lessness (May 03 2022 at 21:41):

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

view this post on Zulip 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). *)

view this post on Zulip Lessness (May 03 2022 at 21:53):

It seems that natlike_rec is opaque or smth like that.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Lessness (May 04 2022 at 18:15):

Can someone help to solve prime_dec problem? :thinking:

view this post on Zulip 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.

view this post on Zulip Lessness (May 04 2022 at 20:33):

vm_compute doesn't help, but thanks anyway.

view this post on Zulip Lessness (May 04 2022 at 20:34):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (May 04 2022 at 21:35):

Is Z_le_lt_dec a qed definition?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Notification Bot (May 05 2022 at 20:43):

Lessness has marked this topic as resolved.


Last updated: May 24 2024 at 22:02 UTC