Library Coq.Arith.Plus

Properties of addition.

This file is mostly OBSOLETE now, see module PeanoNat.Nat instead.

Nat.add is defined in Init/Nat.v as:

Fixpoint add (n m:nat) : nat :=
  match n with
  | O => m
  | S p => S (p + m)
  end
where "n + m" := (add n m) : nat_scope.

Require Import PeanoNat.

Local Open Scope nat_scope.

Neutrality of 0, commutativity, associativity

Notation plus_0_l := Nat.add_0_l (only parsing).
Notation plus_0_r := Nat.add_0_r (only parsing).
Notation plus_comm := Nat.add_comm (only parsing).
Notation plus_assoc := Nat.add_assoc (only parsing).

Notation plus_permute := Nat.add_shuffle3 (only parsing).

Definition plus_Snm_nSm : forall n m, S n + m = n + S m :=
Peano.plus_n_Sm.

Lemma plus_assoc_reverse n m p : n + m + p = n + (m + p ).

Simplification

Lemma plus_reg_l n m p : p + n = p + m -> n = m.

Lemma plus_le_reg_l n m p : p + n <= p + m -> n <= m.

Lemma plus_lt_reg_l n m p : p + n < p + m -> n < m.

Compatibility with order

Lemma plus_le_compat_l n m p : n <= m -> p + n <= p + m.

Lemma plus_le_compat_r n m p : n <= m -> n + p <= m + p.

Lemma plus_lt_compat_l n m p : n < m -> p + n < p + m.

Lemma plus_lt_compat_r n m p : n < m -> n + p < m + p.

Lemma plus_le_compat n m p q : n <= m -> p <= q -> n + p <= m + q.

Lemma plus_le_lt_compat n m p q : n <= m -> p < q -> n + p < m + q.

Lemma plus_lt_le_compat n m p q : n < m -> p <= q -> n + p < m + q.

Lemma plus_lt_compat n m p q : n < m -> p < q -> n + p < m + q.

Lemma le_plus_l n m : n <= n + m.

Lemma le_plus_r n m : m <= n + m.

Theorem le_plus_trans n m p : n <= m -> n <= m + p.

Theorem lt_plus_trans n m p : n < m -> n < m + p.

Inversion lemmas

Lemma plus_is_O n m : n + m = 0 -> n = 0 /\ m = 0.

Definition plus_is_one m n :
m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}.

Derived properties

Notation plus_permute_2_in_4 := Nat.add_shuffle1 (only parsing).

Tail-recursive plus

tail_plus is an alternative definition for plus which is tail-recursive, whereas plus is not. This can be useful when extracting programs.

Fixpoint tail_plus n m : nat :=
  match n with
    | O => m
    | S n => tail_plus n (S m)
  end.

Lemma plus_tail_plus : forall n m, n + m = tail_plus n m.

Discrimination

Lemma succ_plus_discr n m : n <> S (m +n).

Lemma n_SSn n : n <> S (S n).

Lemma n_SSSn n : n <> S (S (S n)).

Lemma n_SSSSn n : n <> S (S (S (S n))).

Compatibility Hints

#[global]
Hint Immediate plus_comm : arith.
#[global]
Hint Resolve plus_assoc plus_assoc_reverse : arith.
#[global]
Hint Resolve plus_le_compat_l plus_le_compat_r : arith.
#[global]
Hint Resolve le_plus_l le_plus_r le_plus_trans : arith.
#[global]
Hint Immediate lt_plus_trans : arith.
#[global]
Hint Resolve plus_lt_compat_l plus_lt_compat_r : arith.

For compatibility, we "Require" the same files as before

Require Import Le Lt.