What is the difference of `induction n, m` and `induction n; induction m` in Coq?

user_652528 0
Viewed 85

I tough that induction n, m would create induction hypothesis for n and m but after some tries this seems not be the case. BTW I'm assuming forall (n m : nat).

So what is the difference of induction n, m induction n. induction m and induction n; induction m?

Here is my currently understanding:

I know that ; is a combinator so that a; b replays b on every subgoal generated by a, so induction n; induction m will generate an induction hypotesis for m for each subgoal of induction n is this right?

And in the same sense induction n. induction m would generate induction hypotesis only for the current goal so that this seems not particularly useful

I expected induction n, m to be like induct on this two variables this generate four goals for natural numbers as I expected, but I expected IHm to be on context on the 4th goal but it isn't! What I'm missing?

--

Still researching on this, it seems that the IHm is merged in IHn at the 4th goal, is this correct?

-- edit 2

Here is some example based on addition commutativity

So first the induction n, m version:

Example add_comm' : forall (n m : nat), n + m = m + n.
  intros. induction n, m; try auto using plus_n_O.

This solves the trivial 3 first goals and leave me with the 4th goal with

n, m : nat
IHn : n + S m = S m + n

========================= (1 / 1)

S n + S m = S m + S n

Now the induction n; induction m version:

n, m : nat
IHn : n + S m = S m + n
IHm : n + m = m + n -> S n + m = m + S n

========================= (1 / 1)

S (n + S m) = S (m + S n)

So for this particular case induction n, m is better but I can't explain (and understand) what it is doing.

In the manual the only case for , in induction is

Variant induction term+, using qualid

This syntax is used for the case qualid denotes an induction principle with complex predicates as the induction principles generated by Function or Functional Scheme may be.

But I'm not using using qualid so I'm not sure if this is the case

-- edit 3 --

As Andrey said in its comment, the using qualid variant is the one being triggered but I have no idea what is the explanation for what it does.

coq
1 Answers

induction n, m is the same as induction n; destruct m. The reason for this is that it's quite rare that you actually want two induction hypotheses, and in cases where you do, you probably don't want induction n; induction m because the induction hypothesis for m will not be appropriately general over n.

The reference manual for 8.15 will be much more complete than the reference manual for 8.14, and you can find this documented in the current documentation for the master branch:

If no induction_principle clause is provided, this is equivalent to doing induction on the first induction_clause followed by destruct on any subsequent clauses.

user_3770220
Related