How to simplify A + 0 > 0 into A > 0?

Question

I'm just a beginner with Coq, and I've been trying to prove a few elementary theorems about natural numbers. I've done a few already, not very elegantly, but completed nether the less. However I'm totally stuck on completing this theorem:

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

Entering this in, I get this output:

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

Obviously, the first goal is pretty trivial to simplify to hypothesis H. However, I just can't figure out how to make this straightforward simplification.

Answer 1

One way to simplify this is to use a rather boring lemma

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

and next use this to rewrite your goal:

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.

To finish the other proof case I've used a little lemma and a tactic that eases the task of proving stuff with inequalities over naturals.

First, I've imported Omega library.

Require Import Omega.

Prove another boring fact.

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.

and going back to add_increase prove we have the following goal:

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

That can be solved by:

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

Again, I've used the previous proved lemma to rewrite the goal. The omega tactic is a very useful one since it is a complete decision procedure for the so called quantifier free Presburger arithmetic, and based on your context, it can solve the goal automagically.

Here's the complete solution to your proof:

 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

Several common lemmas such as a + 0 = 0 etc. are put in the hint database arith. With them, auto can usually solve many simple goals of this kind, so use 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.

To see which lemmas auto used, you can Print add_increase. In this case, auto used three lemmas, and they can alternatively be given explicitly to auto by auto using gt_le_S, le_lt_n_Sm, le_plus_r.

In general, when you need a lemma that you think ought to have already been proven, you can search for it with SearchAbout. Use _ as a wild card, or ?a as a named wild-card. In your case above you wanted something about adding a zero on the right, so

SearchAbout ( _ + 0 =  _ ).

returns

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

You can even find a lemma in the library that is close to what you want to prove.

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

finds

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

which is pretty close to 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.

Answer 3

Another solution using a different natural numbers library ssrnat and the ssreflect proof language (which is needed by the library):

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.

The ltn_add2r : (m + p < n + p) = (m < n) lemma is proved by induction on p, directly by induction on p plus commutativity and other easy properties of addition.

Answer 4

Note that if we're invoking the omega tactic, we could've just done:

Theorem add_increase : forall a b: nat, a > 0 -> a + b > b.
Proof. intros a b. omega. Qed.