CODEWITHSUNDEEP
coqinteger-arithmetic
Aalok Thakkar
Aalok Thakkar

Reputation: 31

Writing proofs of simple arithmetic in Coq

I would like to prove simple things like for every natural number n, there exists a natural number k such that:

(2*n + 1)^2 = 8*k + 1

How does one go about such a proof? I thought of dividing it into cases when n is odd or even, but I do not know how to do so in Coq. Also, is there an inbuilt power (exponent) operator in Coq?

Upvotes: 3

Views: 1021

Answers (3)

Yves
Yves

Reputation: 4236

We can follow the initial plan suggested in the question of reasoning by cases on whether the input is odd or even, only representing parity by the value of n mod 2 and using a boolean equality test to express the alternative.

The proof can also be made with relative integers instead of natural numbers.

From Coq Require Import ZArith Psatz.

Open Scope Z_scope.

Lemma example n : exists k,  (2 * n + 1) ^2 = 8 * k + 1.
Proof.
assert (vn : n = 2 * (n / 2) + n mod 2) by now apply Z_div_mod_eq.
destruct (n mod 2 =? 0) eqn: q.
-  rewrite Z.eqb_eq in q; rewrite vn, q.
exists ((2 * (n / 2) + 1) * (n / 2)); ring.
-  enough (vm : n mod 2 = 1)
    by now rewrite vn, vm; exists (2 * (n / 2) ^ 2 + 3 * (n / 2) + 1); ring.
rewrite Z.eqb_neq in q.
assert (0 <= n mod 2 < 2) by now apply Z_mod_lt.
lia.
Qed.

This proof is not as nice and elementary as the one by @Anton on Jan 24th, though.

Upvotes: 1

Anton Trunov
Anton Trunov

Reputation: 15404

Here is an alternative proof, using the same idea as found in the proof by @Yves:

From Coq Require Import Arith Psatz.

Fact exampleNat n : exists k, (2 * n + 1) ^2 = 8 * k + 1.
Proof.
  exists (n * (S n) / 2).
  assert (H : Nat.even (n * (S n)) = true) by
    now rewrite Nat.even_mul, Nat.even_succ, Nat.orb_even_odd.
  apply Nat.even_spec in H as [m H]; rewrite (Nat.mul_comm 2) in H.
  rewrite H, Nat.div_mul, Nat.pow_2_r; lia.
Qed.

Observe that this proof schema works for the integer numbers too provided you change everything from namespace Nat to Z (S to Z.succ, etc.).

Upvotes: 1

Anton Trunov
Anton Trunov

Reputation: 15404

Yes, there are many built-in functions, you just need the right set of imports or open the right notation scope. One easy way to do the proof is to use induction and some automation like ring, omega or lia tactics.

From Coq Require Import Arith Psatz.

Goal forall n, exists k, (2*n + 1)^2 = 8*k + 1.
Proof.
  induction n as [| n [m IH]].
  - now exists 0.
  - exists (S n + m). rewrite Nat.pow_2_r in *. lia.
Qed.

Upvotes: 6

Related Questions