CODEWITHSUNDEEP
coq
Sam Li
Sam Li

Reputation: 33

Addition of natural numbers in Coq

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.

Upvotes: 3

Views: 681

Answers (2)

M Soegtrop
M Soegtrop

Reputation: 1456

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.

Upvotes: 3

kyo dralliam
kyo dralliam

Reputation: 1217

Yes both additions are equivalent, you can prove it using the lemma plus_n_Sm : forall n m : nat, S (n + m) = n + S m from the standard library (found using Search "+" (S _).) and an adequate induction hypothesis (for instance P(n) := forall m, n + m = add n m).

Upvotes: 0

Related Questions