Stream: Coq users

Topic: gcd of list


view this post on Zulip zeesha huq (May 31 2021 at 03:54):

I have defined a function to find greatest common divisor(gcd) of elements of natural number list. It has two issues (#1)I get
1 as output against two different constructors(first and second constructors of gcd_function) (#2)First three constructors are free
from the effect of input nat argument (gcd_num). Is there any way to correct this definition? Here is code

Fixpoint gcd_function (gcd_num : nat) (l : list nat) :=
match l with
| nil => 1
| a::nil=> 1
| a::a'::nil=> (gcd a a')
| a::a'::l1 => match (gcd_num) with
| O => 1
| S (gcd_num') => gcd_function (gcd_num') (gcd a a'::l1)
end
end.

Definition gcd_val l :=
match l with
| nil => 1
| a :: tl => gcd_function (length l) tl
end.

view this post on Zulip Michael Soegtrop (May 31 2021 at 06:58):

I am not sure what you want to achieve with the length argument. A plain function to compute the gcd of a list of numbers would be:

Require Import List.
Import ListNotations.
Import Nat.

Fixpoint gcd_function (l : list nat) :=
match l with
| nil => 1
| a::nil=> a
| a::tail => gcd a (gcd_function tail)
end.

Eval cbv in gcd_function [18; 24; 42].

In general it is not a good idea to introduce redundant information like the length of a list - a list knows how long it is. Redundant information is usually just an invitation to become inconsistent.

Btw: this would have costed me less time to answer, if you would have included the require statements - It took me a few minutes to find the gcd function. I keep repeating myself: please post code which compiles to the point of your question.

view this post on Zulip Michael Soegtrop (May 31 2021 at 07:09):

P.S.: it is rare that functions get correct by making them longer and longer. A common code review comment of a colleague is: "this function is so long, it must be wrong" - I never experienced that he was wrong with this assessment. So if functions don't do what you want, think of simpler ways of doing it - not more complicated ways.

view this post on Zulip zeesha huq (Jun 02 2021 at 01:28):

Thank you for correction.

view this post on Zulip Olivier Laurent (Jun 03 2021 at 12:24):

This is a typical use case for List.fold_right:

Definition gcd_function := fold_right gcd 0.

Then you can see it is strange to use 1 as base case in your definition (it is not a unit for gcd).
In particular you would miss gcd_function (l1 ++ l2) = gcd (gcd_function l1) (gcd_function l2) for example.

view this post on Zulip Cody Roux (Jun 03 2021 at 21:34):

0 is a unit for gcd??

view this post on Zulip Cody Roux (Jun 03 2021 at 21:35):

Wait nevermind.

view this post on Zulip zeesha huq (Jun 05 2021 at 12:03):

Require Import List.
Import Omega.
Require Import NPeano.
Import Nat.
Fixpoint gcd_function (l : list nat) :=
match l with
| nil => 1
| a::nil=> a
| a::tail => gcd a (gcd_function tail)
end.
Lemma g_prime : forall (a b : nat)(l : list nat),
 a > 1 ->
 b > 1 ->
 0< gcd_function (a::b::l)->
 gcd a b=1 ->  modulo a b <> 0.
Proof.
intros . unfold not. intros.
rewrite (N_div_mod_eq a b) in H2 .

view this post on Zulip zeesha huq (Jun 05 2021 at 12:09):

I want o write a command which is equal to Z_div_mod_eq a b in case of natural numbers? So that I can simplify gcd a b =1

view this post on Zulip Michael Soegtrop (Jun 05 2021 at 13:02):

Olivier Laurent said:

This is a typical use case for List.fold_right:

Interesting, I didn't know that 0 is unit for gcd. Do you have a way to use fold_right for min and max?

view this post on Zulip Olivier Laurent (Jun 06 2021 at 20:23):

Michael Soegtrop said:

Do you have a way to use fold_right for min and max?

For a binary operation op with unit u, a general pattern to extend it to lists is:

Definition list_op := fold_right op u.

You can use this in the particular case of max with unit 0 over nat:

Definition list_max := fold_right max 0.

This is already defined in the standard library: list_max and list_sum.
However when there is no unit, for example with min over nat, there is no canonical value for list_op []. You can fix a default value for list_op [] or put it as a parameter in:

Definition list_min d l := match l with
| [] => d
| h :: t => fold_right min h t
end.

view this post on Zulip Michael Soegtrop (Jun 07 2021 at 08:14):

@Olivier Laurent : thanks - singling out the empty list case and using fold_right for all other cases is a readable and likely proof effort saving way of doing this! It didn't occur to me as yet.

view this post on Zulip Olivier Laurent (Jun 07 2021 at 09:17):

Regarding proofs of properties, it might be even more natural to use fold_left:

Definition list_min d l := match l with
| [] => d
| h :: t => fold_left min t h
end.

view this post on Zulip zeesha huq (Jun 08 2021 at 03:54):

I want to simplify gcd ab=1 by putting command valid for natural numbers and equal to (N_div_mod_eq a b).

Definition gcd_function l := fold_right gcd 0 l .
Lemma g_prime : forall (a b : nat)(l : list nat),
 a > 1 ->
 b > 1 ->
 0< gcd_function (a::b::l)->
 gcd a b=1 ->  modulo a b <> 0.
Proof.
intros . unfold not. intros.
rewrite (N_div_mod_eq a b) in H2 .

view this post on Zulip Michael Soegtrop (Jun 08 2021 at 07:10):

Is it really so difficult to supply Coq code which compiles including require statements? Also please use a current Coq if you want to discuss proofs. Coq 8.13 doesn't seem to have a lemma N_div_mod_eq. Otherwise you should at least state which version of Coq you are using - maybe you are lucky and find someone who is using the same version.

A note: I would think that gcd_function (a::b::l) is always larger than 0 if one of a or b is larger than 0. Since this premise is always True and the rest of the goal doesn't include the list l, it is unclear what you want to achieve with the list l.

view this post on Zulip Olivier Laurent (Jun 08 2021 at 07:22):

There seem to be many useless hypotheses in the statement and gcd_function apparently plays no role.
If this is what you are looking for, here is a proof a slightly generalized statement:

Require Import PeanoNat Lia.

Lemma g_prime a b : b > 1 ->
  Nat.gcd a b = 1 -> Nat.modulo a b <> 0.
Proof.
intros Hb Hg Hm.
assert (b <> 0) as Hmg%(Nat.gcd_mod a) by lia.
rewrite (Nat.gcd_comm b a), Hg, Hm in Hmg.
cbn in Hmg; lia.
Qed.

Last updated: Jan 31 2023 at 13:02 UTC