## Stream: Coq users

### Topic: Proof by induction with n > k

#### Mathieu Dehouck (Feb 14 2022 at 04:47):

Dear all,

I am having a little problem with understanding induction.
I would like to prove a property on a graph that only really makes sense when the graph has more than 3 nodes.
I see two ways :
`forall n g , n > 3 -> length g = n -> P g`
or
`forall n g, length g = n+3 -> P g`
Both look pretty similar to me, however, the first doesn't require me to prove the start of the induction, just that `0 > 3` is False.

So I wonder if I missed something here.
Do you spot any problem ?
Best

#### Li-yao (Feb 14 2022 at 04:57):

There's no problem here. The difference is that induction is being done on different numbers (relative to the graph), but both are valid approaches. In one, `n = length h`, in the other `n = length g - 3`.

#### Mathieu Dehouck (Feb 14 2022 at 05:03):

But in the first case it does not really ask for a proof that the induction is well founded since I just need to show that the graph is too small.
I could prove something like `forall n, n > 3 -> P n`, as soon as `P n -> P (S n)` even if `P 3` is not actually true since I am never asked to show it.

#### Li-yao (Feb 14 2022 at 05:41):

You would be proving `(n > 3 -> P n) -> (S n > 3 -> P n)`, which for `n <= 3` makes the induction hypothesis `n > 3 -> P n` vacuous (true but useless).

#### Mathieu Dehouck (Feb 14 2022 at 05:46):

Yes, but that's exactly my problem.
I prove `(n > 3 -> P n) -> (S n > 3 -> P n)`, but I never actually prove `P 3`.
So for what we know, it could well be false.

#### Li-yao (Feb 14 2022 at 05:58):

How is that a problem? Your initial statement `forall n g , n > 3 -> length g = n -> P n` rules out `n = 3` already.

#### Mathieu Dehouck (Feb 14 2022 at 06:00):

Then I meant `P 4`, sorry.

#### Li-yao (Feb 14 2022 at 06:02):

Ah right, and it's actually `(n > 3 -> P n) -> (S n > 3 -> P (S n))`. When `n = 3`, the two assumptions are true (`(3 > 3 -> P 3)` and `(4 > 3)`) so you're exactly proving `P 4`.

#### Mathieu Dehouck (Feb 14 2022 at 06:05):

Ok, it gets a bit clearer, but still, it seems that I can get by only proving `~ 0>3` and then the induction hypothesis.
Is it really enough ?

#### Pierre Castéran (Feb 14 2022 at 06:26):

Did you do an induction over `n`or over the proposition `n > 3` (which applies `le_ind`) ? In the second case, the sub-goals appear clearly.

``````Goal forall n, n > 3 -> P n.
induction 1.
(*
=======
P 4

m : nat
H : 4 <= m
IHle : P m
============================
P (S m)
*)
``````

#### Li-yao (Feb 14 2022 at 06:46):

Mathieu Dehouck said:

Ok, it gets a bit clearer, but still, it seems that I can get by only proving `~ 0>3` and then the induction hypothesis.
Is it really enough ?

It is indeed enough. The "real" base case `P 4` is part of the induction step.

The notion of base case is kinda arbitrary. A general formulation of induction over a well-founded relation `<` yields only one case, a very general "induction step". `forall n, P n` iff `forall n, (forall m, m < n -> P m) -> P n`.

The standard induction principle for `nat` can be viewed as that more general principle (with `x < y` as the successor relation `S x = y`) followed by a case analysis, comparing `n` to `0`. But it's not always necessary to case split at `0`.

#### Mathieu Dehouck (Feb 14 2022 at 07:33):

I see.
And Yes, I did induction over n, not over <.
I'try that.

Last updated: Feb 08 2023 at 23:03 UTC