GCD and mod in Coq

Question

I'm stuck at a problem in Coq, would be great if anyone had any tips on how to break the problem down into smaller steps. The lemma is this:

Lemma gcd_prime : forall (a b : Z), a > 1 -> b > 1 -> 
  Z.gcd a b = 1 -> Zmod a b <> 0

That is, if a and b are coprime and higher than 1, a mod b is not 0.

This is where I'm stuck:

 p : positive
 p0 : positive
 H : Z.pos p > 1
 H0 : Z.pos p0 > 1
 H1 : Z.gcd (Z.pos p) (Z.pos p0) = 1
  ============================
  Z.pos p mod Z.pos p0 <> 0

After doing the intros and induction and removed the obvious cases.

Maybe I must rephrase the mod part into remainder instead? Or should I replace H1 with something weaker, like p <> p0?

Doing SearchAbout Zmod. returns a lot of lemmas, but I'm not sure on how to adapt them.

Regards

Olle

I find it usually helps, when stuck on a Coq proof, to write out how I would prove this in a traditional prose proof. Can you write that here ? That will help us see which next step you wish to take. — jbapple
@jbapple I don't know. I think I need simpler relations between gcd and mod. Or unfold the definitions so it's more explicit. — Olle Härstedt
In my experience, if I don't know how to do the paper proof, the resulting Coq proof has little value to me. I'd suggest you do the paper proof first. In my prose proof, I would use Bézout's identity: en.wikipedia.org/wiki/B%C3%A9zout%27s_identity — jbapple

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2014-10-26T15:55:00

SearchAbout and omega are your friends. Remember you can search things that mention several definitions at once, such as Z.gcd and 0. Here's a solution:

Require Import ZArith.

Open Scope Z_scope.

Lemma gcd_prime : forall (a b : Z), a > 1 -> b > 1 ->
  Z.gcd a b = 1 -> Zmod a b <> 0.
Proof.
  intros a b Ha Hb Hgcd Hmod.
  rewrite (Z_div_mod_eq a b), Hmod, Zplus_0_r in Hgcd; try omega.
  rewrite Z.gcd_comm, Z.gcd_mul_diag_l in Hgcd; omega.
Qed.

GCD and mod in Coq

1 Answers