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.
Edit: I'm using Coq 8.12.2 in CoqIDE.