| Properties of addition |
Require Import Le.
Require Import Lt.
Open Local Scope nat_scope.
Implicit Types m n p q : nat.
| Zero is neutral |
Lemma plus_0_l : forall n, 0 + n = n.
Proof.
reflexivity.
Qed.
Lemma plus_0_r : forall n, n + 0 = n.
Proof.
intro; symmetry in |- *; apply plus_n_O.
Qed.
| Commutativity |
Lemma plus_comm : forall n m, n + m = m + n.
Proof.
intros n m; elim n; simpl in |- *; auto with arith.
intros y H; elim (plus_n_Sm m y); auto with arith.
Qed.
Hint Immediate plus_comm: arith v62.
| Associativity |
Lemma plus_Snm_nSm : forall n m, S n + m = n + S m.
intros.
simpl in |- *.
rewrite (plus_comm n m).
rewrite (plus_comm n (S m)).
trivial with arith.
Qed.
Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p.
Proof.
intros n m p; elim n; simpl in |- *; auto with arith.
Qed.
Hint Resolve plus_assoc: arith v62.
Lemma plus_permute : forall n m p, n + (m + p) = m + (n + p).
Proof.
intros; rewrite (plus_assoc m n p); rewrite (plus_comm m n); auto with arith.
Qed.
Lemma plus_assoc_reverse : forall n m p, n + m + p = n + (m + p).
Proof.
auto with arith.
Qed.
Hint Resolve plus_assoc_reverse: arith v62.
| Simplification |
Lemma plus_reg_l : forall n m p, p + n = p + m -> n = m.
Proof.
intros m p n; induction n; simpl in |- *; auto with arith.
Qed.
Lemma plus_le_reg_l : forall n m p, p + n <= p + m -> n <= m.
Proof.
induction p; simpl in |- *; auto with arith.
Qed.
Lemma plus_lt_reg_l : forall n m p, p + n < p + m -> n < m.
Proof.
induction p; simpl in |- *; auto with arith.
Qed.
| Compatibility with order |
Lemma plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m.
Proof.
induction p; simpl in |- *; auto with arith.
Qed.
Hint Resolve plus_le_compat_l: arith v62.
Lemma plus_le_compat_r : forall n m p, n <= m -> n + p <= m + p.
Proof.
induction 1; simpl in |- *; auto with arith.
Qed.
Hint Resolve plus_le_compat_r: arith v62.
Lemma le_plus_l : forall n m, n <= n + m.
Proof.
induction n; simpl in |- *; auto with arith.
Qed.
Hint Resolve le_plus_l: arith v62.
Lemma le_plus_r : forall n m, m <= n + m.
Proof.
intros n m; elim n; simpl in |- *; auto with arith.
Qed.
Hint Resolve le_plus_r: arith v62.
Theorem le_plus_trans : forall n m p, n <= m -> n <= m + p.
Proof.
intros; apply le_trans with (m:= m); auto with arith.
Qed.
Hint Resolve le_plus_trans: arith v62.
Theorem lt_plus_trans : forall n m p, n < m -> n < m + p.
Proof.
intros; apply lt_le_trans with (m:= m); auto with arith.
Qed.
Hint Immediate lt_plus_trans: arith v62.
Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m.
Proof.
induction p; simpl in |- *; auto with arith.
Qed.
Hint Resolve plus_lt_compat_l: arith v62.
Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p.
Proof.
intros n m p H; rewrite (plus_comm n p); rewrite (plus_comm m p).
elim p; auto with arith.
Qed.
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.
Proof.
intros n m p q H H0.
elim H; simpl in |- *; auto with arith.
Qed.
Lemma plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q.
Proof.
unfold lt in |- *. intros. change (S n + p <= m + q) in |- *. rewrite plus_Snm_nSm.
apply plus_le_compat; assumption.
Qed.
Lemma plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q.
Proof.
unfold lt in |- *. intros. change (S n + p <= m + q) in |- *. apply plus_le_compat; assumption.
Qed.
Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
Proof.
intros. apply plus_lt_le_compat. assumption.
apply lt_le_weak. assumption.
Qed.
| Inversion lemmas |
Lemma plus_is_O : forall n m, n + m = 0 -> n = 0 /\ m = 0.
Proof.
intro m; destruct m as [| n]; auto.
intros. discriminate H.
Qed.
Definition plus_is_one :
forall m n, m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}.
Proof.
intro m; destruct m as [| n]; auto.
destruct n; auto.
intros.
simpl in H. discriminate H.
Defined.
| Derived properties |
Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q).
Proof.
intros m n p q.
rewrite <- (plus_assoc m n (p + q)). rewrite (plus_assoc n p q).
rewrite (plus_comm n p). rewrite <- (plus_assoc p n q). apply plus_assoc.
Qed.
| 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 plus_acc q n {struct n} : nat :=
match n with
| O => q
| S p => plus_acc (S q) p
end.
Definition tail_plus n m := plus_acc m n.
Lemma plus_tail_plus : forall n m, n + m = tail_plus n m.
unfold tail_plus in |- *; induction n as [| n IHn]; simpl in |- *; auto.
intro m; rewrite <- IHn; simpl in |- *; auto.
Qed.