Using induction starting from 1 in Coq

Question

I am trying to use induction starting from 1 in a Coq proof. From this question I got a proof of the induction principle I need:

Require Import Coq.micromega.Lia.

Section induction_at_1.
  Variable P : nat -> Prop.
  Hypothesis p1 : P 1.
  Hypothesis pS : forall n, P n -> P (S n).

  Theorem induction_at_1:
    forall n, n > 0 -> P n.
P: nat -> Prop
p1: P 1
pS: forall n : nat, P n -> P (S n)
forall n : nat, n > 0 -> P n
  Proof using p1 pS.
P: nat -> Prop
p1: P 1
pS: forall n : nat, P n -> P (S n)
forall n : nat, n > 0 -> P n
    induction n; intro.
P: nat -> Prop
p1: P 1
pS: forall n : nat, P n -> P (S n)
H: 0 > 0
P 0
P: nat -> Prop
p1: P 1
pS: forall n : nat, P n -> P (S n)
n: nat
IHn: n > 0 -> P n
H: S n > 0
P (S n)
    -
P: nat -> Prop
p1: P 1
pS: forall n : nat, P n -> P (S n)
H: 0 > 0
P 0 exfalso.
P: nat -> Prop
p1: P 1
pS: forall n : nat, P n -> P (S n)
H: 0 > 0
False lia.
    -
P: nat -> Prop
p1: P 1
pS: forall n : nat, P n -> P (S n)
n: nat
IHn: n > 0 -> P n
H: S n > 0
P (S n) destruct n.
P: nat -> Prop
p1: P 1
pS: forall n : nat, P n -> P (S n)
IHn: 0 > 0 -> P 0
H: 1 > 0
P 1
P: nat -> Prop
p1: P 1
pS: forall n : nat, P n -> P (S n)
n: nat
IHn: S n > 0 -> P (S n)
H: S (S n) > 0
P (S (S n))
      +
P: nat -> Prop
p1: P 1
pS: forall n : nat, P n -> P (S n)
IHn: 0 > 0 -> P 0
H: 1 > 0
P 1 apply p1.
      +
P: nat -> Prop
p1: P 1
pS: forall n : nat, P n -> P (S n)
n: nat
IHn: S n > 0 -> P (S n)
H: S (S n) > 0
P (S (S n)) assert (S n > 0) by lia.
P: nat -> Prop
p1: P 1
pS: forall n : nat, P n -> P (S n)
n: nat
IHn: S n > 0 -> P (S n)
H: S (S n) > 0
H0: S n > 0
P (S (S n)) intuition.
  Qed.
End induction_at_1.

What I get looks structurally very similar to standard induction. In fact, Check nat_ind yields

nat_ind
     : forall P : nat -> Prop,
       P 0 ->
       (forall n : nat, P n -> P (S n)) ->
       forall n : nat, P n

while Check induction_at_1 yields

induction_at_1
     : forall P : nat -> Prop,
       P 1 ->
       (forall n : nat, P n -> P (S n)) ->
       forall n : nat, n > 0 -> P n

The issue arises when I try to apply this induction principle. For instance, I would like to prove by induction

Lemma cancellation:
  forall a b c : nat, a > 0 -> a * b = a * c -> b = c.
forall a b c : nat, a > 0 -> a * b = a * c -> b = c

This seems exactly suited to the kind of induction I have above, but when I start my proof like this

  intros a b c H0 H1.
a, b, c: nat
H0: a > 0
H1: a * b = a * c
b = c
  induction a using induction_at_1.
Not the right number of induction arguments (expected 2 arguments).

I get the above error, which I cannot interpret. Since the two induction principles look almost identical to me, I am not sure why this does not work. Any ideas?

Answer

I also find this behavior puzzling, but there are a few ways around it. One is to use the ssreflect induction tactic, called elim:

From Coq Require Import ssreflect.

Lemma cancellation:
  forall a b c : nat, a > 0 -> a * b = a * c -> b = c.
forall a b c : nat, a > 0 -> a * b = a * c -> b = c
Proof.
forall a b c : nat, a > 0 -> a * b = a * c -> b = c
  intros a b c H.
a, b, c: nat
H: a > 0
a * b = a * c -> b = c
  elim/induction_at_1: a / H.
b, c: nat
1 * b = 1 * c -> b = c
b, c: nat
forall n : nat,
(n * b = n * c -> b = c) -> S n * b = S n * c -> b = c
  (* ... *)
Abort.

The second line is telling Coq to perform induction on H (not a) while generalizing a and using the induction principle induction_at_1. I couldn't get something similar to work using the regular Coq induction.

An alternative is to use plain natural number induction. In this case, I believe that the lemma follows by induction on b while generalizing c (I am not sure that induction on a works). If you do need to show something of the form m <= n -> P n for all n, you can replace n by n - m + m (which should be possible with the m <= n hypothesis), and then prove P (n - m + m) by induction on n - m.