Написание доказательств простой арифметики в Coq

Я хотел бы доказать простые вещи, например, для каждого натурального числа n существует натуральное число k такое, что:

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

Как можно получить такое доказательство? Думал разбить на случаи, когда n нечетно или четно, но не знаю, как это сделать в Coq. Кроме того, есть ли в Coq встроенный оператор мощности (экспоненты)?


integer-arithmetic coq
person Aalok Thakkar    schedule 24.01.2018    source источник

Ответы (3)


arrow_upward
5
arrow_downward

Да, есть много встроенных функций, вам просто нужен правильный набор импортов или открытая правильная область нотации. Один из простых способов сделать доказательство — использовать индукцию и некоторую автоматизацию, например ring. , omega или lia тактики.

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.
person Anton Trunov    schedule 24.01.2018

arrow_upward
1
arrow_downward

Вот альтернативное доказательство, использующее ту же идею, что и в доказательстве @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.powNatr; lia.
Qed.

Обратите внимание, что эта схема доказательства работает и для целых чисел, если вы измените все пространство имен с Nat на Z (с S на Z.succ и т. д.).

person Anton Trunov    schedule 26.01.2018

arrow_upward
1
arrow_downward

Мы можем следовать первоначальному плану, предложенному в вопросе о рассуждениях по прецедентам о том, являются ли входные данные четными или нечетными, только представляя четность значением n mod 2 и используя булев тест на равенство для выражения альтернативы.

Доказательство также может быть сделано с относительными целыми числами вместо натуральных чисел.

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.

Однако это доказательство не такое красивое и элементарное, как доказательство @Anton от 24 января.

person Yves    schedule 26.01.2018