So I am playing with Coq, working through the Software Foundations text and I am trying to do a proof outside of what’s in the text for practice.

Here’s my Gallina code:

Fixpoint add (n m: nat) : nat :=
match n with
| O => m
| S n' => S (add n' m)
end.
Theorem sum_should_be_equal_or_greater: forall n m : nat, add n m >= n.
Proof.
intros n m.
induction n as [| n' IHn'].
- simpl.

I get this far in proving it:

1 subgoal
m : nat
______________________________________(1/1)
m >= 0

I would say that since m is a natural, by the definition of a natural number it’s greater than or equal to 0 but I’m not sure which tactic I should use to prove that. And, of course, I’ll have to prove P(S n’) as well but that’s a different question.

Or is induction not even the right approach to use?

For the 0 in the induction, you need the following lemma:

forall n, 0 <= n

This can be proved by induction on n.

In the S n' case, you need the following lemma:

forall n m, n <= m -> S n <= S m

This can be proved by induction on n <= m. You should check the definition of le and its inductive lemma:

Print le.
(*
Inductive le (n : nat) : nat -> Prop :=
| le_n : n <= n
| le_S : forall m : nat, n <= m -> n <= S m
*)
Check le_ind.
(*
: forall (n : nat) (P : nat -> Prop),
P n ->
(forall m : nat, n <= m -> P m -> P (S m)) ->
forall m : nat, n <= m -> P m
*)

PS: Note that in Coq, m >= n is simply defined as n <= m. It is more ‘natural’ in Coq to use the latter.

To be sure — the lemmas @mwuttke97 mentions exist in the stdlib (I think). Proving them yourself might be good practice, but since you’re creating these exercises on your own, I guess that decision is up to you @Onorio.
But I don’t want to spoil your practice either, so if you want to use them and don’t know how to find them, ask again

Thanks for the suggestions! I’ll pursue this approach and see where I can get.

But I am still wondering–since the set of natural numbers is defined as whole numbers 0 and above (or 1 and above, I guess), isn’t there some way to accept forall n: nat, 0 <= n by the fact of the definition of the set?

That is not true; your intuition about ‘sets’ doesn’t apply to Coq. In Coq, natural numbers are represented by objects of the type nat. This type is defined inductively with two constructors:

Inductive nat :=
| O : nat
| S : nat -> nat

O represents the number 0, S 0 represents 1, S (S 0) is 2, etc. That means, S x is the successor of x. This representation of natural numbers is called ‘Piano numbers’.

Now, check again the definition of le. It is an inductive predicate on natural numbers:

Inductive le (n : nat) : nat -> Prop :=
| le_n : le n n
| le_S : forall m : nat, le n m -> le n (S m)

There are two constructors:

le_n n is a proof that n <= n, for every number n : nat,

With le_S, it follows that if n <= m, then n <= S m.

Maybe you should think a bit why these two rules are enough to characterise <=. For example, you can prove that 2 <= 4 by applying le_S twice, and then le_n.

Using this inductively defined predicate, you can prove properties about le, like the two properties that I mentioned before. For example, how can you prove that 0 <= m for every m?

For this, you can do induction on m:

In the first case, you have to show 0 <= 0. That holds with the rule le_n.

In the second case, you can assume that 0 <= m and have to show 0 <= S m. For this, you only need to apply le_S.

I agree with the point, but I’d phrase it a bit differently; the intuition is not wrong, except that those intuitive properties are actual theorems and not formal definitions.

Actually, such tactics exist for numbers, and the text will introduce them later; doing these proofs by hand is still a useful exercise. Once you switch to proofs over other data structures, such as lists or trees, those special tactics for numbers won’t work, but you’ll be able to prove many properties by similar inductions.