Addition of natural numbers in Coq

Question

Coq's standard libraries give the Peano natural numbers and addition:

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

Fixpoint add n m :=
  match n with
  | 0 => m
  | S p => S (add p m)
  end.

I am curious if I change the fix_definition of addition like

Fixpoint add n m :=
  match n with
  | 0 => m
  | S p => add p (S m)
  end.

Is the new addition equivalent to the old one? I tried to prove their equivalence by proving forall n m, add (S n) m = S (add n m) but failed.

Answer 1

In order to proof your helper lemma, you need to be careful what to introduce. If you don't introduce m, you get a more general induction hypothesis as in:

Require Import Nat.

Print add.

Fixpoint my_add n m :=
  match n with
  | 0 => m
  | S p => my_add p (S m)
  end.

Lemma my_add_S_r: forall n m, my_add n (S m) = S (my_add n m).
Proof.
  (* Note: don't introduce m here - you get a more general induction hypothesis this way *)
  intros n.
  induction n.
  - intros; reflexivity.
  - intros; cbn. rewrite IHn. reflexivity.
Qed.

Lemma my_add_equiv: forall n m, add n m = my_add n m.
intros.
induction n.
- reflexivity.
- cbn. rewrite my_add_S_r. rewrite IHn. reflexivity.
Qed.