zeesha huq (May 31 2021 at 03:54): 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.
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??
Cody Roux (Jun 03 2021 at 21:35):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 .
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_rightforminandmax?
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.
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.
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.
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: Oct 13 2024 at 01:02 UTC