diff options
Diffstat (limited to 'theories/Arith/Plus.v')
| -rwxr-xr-x | theories/Arith/Plus.v | 202 |
1 files changed, 202 insertions, 0 deletions
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v new file mode 100755 index 00000000..e4ac631e --- /dev/null +++ b/theories/Arith/Plus.v @@ -0,0 +1,202 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Plus.v,v 1.18.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +(** 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.
\ No newline at end of file |