I'm stuck trying to prove ∀x : ℕ, 3 | (x + 5x) with Coq

Question

Specifically, I think what's got me is showing that ∀x y z : ℕ, (z|x and z|y) → z|(x + y), or that ∀x y z : ℕ, (x mod y) = 0 → z mod y = (z + x) mod y, depending on how you want to look at it. I know those aren't exactly the same, but I believe either works for this purpose.

This proof is super easy to do on paper with weak induction, especially if you consider the problem as showing a property of pairs in an inductively defined set. One, because the algebra rules (factoring, principally) are given, and two, because I can succinctly write the set of all z|x as x = zk for some natural k.

I'm just having quite a bit of trouble formulating this in Coq terms. Here's what I've got. It feels like distinctly the wrong approach, but it's the best I can do with my very limited knowledge of Coq (and type based proofs in general, to be honest).

Theorem principal : forall x, eqb ((x + (5 * x)) mod 3) 0 = true.
Proof.
  induction x.
  - reflexivity.
  - rewrite special_factor_neutral. rewrite IHx. reflexivity.
Qed.

This obviously expects a special_factor_neutral lemma do do the heavy lifting, which I've been unable to define acceptably. Here it is.

Lemma special_factor_neutral : forall x,
  (((S x + 5 * S x)) mod 3) = (((x + 5 * x)) mod 3).
Proof. Admitted.

I suspect that with mod is not the ideal way to express divisibility in this problem — and the lemma clearly could be a good deal more general — but it's what I've got so far.

If you could suggest an alternate approach, or a way to make my current approach work, it would be greatly appreciated. To be clear, this is just for fun, so the stakes aren't very high, but I'd like to learn this stuff as well as possible.

Thank you!

Edit: I'm using Coq 8.12.2 in CoqIDE.

Answer 1

When proving this, you will likely want to use several lemmas from the standard library, especially those involving mod.

The first step, of course, is to figure out why what you are proving is actually true. Here, we can do a quick algebraic manipulation:

$(x + 5x) \equiv 6x \equiv 0 \mod 3$, as $6 \equiv 0 \mod 3$

In Coq, we should be able to replay this argument, proving the rules we intuitively used if we get stuck.

The first thing we want to do is change $x + 5x$ into $6x$. In this case, Coq can directly see that these terms are equal since they can be partially computed, and when you do this you get syntactically equivalent terms. This is called "evaluating to normal form" and happens whenever Coq tries to prove that two things are equal. This kind of equality is called computational equality. The tactic reflexivity (among other things) proves that two things are computationally equal (or fails if they are not).

So, you might extract this into a separate lemma, and then just prove it using reflexivity. Try to read up on Coq's reduction system if you are unsure why these two terms are computationally equal.

To continue, next we used the fact that $x*y \equiv x' * y' \mod z \Leftarrow (x \equiv x' \mod z) \wedge (y \equiv y' \mod z)$.

Unfortunately, that theorem is not that trivial, since it involves proving correctness of the concrete implementation of Coq's division algorithm, which is not particularly pretty. We are lucky, though, since this is part of the standard library. Just Require Import Coq.Init.Nat Coq.Arith.PeanoNat., and notice that Nat.mul_mod_idemp_l : forall a b n : nat, n <> 0 -> (a mod n * b) mod n = (a * b) mod n is exactly the version of the general equivalence above we need.

The standard library also contains a few more fundamental theorems, which you can use to derive the above. You might want to look at the implementation of div and divmod and in particular use the Nat.divmod_spec lemma, if you feel like this approach is cheating.

The way you find these lemmas is by using Search "mod", or even stronger by searching for ((?a * ?b) mod ?c).

In total, the proof becomes

Lemma total x : (x + (5 * x)) mod 3 = 0 mod 3.
Proof.
  assert ((x + 5*x) = 6*x) as -> by reflexivity.
  rewrite <- Nat.mul_mod_idemp_l.
  - reflexivity.
  - discriminate.
