Coq - Как доказать eqb_neq?

Пытаюсь доказать eqb_neq:

Theorem eqb_neq : forall x y : nat,
  x =? y = false <-> x <> y.

Это мой текущий статус подтверждения: введите описание изображения здесь

Во время доказательства я дошел до последнего шага, на котором мне просто нужно доказать дополнительную вспомогательную теорему:

Theorem eqb_false_helper : forall n m : nat,
    n <> m -> S n <> S m.

Я пробовал несколько стратегий, но теперь даже не уверен, что можно доказать эту вспомогательную теорему.

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

Что еще можно попробовать? Какие-нибудь советы по eqb_neq или теореме о помощнике?

Спасибо


coq coqide proof
person jonb    schedule 27.05.2020    source источник
comment
Убедительно прошу вас воздержаться от размещения (частичных) решений упражнений по научной фантастике на публичных форумах. Если вы можете повторно опубликовать свой вопрос, чтобы удалить доказательство, мы будем рады вам помочь.   -  person Arthur Azevedo De Amorim    schedule 27.05.2020

Ответы (1)


arrow_upward
1
arrow_downward

На самом деле это довольно просто для вашей вспомогательной теоремы, если вы просто не развернете:

Theorem eqb_false_helper : forall n m : nat,
    n <> m -> S n <> S m.
Proof.
unfold not; intros.
apply H; injection H0; intro; assumption.
Qed.

На самом деле вам просто нужно доказать, что S n = S m -> False, вы предполагаете, что n = m -> False, таким образом, вы можете доказать, что S n = S m -> n = m, что является введением гипотезы S n = S m.

person Lucien David    schedule 27.05.2020