# Proving factors of GCD in Dafny

While trying to prove various properties of GCD I ran into a proof I am a bit stumped with. Gcd can be defined as the max element in the intersection of the divisors of two numbers. In the code I used the definition Factors() to represent the divisor set.

I had the intuition that the divisors of the GCD were equal to the intersection of the factors of the the two numbers. One direction is easy to prove but the other direction has me stuck. I found one approach, the idea is that if a factor is not a factor of GCD then it must be a factor of the dividend divided by the GCD (which should be the LCM but I haven't defined or proved that yet). However, I can't quite prove that the factor p itself doesn't have factors which belong to either set. I feel like the fact that any factor of p is also in the set of factor intersections means something but I can't quite connect it.

    lemma GcdFactors(x: pos, y: pos)
ensures Factors(x) * Factors(y) == Factors(Gcd(x,y))
{
FactorsContainsSelf(Gcd(x,y));
assert Gcd(x,y) <= x;
assert Gcd(x,y) <= y;
var s :| Gcd(x,y) * s == x;
assert s * Gcd(x,y) == x;
var t :| Gcd(x,y) * t == y;
assert t * Gcd(x,y) == y;
GcdRest(x,y, s, t);
assert forall p: pos :: p in Factors(x)*Factors(y) ==> p in Factors(Gcd(x,y)) by {
forall p: pos | p in Factors(x)*Factors(y)
ensures p in Factors(Gcd(x,y))
{
assert IsFactor(s, x);
assert IsFactor(t, y);
assert p <= Gcd(x,y);
assert IsFactor(p, Gcd(x,y)) by {
if p == Gcd(x,y) {
}else{
if !IsFactor(p, Gcd(x,y)) {
assert p !in Factors(Gcd(x,y));
assert p in Factors(x);
assert p in Factors(y);
FactorsMult(Gcd(x,y), s);
FactorsMult(Gcd(x,y), t);
FactorsContains1(Gcd(x,y));
assert p != 1;
assert p in Factors(s) by {
assert p in set d_x, d_y | d_x in Factors(Gcd(x,y)) && d_y in Factors(s) :: d_x * d_y;
if l: pos, m: pos :| l in Factors(Gcd(x,y)) && m in Factors(s) && l * m == p {
assert false;
}
}
assert p in Factors(t) by {
assert p in set d_x, d_y | d_x in Factors(Gcd(x,y)) && d_y in Factors(t) :: d_x * d_y;
if l: pos, m: pos :| l in Factors(Gcd(x,y)) && m in Factors(t) && l * m == p {
assert false;
}
}
assert p in Factors(s) * Factors(t);
// calc {
//     p * q;
//     Gcd(x,y)*s;
// }
// assert p*q/s == Gcd(x,y);
// calc {
//     p*r;
//     Gcd(x,y)*t;
// }
// assert p*r/t == Gcd(x,y);
assert false;
}
}
}
}
}
assert forall p: pos :: p in Factors(Gcd(x,y)) ==> p in Factors(x)*Factors(y) by {
forall p: pos | p in Factors(Gcd(x,y))
ensures p in Factors(x)*Factors(y)
{
var q :| p * q == Gcd(x,y);
assert q * p == Gcd(x,y);
var s' := q*s;
assert p * s' == x;
var t' := q*t;
assert p * t' == y;
assert IsFactor(p, x);
assert IsFactor(p, y);
}
}
}


The rest of the definitions.

    type pos = x: nat | 1 <= x witness 1
ghost predicate IsFactor(p: pos, x: pos) {
exists q: pos ::  p * q == x
}

ghost function Factors(x: pos): set<pos> {
set p: pos | p <= x  && IsFactor(p, x)  // error: set constructed must be finite
}
ghost function Max(s: set<pos>): pos
requires s != {}
{
MaxExists(s);
var x :| x in s && forall y :: y in s ==> y <= x;
x
}
lemma MaxExists(s: set<pos>)
requires s != {}
ensures exists x :: x in s && forall y :: y in s ==> y <= x
{
var x := FindMax(s);
}

ghost function FindMax(s: set<pos>): (max: pos)
requires s != {}
ensures max in s && forall y :: y in s ==> y <= max
{
var x :| x in s;
if s == {x} then
x
else
var s' := s - {x};
assert s == s' + {x};
var y := FindMax(s');
if x < y then y else x
}
ghost function Gcd(x: pos, y: pos): pos {
var common := Factors(x) * Factors(y);
assert 1 in common by {
FactorsContains1(x);
FactorsContains1(y);
}
Max(common)
}

ensures IsFactor(Gcd(x, y), x)
ensures IsFactor(Gcd(x, y), y)
ensures forall p: pos :: IsFactor(p, x) && IsFactor(p, y) ==> p <= Gcd(x, y)
{
forall p: pos | IsFactor(p, x) && IsFactor(p, y)
ensures p <= Gcd(x, y)
{
assert p in Factors(x) * Factors(y);
}
}
lemma FactorsContains1(x: pos)
ensures 1 in Factors(x)
{
assert 1 * x == x;
}

lemma FactorsContainsSelf(x: pos)
ensures x in Factors(x)
{
assert x * 1 == x;
}

lemma GcdRest(x: pos, y: pos, s: pos, t: pos)
requires Gcd(x,y) * s == x
requires Gcd(x,y) * t == y
ensures Gcd(s,t) == 1
ensures Factors(s) * Factors(t) == {1}
{
assert s * Gcd(x,y) == x;
assert IsFactor(s, x);
assert t * Gcd(x,y) == y;
assert IsFactor(t, y);
if Gcd(s,t) != 1 {
var p :| Gcd(s,t) * p == s;
var q :| Gcd(s,t) * q == t;
calc {
x;
Gcd(x,y) * s;
Gcd(x,y) * Gcd(s,t) * p;
}

assert IsFactor(Gcd(x,y) * Gcd(s,t), x);
calc {
y;
Gcd(x,y)*t;
Gcd(x,y)*Gcd(s,t)*q;
}
assert IsFactor(Gcd(x,y)*Gcd(s,t), y);
assert false;
}
FactorsContains1(s);
FactorsContains1(t);
if Factors(s) * Factors(t) != {1} {
assert Factors(s) * Factors(t) != {};
var x :| x in Factors(s) * Factors(t) && x != 1;
assert false;
}
}

• I don’t know if there are any Dafny users active here. If you get an answer elsewhere feel free to self-answer your question. Commented Jul 14 at 8:59

I am not surprised that there are not many Dafny users here (we seem to hangout on SO...) but I hoped that folks who are familiar with proving mathematical arguments in code here might ideas about how to prove the argument.

In the end if something is hard to show directly then induction is probably required. I found the approach in my copy of "Fundamental Proof Methods in Computer Science: A Computer-Based Approach" by Musser and Arkoudas p. 619-620 with similar but different definitions. I recreated their definitions and arguments and proved it in a round about way. Now with that understanding I was able to simplify it using my original definitions.

    lemma GcdGreatest(x: pos, y: pos)
ensures forall z :: z in Factors(x) * Factors(y) ==> IsFactor(z, Gcd(x,y))
decreases x + y
{
forall z | z in Factors(x) * Factors(y)
ensures IsFactor(z, Gcd(x, y))
{
if x == y {
GcdIdempotent(x);
assert IsFactor(z, Gcd(x, y));
}else if x < y {
ModPosLemma(x, y, z);
GcdSubtract(x, y);
GcdGreatest(x, y - x);
assert IsFactor(z, Gcd(x, y));
}else{
ModPosLemma(y, x, z);
GcdSymmetric(x, y);
GcdSubtract(y, x);
GcdGreatest(y, x - y);
assert IsFactor(z, Gcd(x, y));
}
}
}

    lemma GcdSymmetric(x: pos, y: pos)
ensures Gcd(x, y) == Gcd(y, x)
{
assert Factors(x) * Factors(y) == Factors(y) * Factors(x);
}

lemma GcdIdempotent(x: pos)
ensures Gcd(x, x) == x
{
FactorsContainsSelf(x);
assert x in Factors(x) * Factors(x);
}
lemma GcdSubtract(x: pos, y: pos)
requires x < y
ensures Gcd(x, y) == Gcd(x, y - x)
{
var p := Gcd(x, y);

// By the definition of Gcd, we know that p is a factor of both x and y,
// We now show that p is also a factor of y - x.
assert IsFactor(p, y - x) by {
var a :| p * a == x;
var b :| p * b == y;
calc {
y - x;
==
p * b - p * a;
==
p * (b - a);
}
}

// Hence, p is a common factor of x and y - x
var common := Factors(x) * Factors(y - x);
assert p in common;

// It remains to show that, among the common factors of x and
// y - x, p is the greatest
forall q | q in common
ensures q <= p
{
// q is a factor of both x and y - x, so a and b exist:
var a :| q * a == x;
var b :| q * b == y - x;
assert IsFactor(q, y) by {
calc {
y;
==
x + (y - x);
==
q * a + q * b;
==
q * (a + b);
}
}
// We just showed that q is a common factor of x and y.
assert q in Factors(x) * Factors(y);
// By the definition of Gcd(x, y), we then have that q <= p.
}
}
lemma ModPosLemma(x: pos, y: pos, z: pos)
requires x < y
requires IsFactor(z, x)
requires IsFactor(z, y)
ensures IsFactor(z, y - x)
{
var p :| z * p == x;
var q :| z * q == y;
assert q > p;
// assert p - q * (x/y) > 0;
calc {
y - x;
z * q - z * p;
z * (q-p);
}
assert IsFactor(z, y - x);
}


full code here