Back to Coq proof checker after 5-8 years away: how to prove that (forall n, m : N, (n - (S m)) = pred(n - m))?

Question

Somewhere between 5 and 8 years ago (probably 6 or 7) I wrote a full Formalization of Bubble Sort in Coq. One of the earliest Lemmas proven was the one in the title, which I called "sub_succ_r" (or maybe it's the standard name?):

forall n m : nat, (n - (S m))%nat = pred(n - m)

Now, back then, this was the very simple proof for that Lemma:

intros n m.
induction n m using n_double_ind.
simpl.
auto.
apply sub_0_r.
Qed.

"sub_0_r" is the Lemma that asserts that

forall n : nat, (n - 0)%nat = n

Now, attentive readers who are also familiar with modern Coq might have already spotted the problem with the old proof: that second line.

induction n m

i.e. simultaneous induction on 2 terms, doesn't work any more, not even when specifying that one is using "n_double_ind". I've been wracking my head over how to prove this using first induction over n and then induction over m, but I just can't figure it out.

Any help, great or small, would be much appreciated.

Kamyar Mirzavaziri Kamyar Mirzavaziri · Accepted Answer · 2020-03-22T02:53:54

If you want to apply induction on two variables simultaneously, you need to use comma separator, or Coq recognizes f t as f applied to t, so when you write n m this actually means n is a function and you want to apply it to m. Instead, use comma like this:

induction n, m.

this generates four subgoals. Two of them can be proved using auto so you can ask Coq to use auto tactic on every subgoal generated by induction, using semicolon like this:

induction n, m; auto.

and the remaining subgoals are easy to prove using the lemma you mentioned and induction hypotheses. so the whole script is as follows:

Lemma sub_0_r : forall n : nat, (n - 0) = n.
Admitted.

Theorem sub_succ_r: forall n m : nat, (n - (S m)) = pred(n - m).
Proof.
  induction n, m; auto.
  - apply sub_0_r.
  - apply IHn.
Qed.

Also note that using %nat is not necessary.

But as you saw we only used IHn which means that we didn't use the induction hypothesis for m, so we do not need to use induction on m, only a destruct tactic would do the job, a better proof is:

induction n; destruct m; auto.
- apply sub_0_r.
- apply IHn.

which is minimal and elegant.

Back to Coq proof checker after 5-8 years away: how to prove that (forall n, m : N, (n - (S m)) = pred(n - m))?

1 Answers