Stream: Coq users

Topic: gcd of list

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

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.

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.

zeesha huq (Jun 02 2021 at 01:28):

Thank you for correction.

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.

Cody Roux (Jun 03 2021 at 21:34):

`0` is a unit for `gcd`??

Wait nevermind.

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

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

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

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

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.

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

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

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

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: May 24 2024 at 22:02 UTC