How to do simultaneous induction in Coq?

Question

I have proofs for

1. P(0, 0)
2. P(0,n)->P(0, Sn)
3. P(m,0)->P(S m, 0)
4. P(m,n)->P(S m, S n).

How do I prove A for all values in Coq?

I tried two normal inductions, but it required P(m, S n)->P(S m, S n), which is not necessarily true.

Thank you.

Answer 1

Doing two nested inductions works, like this:

Lemma simultaneous_induction
  (P : nat -> nat -> Prop)
  (H_base : P 0 0)
  (H_ind_vertical : forall n, P 0 n -> P 0 (S n))
  (H_ind_horizontal : forall m, P m 0 -> P (S m) 0)
  (H_ind_diagonal : forall m n, P m n -> P (S m) (S n)) :
  forall m n, P m n.
Proof.
  induction m as [|m IH].
  - induction n as [|n IH'].
    + apply H_base.
    + apply H_ind_vertical. apply IH'.
  - induction n as [|n IH'].
    + apply H_ind_horizontal. apply IH.
    + apply H_ind_diagonal. apply IH.
Qed.

If Coq asked you to prove P m (S n) -> P (S m) (S n), it probably means that you did intros m n. induction m. instead of intros m. induction m. (or just induction m. which does the intros directly). If you introduce n before doing the induction on m, it means you are fixing a certain $n$ and proving by induction on $m$ that for all $m$ we have $P(m, n)$. But this does not work, because we need to invoke H_ind_diagonal with a different value of $n$. Instead, you should prove by induction on $m$ that for all $m$ we have: for all $n$, $P(m, n)$ holds. The quantifier on $n$ should be inside what you're proving by induction.