Докажите, что n ‹m + n или что 0‹ m в COQ

Я пытаюсь использовать лемму для большего доказательства, но не могу найти способ доказать одну из этих двух вещей. Кто-нибудь может мне помочь? Вот доказательство:

Lemma less_r : (forall m n p : nat, n + m < p + n + m).

Proof.
 intros.
 apply PeanoNat.Nat.add_lt_mono_r.
 apply PeanoNat.Nat.lt_add_pos_l.
 admit.
Qed.

inequality coq proof
person Rafael Santos    schedule 30.06.2018    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Ваше утверждение не может быть доказано, потому что оно неверно. Например, если мы возьмем n = m = p = 0, это влечет 0 < 0, явное противоречие.

person Arthur Azevedo De Amorim    schedule 30.06.2018
comment
Но доказать это невозможно, кроме как где 0 ‹0? - person Rafael Santos; 30.06.2018
comment
@RafaelSantos Я не понимаю, о чем вы. Вам необходимо изменить свое утверждение, если вы хотите его доказать. Одна из возможностей - добавить предварительное условие о p: forall n m p, 0 < p -> n + m < p + n + m, которое вы можете легко доказать с помощью тактики omega (после добавления Require Import Omega. в ваш файл). Но я не знаю, подходит ли вам эта лемма. - person Arthur Azevedo De Amorim; 30.06.2018
comment
Итак, чтобы мы поняли, что вы хотите сделать, вы хотите получить coq, чтобы опровергнуть ваше утверждение? - person Lasse V. Karlsen; 30.06.2018