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

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`

.

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.

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).

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.

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

rules out `n = 3`

already.

Then I meant `P 4`

, sorry.

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`

.

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 ?

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)
*)
```

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`

.

I see.

And Yes, I did induction over n, not over <.

I'try that.

Last updated: Sep 30 2023 at 05:01 UTC