четный (n + m) -> четный n / \ четный m \ / нечетный n / \ нечетный m - PullRequest
Новая
       10

четный (n + m) -> четный n / \ четный m \ / нечетный n / \ нечетный m

0 голосов
/ 02 мая 2018

Как мне доказать эту лемму: 

 Lemma even_plus_split n m :
 even (n + m) -> even n /\ even m \/ odd n /\ odd m.

Это единственные библиотеки и определения, которые можно использовать: 

 Require Import Arith.
 Require Import Coq.omega.Omega.

 Definition even (n: nat) := exists k, n = 2 * k.
 Definition odd  (n: nat) := exists k, n = 2 * k + 1.

Я новичок в Coq и запутался в этом. Можете ли вы дать мне решение? Заранее спасибо!

код пока: 

 Lemma even_plus_split n m :
   even (n + m) -> even n /\ even m \/ odd n /\ odd m.
 Proof.
   intros.
   unfold even.
   unfold even in H.
   destruct H as [k H].
   unfold odd.
   exists (1/2*k).

результат пока: 

 1 subgoal
 n, m, k : nat
 H : n + m = 2 * k
 ______________________________________(1/1)
 (exists k0 : nat, n = 2 * k0) /\ (exists k0 : nat, m = 2 * k0) \/
 (exists k0 : nat, n = 2 * k0 + 1) /\ (exists k0 : nat, m = 2 * k0 + 1)

Я просто хочу сделать k0 равным 1/2 * k, и поэтому я полагаю, что это имело бы смысл, но я не могу этого сделать.

Ответы [ 2 ]

0 голосов
/ 03 мая 2018

Кажется, что каждый, кто пытается ответить, танцует вокруг того факта, что вы на самом деле выбрали неверное направление для этого доказательства. Вот пример:

если n = 601 и m = 399, то n + m = 2 * 500, n = 2 * 300 + 1 и m = 2 * 199 + 1.

Между 500, 300 и 199 соотношение 1/2 нигде не появляется.

Тем не менее утверждение (четное n / \ четное m) / (нечетное n / \ нечетное m) определенно верно.

Итак, сейчас у вас больше математическая проблема, чем проблема Coq.

Вы должны сделать доказательство для универсально количественных чисел n и m, но каким-то образом это доказательство также должно работать для конкретных вариантов выбора этих чисел. Таким образом, в некотором смысле вы можете мысленно проверить свои доказательства на примерах.

0 голосов
/ 03 мая 2018

Я просто хочу сделать k0 равным 1/2 * k, и поэтому я полагаю, что это имеет смысл, но я не могу этого сделать.

Существует функция с именем Nat.div2, которая делит натуральное число на 2. Запуск Search Nat.div2.

Nat.le_div2: forall n : nat, Nat.div2 (S n) <= n
Nat.lt_div2: forall n : nat, 0 < n -> Nat.div2 n < n
Nat.div2_decr: forall a n : nat, a <= S n -> Nat.div2 a <= n
Nat.div2_wd: Morphisms.Proper (Morphisms.respectful eq eq) Nat.div2
Nat.div2_spec: forall a : nat, Nat.div2 a = Nat.shiftr a 1
Nnat.N2Nat.inj_div2: forall a : N, N.to_nat (N.div2 a) = Nat.div2 (N.to_nat a)
Nnat.Nat2N.inj_div2: forall n : nat, N.of_nat (Nat.div2 n) = N.div2 (N.of_nat n)
Nat.div2_double: forall n : nat, Nat.div2 (2 * n) = n
Nat.div2_div: forall a : nat, Nat.div2 a = a / 2
Nat.div2_succ_double: forall n : nat, Nat.div2 (S (2 * n)) = n
Nat.div2_odd: forall a : nat, a = 2 * Nat.div2 a + Nat.b2n (Nat.odd a)
Nat.div2_bitwise:
  forall (op : bool -> bool -> bool) (n a b : nat),
  Nat.div2 (Nat.bitwise op (S n) a b) = Nat.bitwise op n (Nat.div2 a) (Nat.div2 b)

Из них наиболее многообещающим кажется Nat.div2_odd: forall a : nat, a = 2 * Nat.div2 a + Nat.b2n (Nat.odd a). Если вы pose proof эту лемму, вы можете destruct (Nat.odd a) и использовать simpl, чтобы получить либо a = 2 * Nat.div2 a, либо a = 2 * Nat.div2 a + 1, для любого a, который вы выберете.

Это может не дать вам решения напрямую (я не уверен, что установка k0 в k / 2 - правильное решение), но если это не так, вы должны убедиться, что можете придумать, как доказать это факт на бумаге, прежде чем попробовать это в Coq. Coq очень хорошо убеждается, что вы не делаете никаких скачков логики, которые вам не разрешено делать; крайне плохо помочь вам понять, как доказать факт, который вы еще не знаете, как доказать.

...