Как упростить A + 0> 0 в A> 0?

Question

Я просто новичок в Coq, и я пытался доказать несколько элементарных теорем о натуральных числах. Я уже делал несколько, не очень изящно, но заканчивал меньше, чем меньше. Тем не менее, я полностью застрял на завершение этой теоремы:

Theorem add_increase: (forall a b: nat, a > 0 -> a + b > b). 
Proof. 
    intros A. 
    intros B. 
    intros H. 
    case B. 

Ввод это, я получаю этот выход:

2 subgoals 
A, B : nat 
H : A > 0 
______________________________________(1/2) 
A + 0 > 0 
______________________________________(2/2) 
forall n : nat, A + S n > S n 

Очевидно, что первая цель является довольно тривиальной упростить гипотезы H. Однако я просто не могу понять, как сделать это простое упрощение.

Answer 1

Один из способов упростить это использовать довольно скучную лемму

Lemma add_zero_r : forall n, n + 0 = n. 
Proof. 
    intros n. induction n. reflexivity. 
    simpl. rewrite IHn. reflexivity. 
Qed. 

и в следующих использовать это, чтобы переписать цель:

Theorem add_increase: (forall a b: nat, a > 0 -> a + b > b). 
Proof. 
    intros A. 
    intros B. 
    intros H. 
    case B. 
    rewrite (add_zero_r A). 
    assumption. 

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

Во-первых, я импортировал библиотеку Omega.

Require Import Omega. 

Докажите еще один скучный факт.

Lemma add_succ_r : forall n m, n + (S m) = S (n + m). 
Proof. 
    intros n m. induction n. reflexivity. 
    simpl. rewrite IHn. reflexivity. 
Qed. 

и вернуться к add_increase prove мы имеем следующую цель:

A, B : nat 
H : A > 0 
============================ 
forall n : nat, A + S n > S n 

Это может быть решена путем:

intros C. 
rewrite (add_succ_r A C). 
omega. 

Снова, я использовал предыдущий доказал лемму переписать цель. Тактика omega очень полезна, так как это полная процедура принятия решения так называемого quantifier free Presburger arithmetic, и на основе вашего контекста он может решить цель automagically.

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

Require Import Omega. 

Lemma add_zero_r : forall n, n + 0 = n. 
Proof. 
    intros n. induction n. reflexivity. 
    simpl. rewrite IHn. reflexivity. 
Qed. 

Lemma add_succ_r : forall n m, n + (S m) = S (n + m). 
Proof. 
    intros n m. induction n. reflexivity. 
    simpl. rewrite IHn. reflexivity. 
Qed. 

Theorem add_increase: (forall a b: nat, a > 0 -> a + b > b). 
Proof. 
    intros A. 
    intros B. 
    intros H. 
    case B. 
    rewrite (add_zero_r A). 
    assumption. 
    intros C. 
    rewrite (add_succ_r A C). 
    omega. 
Qed. 

Answer 2

Другое решение, используя различные натуральные числа библиотеки ssrnat и ssreflect стойкую язык (который необходим в библиотеке):

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. 

Theorem add_increase a b : 0 < a -> b < a + b. 
Proof. by rewrite -{1}[b]add0n ltn_add2r. Qed. 

ltn_add2r : (m + p < n + p) = (m < n) Лемма доказана индукцией по p, непосредственно по индукции по p плюс коммутативность и другие легкие свойства добавления.

Answer 3

Несколько стандартных лемм, таких как a + 0 = 0 и т. Д., Помещаются в базу данных подсказок arith.С ними auto обычно можно решить многие простые задачи такого рода, поэтому используйте auto with arith.

Require Import Arith. 
Theorem add_increase: (forall a b: nat, a > 0 -> a + b > b). 
    destruct a; intros b H. 
    - inversion H. (* base case, H: 0 > 0 *) 
    - simpl. auto with arith. 
Qed. 

Чтобы узнать, какие леммы auto используется, вы можете Print add_increase. В этом случае auto используются три леммы, и они в качестве альтернативы могут быть даны в явном виде to auto by auto using gt_le_S, le_lt_n_Sm, le_plus_r.

В общем, если вам нужна лемма, которую, по вашему мнению, уже доказали, вы можете найти ее с помощью SearchAbout. Используйте _ в качестве дикой карты или ?a в качестве именованной дикой карты. В вашем случае выше вы хотели что-то о добавлении нуля на правой, так

SearchAbout (_ + 0 = _). 

возвращается

plus_0_r: forall n : nat, n + 0 = n 
NPeano.Nat.add_0_r: forall n : nat, n + 0 = n 

Вы можете даже найти лемму в библиотеке, которая близка к тому, что вы хотите доказать.

SearchAbout (_ > _ -> _ + _ > _). 

находит

plus_gt_compat_l: forall n m p : nat, n > m -> p + n > p + m 

который довольно близко к add_increase.

Theorem add_increase: (forall a b: nat, a > 0 -> a + b > b). 
    intros. 
    pose (plus_gt_compat_l a 0 b H) as A. 
    repeat rewrite (plus_comm b) in A. 
    apply A. 
Qed.