Qed.

All reflexivitiy instances are computational equalities. You might want to investigate why each of these actually hold by computation, i.e. reduce them by hand.

discriminate is used to prove that 3 <> 0. This holds in particular since we can find computationally how to tell these two apart, since both are constructed using different constructors (when considering the inductive definition of nat).

Answer 2

If you prefer an idiomatic short solution:

Require Import Arith. (* Basic definitions. *)
Require Import Ring. (* The ring tactic. *)

Include Nat. (* Part of PeanoNat, to get access to x|y notation. *)

Theorem mobostar : forall x, (3 | x + 5 * x).
Proof.
  intro x.
  exists (2 * x).
  ring.
Qed.

Answer 3

I've figured it out. Not pretty, but it does work.

Lemma plus_0 : forall x, x + 0 = x.
Proof.
  induction x.
  - reflexivity.
  - simpl. rewrite IHx. reflexivity.
Qed.

Lemma plus_comm : forall a b, a + b = b + a.
Proof.
  induction a.
  - intro b. rewrite plus_0. reflexivity.
  - intro b. rewrite <- plus_n_Sm. rewrite <- IHa. reflexivity.
Qed.

Lemma plus_assoc : forall a b c, a + b + c = a + (b + c).
Proof.
  induction a.
  - reflexivity.
  - intros b c. simpl. rewrite IHa. reflexivity.
Qed.

Lemma mul_dist : forall k x y, k * (x + y) = k * x + k * y.
Proof.
  induction k.
  - intros x y. reflexivity.
  - intros x y. simpl. rewrite IHk.
    replace (k*x+k*y) with (k*y+k*x).
    rewrite <- plus_assoc.
    replace (x+y+k*y) with (x + (y+k*y)).
    replace (y + k * y) with (S k * y).
    rewrite plus_comm.
    rewrite <- plus_assoc.
    replace (k*x+x) with (x+k*x).
    reflexivity.
    + rewrite plus_comm. reflexivity.
    + reflexivity.
    + rewrite plus_assoc. rewrite plus_comm. reflexivity.
    + rewrite plus_comm. reflexivity.
Qed.

Lemma times_0 : forall a, a * 0 = 0.
Proof.
  induction a.
  - reflexivity.
  - simpl. rewrite IHa. reflexivity.
Qed.

Lemma mul_comm : forall a b, a * b = b * a.
Proof.
  induction a.
  - intro b. rewrite times_0. reflexivity.
  - intro b. rewrite <- mult_n_Sm. rewrite <- IHa.
    rewrite plus_comm. reflexivity.
Qed.

Lemma mul_assoc : forall a b c, a * b * c = a * (b * c).
Proof.
  induction a.
  - reflexivity.
  - intros b c. simpl. rewrite <- IHa.
    rewrite mul_comm. rewrite mul_dist.
    replace (c * (a * b)) with (a * b * c). rewrite mul_comm. reflexivity.
    + rewrite mul_comm. reflexivity.
Qed.

Lemma principal : forall x, 6 * x = 3 * (2 * x).
Proof.
  intro x. replace 6 with (3 * 2). rewrite mul_assoc. reflexivity.
  - reflexivity.
Qed.

Answer 4

Assuming you didn't want to recreate everything from scratch, I highly recommend checking out the ssreflect library, it can really trim down your proofs greatly. It comes bundled with the Coq installer (If you want to search for a proof, you can use the Search command)

For instance, here is the proof in SSReflect:

From mathcomp Require Import all_ssreflect.

Lemma three_div: forall x, 3 %| (x + 5*x).
move => x.
rewrite -{1}(mul1n x) -mulnDl addnE /=.
(have ->: 6 = 3*2 by done); rewrite -mulnA.
exact/dvdn_mulr/dvdnn.
Qed.

First line transforms it into 3 %| 6x, second one writes it into 3 %| 3 * (2*x) then the last one just concludes.

Hope this was helpful :)