Coq - доказательство того, что уже определено? - PullRequest
Новая
       7

Coq - доказательство того, что уже определено?

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

Принимая очень прямое доказательство "сумма двух натуральных чисел нечетна, если одно из них четное, а другое нечетное": 

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.

Lemma sum_odd_even : forall n m, odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
Proof.
  intros n. intros m. left.
  destruct H. firstorder.

Состояние в конце этого блока кода: 

2 subgoals
n, m, x : nat
H : n + m = 2 * x + 1
______________________________________(1/2)
odd n
______________________________________(2/2)
even m

Насколько я понимаю, это говорит мне, что я должен доказать ему, что у меня есть нечетное число n и четное число m в гипотезе? Хотя я уже говорил, что n нечетно, а m четно? Как мне продолжить отсюда?

UPDATE:

После небольшого волнения (в свете комментариев), я думаю, мне придется сделать что-то подобное? 

Lemma even_or_odd: forall (n: nat), even n \/ odd n.
Proof.
  induction n as [|n IHn].
  (* Base Case *)
  left. unfold even. exists 0. firstorder.
  (* step case *)
  destruct IHn as [IHeven | IHodd].
  right. unfold even in IHeven. destruct IHeven as [k Heq].
  unfold odd. exists k. firstorder.
  left. unfold odd in IHodd. destruct IHodd as [k Heq].
  unfold even. exists (k + 1). firstorder.
Qed.

Что означает, что сейчас: 

Lemma sum_odd : forall n m, odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
Proof.
  intros n. intros m. left. destruct H. firstorder.
  pose proof (even_or_odd n). pose proof (even_or_odd m).

Результат: 

    2 subgoals
n, m, x : nat
H : n + m = 2 * x + 1
H0 : even n \/ odd n
H1 : even m \/ odd m
______________________________________(1/2)
odd n
______________________________________(2/2)
even m

Интуитивно все, что я сделал, это сказал, что каждое число является либо четным, либо нечетным. Теперь я должен сказать coq, что мои нечетные и четные числа действительно нечетные и четные (наверное?).

ОБНОВЛЕНИЕ 2:

Кроме того, проблема решаема только с помощью первого порядка: 

Lemma sum_odd : forall n m, odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
Proof.
  intros n. intros m. firstorder.
  pose proof (even_or_odd n). pose proof (even_or_odd m).
  destruct H0 as [Even_n | Odd_n]. destruct H1 as [Even_m | Odd_m].
  exfalso. firstorder.
  right. auto.
  destruct H1. left. auto.
  exfalso. firstorder.
Qed.

1 Ответ

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

Ваше использование left по-прежнему неверно и не позволяет вам завершить доказательство. Вы применяете это для достижения следующей цели: 

odd (n + m) -> odd n /\ even m \/ even n /\ odd m

и это дает: 

H : odd (n + m)
______________________________________(1/1)
odd n /\ even m

Вы обязуетесь доказать, что если n + m нечетно, то n нечетно, а m четно. Но это не так: n может быть нечетно и m может быть даже Применяйте left или right только тогда, когда у вас достаточно информации в контексте, чтобы убедиться, какую именно информацию вы хотите доказать.

Итак, давайте перезагрузим без left: 

Lemma sum_odd : forall n m, odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
Proof.
  intros n. intros m. firstorder.
  pose proof (even_or_odd n). pose proof (even_or_odd m).

На данный момент мы находимся по адресу: 

H : n + m = 2 * x + 1
H0 : even n \/ odd n
H1 : even m \/ odd m
______________________________________(1/1)
odd n /\ even m \/ even n /\ odd m

Теперь вы хотите доказать что-то из дизъюнкций. Чтобы доказать что-то вроде A \/ B -> C в конструктивной логике Кока, вы должны доказать и A -> C и B -> C. Вы делаете это путем анализа кейса на A \/ B (используя destruct или другую тактику). В этом случае у нас есть две дизъюнкции для разложения: 

  destruct H0 as [Even_n | Odd_n], H1 as [Even_m | Odd_m].

Это дает четыре случая. Я покажу вам первые два, последние два симметричны.

Футляр: 

H : n + m = 2 * x + 1
Even_n : even n
Even_m : even m
______________________________________(1/1)
odd n /\ even m \/ even n /\ odd m

Предположения противоречивы: если и n, и m четные, то H не может удержаться. Мы можем доказать это следующим образом: 

  - exfalso. destruct Even_n, Even_m. omega.

(Пройдите через это, чтобы понять, что происходит!) exfalso не является действительно необходимым, но это хорошая документация, что мы проводим доказательство, показывая, что предположения противоречат.

Второй случай: 

H : n + m = 2 * x + 1
Even_n : even n
Odd_m : odd m
______________________________________(1/1)
odd n /\ even m \/ even n /\ odd m

Теперь , зная предположения, которые применяются в в этом случае , мы можем совершить правильное разобщение. Вот почему ваш left мешал вам прогрессировать! 

  - right.

Все, что остается доказать: 

Even_n : even n
Odd_m : odd m
______________________________________(1/1)
even n /\ odd m

И auto может справиться с этим.

...