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

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.

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.

Thank you for correction.

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.

`0`

is a unit for `gcd`

??

Wait nevermind.

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

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

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`

?

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

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

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

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

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`

.

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