[eperdew]

The example I'm about to give is overkill, but I'm trying to make my point very carefully.

Suppose you want to prove something for integers >= 2. E.g., suppose you want to prove for all n >= 2, n is positive. The statement you're trying to prove for a given n is actually

P(n) := n >= 2 -> n is positive

Let's prove it by induction.

P(0) is 0 >= 2 -> 0 is positive. P(0) is vacuously true, because 0 < 2.

Suppose P(n). We want to show P(n + 1). Our goal is

n + 1 >= 2 -> n + 1 is positive. Let's break this into the cases n >= 2 and n < 2.

For n >= 2, we assume P(n) and have the LHS of the implies. This gives us n is positive. Say by definition or by a lemma that n positive -> n + 1 is positive, and we handle this branch.

For n < 2, the inductive hypothesis tells us nothing. Assume the LHS of our goal, i.e. n + 1 >= 2. We want to prove n + 1 is positive. Well 2 is positive and therefore n + 1 is positive by transitivity.

This is what I mean by the base case not being special. E.g., in Coq, induction over the natural numbers always starts at 0. When you think about doing induction starting at another number, you're transforming your goal to include something of the form n >= m -> P(n).

[ashtonbaker]

> E.g., in Coq, induction over the natural numbers always starts at 0. When you think about doing induction starting at another number, you're transforming your goal to include something of the form n >= m -> P(n).

The concept of a “minimal base case” really weirded me out but I couldn’t quite put my finger on why. Thanks for the painstaking explanation, this was perspective-broadening.

[tsimionescu]

But does this do anything meaningful, or is it just pointless drudgery because Coq is a machine and can't 'understand'/assume even simple maths/logic if it isn't explicitly stated? This is not a slight on Coq by any means, just pointing out the difference between human proofs and machine proofs. (Humans can of course be tricked into thinking that subtly false statements are trivially true, which the much more meticulous machine proof would discover)

That is, what is being gained by looking at the vacuously true cases where n<2, when the only interesting base case is the one where the LHS of the implication is true?

[eperdew]

I wrote out quite a bit for this, but I think that the main point is that by falling back to the formalism, we see the the LHS of the implication affects our inductive hypothesis. I think this is something that is not clear if you just do "base case starting at n" style proofs."

As far as drudgery, Coq will solve the trivial cases automatically, so you'd never have to prove the n = 0 case by hand. That said, there's a reason most math is done on paper and not in Coq - there's usually an order of magnitude more detail and drudgery in a formal proof, even with automation.