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
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
In particular you would miss
gcd_function (l1 ++ l2) = gcd (gcd_function l1) (gcd_function l2) for example.
0 is a unit for
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
Interesting, I didn't know that
0 is unit for
gcd. Do you have a way to use
Michael Soegtrop said:
Do you have a way to use
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
Definition list_max := fold_right max 0.
This is already defined in the standard library:
However when there is no unit, for example with
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
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
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