Stream: Coq users

Topic: Proof by induction with n > k


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mathieu Dehouck (Feb 14 2022 at 06:00):

Then I meant P 4, sorry.

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip Pierre Castéran (Feb 14 2022 at 06:26):

Did you do an induction over nor 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)
*)

view this post on Zulip 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.

view this post on Zulip 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