Доказательство Coq для вычитания не коммутирует

Я хотел бы доказать, что вычитание не работает в Coq, но я застрял. Я считаю, что утверждение, которое я хотел бы доказать в Coq, было бы написано forall a b : nat, a <> b -> a - b <> b - a

Вот что у меня есть для доказательства.

Theorem subtraction_does_not_commute :
  forall a b : nat, a <> b -> a - b <> b - a.
Proof.
  intros a b C.
  unfold not; intro H.
  apply C.

Думаю, я мог бы использовать C : a <> b, чтобы противоречить цели a = b.


coq coq-tactic
person Mike Harris    schedule 18.05.2017    source источник
comment
Я предлагаю вам сначала доказать лемму для a < b -> a - b <> b -a. Вам нужно будет использовать индукцию.   -  person ejgallego    schedule 18.05.2017
comment
Однако напрямую доказать это не составляет особого труда.   -  person ejgallego    schedule 18.05.2017

Ответы (1)


arrow_upward
2
arrow_downward

Один из способов решить эту проблему - использовать индукцию по a. Однако если вы начнете доказательство с

intros a b C; induction a.

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

C : S a <> b
IHa : a <> b -> a - b <> b - a

Вы не сможете использовать гипотезу индукции IHa, потому что нельзя вывести предпосылку IHa (a <> b) из S a <> b: например, 1 <> 0 не означает 0 <> 0.

Но мы можем усилить гипотезу индукции, не вводя переменные в контекст преждевременно:

Require Import Coq.Arith.Arith.

Lemma subtraction_does_not_commute :
  forall a b : nat, a <> b -> a - b <> b - a.
Proof.
  induction a; intros b C.
  - now rewrite Nat.sub_0_r.
  - destruct b.
    + trivial.
    + repeat rewrite Nat.sub_succ. auto.
Qed.

Или, альтернативно, используя тактику omega, мы получаем однострочное доказательство:

Require Import Omega.

Lemma subtraction_does_not_commute :
  forall a b : nat, a <> b -> a - b <> b - a.
Proof. intros; omega. Qed.
person Anton Trunov    schedule 18.05.2017
comment
С omega вам больше не нужен induction. - person eponier; 18.05.2017
comment
Конечно, спасибо! Забыл, что в данном случае мы находимся в области арифметики Пресбургера. - person Anton Trunov; 18.05.2017
comment
Спасибо большое, прекрасно работает. Полный вопрос о новичках, как мне найти список определений и теорем, которые доступны как Nat.sub_succ и Nat.sub_0_r? - person Mike Harris; 18.05.2017
comment
@MikeHarris Require Import Coq.Arith.Arith., затем Search (S _ - S _). или Search (_ - 0). соответственно. Помимо подстановочного знака _, поиск Coq также понимает Search (?a + ?b = ?b + ?a). - он должен найти Nat.add_comm. Дополнительную информацию см. здесь. - person Anton Trunov; 18.05.2017