Proof by induction with n > k · Coq users

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.

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

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

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

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.

Stream: Coq users

Topic: Proof by induction with n > k

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