Library Coq.Arith.Plus


Properties of addition. add is defined in Init/Peano.v as: 
Fixpoint plus (n m:nat) : nat :=
  match n with
  | O => m
  | S p => S (p + m)
  end
where "n + m" := (plus n m) : nat_scope.

Require Import Le.
Require Import Lt.

Local Open Scope nat_scope.

Implicit Types m n p q : nat.

Zero is neutral

Deprecated : Already in Init/Peano.v
Notation plus_0_l := plus_O_n (only parsing).
Definition plus_0_r n := eq_sym (plus_n_O n).

Commutativity


Lemma plus_comm : forall n m, n + m = m + n.
Hint Immediate plus_comm: arith v62.

Associativity


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

Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p.
Hint Resolve plus_assoc: arith v62.

Lemma plus_permute : forall n m p, n + (m + p) = m + (n + p).

Lemma plus_assoc_reverse : forall n m p, n + m + p = n + (m + p).
Hint Resolve plus_assoc_reverse: arith v62.

Simplification


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

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

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

Compatibility with order


Lemma plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m.
Hint Resolve plus_le_compat_l: arith v62.

Lemma plus_le_compat_r : forall n m p, n <= m -> n + p <= m + p.
Hint Resolve plus_le_compat_r: arith v62.

Lemma le_plus_l : forall n m, n <= n + m.
Hint Resolve le_plus_l: arith v62.

Lemma le_plus_r : forall n m, m <= n + m.
Hint Resolve le_plus_r: arith v62.

Theorem le_plus_trans : forall n m p, n <= m -> n <= m + p.
Hint Resolve le_plus_trans: arith v62.

Theorem lt_plus_trans : forall n m p, n < m -> n < m + p.
Hint Immediate lt_plus_trans: arith v62.

Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m.
Hint Resolve plus_lt_compat_l: arith v62.

Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p.
Hint Resolve plus_lt_compat_r: arith v62.

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

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

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

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

Inversion lemmas


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

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

Derived properties


Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q).

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 : forall n m, n <> S (plus m n).

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

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

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