diff options
Diffstat (limited to 'theories7/Arith/Plus.v')
| -rwxr-xr-x | theories7/Arith/Plus.v | 223 |
1 files changed, 223 insertions, 0 deletions
diff --git a/theories7/Arith/Plus.v b/theories7/Arith/Plus.v new file mode 100755 index 00000000..23488b4c --- /dev/null +++ b/theories7/Arith/Plus.v @@ -0,0 +1,223 @@ +(************************************************************************) +(* 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.5.2.1 2004/07/16 19:31:25 herbelin Exp $ i*) + +(** Properties of addition *) + +Require Le. +Require Lt. + +V7only [Import nat_scope.]. +Open Local Scope nat_scope. + +Implicit Variables Type m,n,p,q:nat. + +(** Zero is neutral *) + +Lemma plus_0_l : (n:nat) (O+n)=n. +Proof. +Reflexivity. +Qed. + +Lemma plus_0_r : (n:nat) (n+O)=n. +Proof. +Intro; Symmetry; Apply plus_n_O. +Qed. + +(** Commutativity *) + +Lemma plus_sym : (n,m:nat)(n+m)=(m+n). +Proof. +Intros n m ; Elim n ; Simpl ; Auto with arith. +Intros y H ; Elim (plus_n_Sm m y) ; Auto with arith. +Qed. +Hints Immediate plus_sym : arith v62. + +(** Associativity *) + +Lemma plus_Snm_nSm : (n,m:nat)((S n)+m)=(n+(S m)). +Intros. +Simpl. +Rewrite -> (plus_sym n m). +Rewrite -> (plus_sym n (S m)). +Trivial with arith. +Qed. + +Lemma plus_assoc_l : (n,m,p:nat)((n+(m+p))=((n+m)+p)). +Proof. +Intros n m p; Elim n; Simpl; Auto with arith. +Qed. +Hints Resolve plus_assoc_l : arith v62. + +Lemma plus_permute : (n,m,p:nat) ((n+(m+p))=(m+(n+p))). +Proof. +Intros; Rewrite (plus_assoc_l m n p); Rewrite (plus_sym m n); Auto with arith. +Qed. + +Lemma plus_assoc_r : (n,m,p:nat)(((n+m)+p)=(n+(m+p))). +Proof. +Auto with arith. +Qed. +Hints Resolve plus_assoc_r : arith v62. + +(** Simplification *) + +Lemma plus_reg_l : (m,p,n:nat)((n+m)=(n+p))->(m=p). +Proof. +Intros m p n; NewInduction n ; Simpl ; Auto with arith. +Qed. +V7only [ +(* Compatibility order of arguments *) +Notation "'simpl_plus_l' c" := [a,b:nat](plus_reg_l a b c) + (at level 10, c at next level). +Notation "'simpl_plus_l' c a" := [b:nat](plus_reg_l a b c) + (at level 10, a, c at next level). +Notation "'simpl_plus_l' c a b" := (plus_reg_l a b c) + (at level 10, a, b, c at next level). +Notation simpl_plus_l := plus_reg_l. +]. + +Lemma plus_le_reg_l : (n,m,p:nat)((p+n)<=(p+m))->(n<=m). +Proof. +NewInduction p; Simpl; Auto with arith. +Qed. +V7only [ +(* Compatibility order of arguments *) +Notation "'simpl_le_plus_l' c" := [a,b:nat](plus_le_reg_l a b c) + (at level 10, c at next level). +Notation "'simpl_le_plus_l' c a" := [b:nat](plus_le_reg_l a b c) + (at level 10, a, c at next level). +Notation "'simpl_le_plus_l' c a b" := (plus_le_reg_l a b c) + (at level 10, a, b, c at next level). +Notation simpl_le_plus_l := [p,n,m:nat](plus_le_reg_l n m p). +]. + +Lemma simpl_lt_plus_l : (n,m,p:nat) (p+n)<(p+m) -> n<m. +Proof. +NewInduction p; Simpl; Auto with arith. +Qed. + +(** Compatibility with order *) + +Lemma le_reg_l : (n,m,p:nat) n<=m -> (p+n)<=(p+m). +Proof. +NewInduction p; Simpl; Auto with arith. +Qed. +Hints Resolve le_reg_l : arith v62. + +Lemma le_reg_r : (a,b,c:nat) a<=b -> (a+c)<=(b+c). +Proof. +NewInduction 1 ; Simpl; Auto with arith. +Qed. +Hints Resolve le_reg_r : arith v62. + +Lemma le_plus_l : (n,m:nat) n<=(n+m). +Proof. +NewInduction n; Simpl; Auto with arith. +Qed. +Hints Resolve le_plus_l : arith v62. + +Lemma le_plus_r : (n,m:nat) m<=(n+m). +Proof. +Intros n m; Elim n; Simpl; Auto with arith. +Qed. +Hints Resolve le_plus_r : arith v62. + +Theorem le_plus_trans : (n,m,p:nat) n<=m -> n<=(m+p). +Proof. +Intros; Apply le_trans with m:=m; Auto with arith. +Qed. +Hints Resolve le_plus_trans : arith v62. + +Theorem lt_plus_trans : (n,m,p:nat) n<m -> n<(m+p). +Proof. +Intros; Apply lt_le_trans with m:=m; Auto with arith. +Qed. +Hints Immediate lt_plus_trans : arith v62. + +Lemma lt_reg_l : (n,m,p:nat) n<m -> (p+n)<(p+m). +Proof. +NewInduction p; Simpl; Auto with arith. +Qed. +Hints Resolve lt_reg_l : arith v62. + +Lemma lt_reg_r : (n,m,p:nat) n<m -> (n+p)<(m+p). +Proof. +Intros n m p H ; Rewrite (plus_sym n p) ; Rewrite (plus_sym m p). +Elim p; Auto with arith. +Qed. +Hints Resolve lt_reg_r : arith v62. + +Lemma le_plus_plus : (n,m,p,q:nat) n<=m -> p<=q -> (n+p)<=(m+q). +Proof. +Intros n m p q H H0. +Elim H; Simpl; Auto with arith. +Qed. + +Lemma le_lt_plus_plus : (n,m,p,q:nat) n<=m -> p<q -> (n+p)<(m+q). +Proof. + Unfold lt. Intros. Change ((S n)+p)<=(m+q). Rewrite plus_Snm_nSm. + Apply le_plus_plus; Assumption. +Qed. + +Lemma lt_le_plus_plus : (n,m,p,q:nat) n<m -> p<=q -> (n+p)<(m+q). +Proof. + Unfold lt. Intros. Change ((S n)+p)<=(m+q). Apply le_plus_plus; Assumption. +Qed. + +Lemma lt_plus_plus : (n,m,p,q:nat) n<m -> p<q -> (n+p)<(m+q). +Proof. + Intros. Apply lt_le_plus_plus. Assumption. + Apply lt_le_weak. Assumption. +Qed. + +(** Inversion lemmas *) + +Lemma plus_is_O : (m,n:nat) (m+n)=O -> m=O /\ n=O. +Proof. + Intro m; NewDestruct m; Auto. + Intros. Discriminate H. +Qed. + +Definition plus_is_one : + (m,n:nat) (m+n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}. +Proof. + Intro m; NewDestruct m; Auto. + NewDestruct n; Auto. + Intros. + Simpl in H. Discriminate H. +Defined. + +(** Derived properties *) + +Lemma plus_permute_2_in_4 : (m,n,p,q:nat) ((m+n)+(p+q))=((m+p)+(n+q)). +Proof. + Intros m n p q. + Rewrite <- (plus_assoc_l m n (p+q)). Rewrite (plus_assoc_l n p q). + Rewrite (plus_sym n p). Rewrite <- (plus_assoc_l p n q). Apply plus_assoc_l. +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:nat] : nat := + Cases n of + O => q + | (S p) => (plus_acc (S q) p) + end. + +Definition tail_plus := [n,m:nat](plus_acc m n). + +Lemma plus_tail_plus : (n,m:nat)(n+m)=(tail_plus n m). +Unfold tail_plus; NewInduction n as [|n IHn]; Simpl; Auto. +Intro m; Rewrite <- IHn; Simpl; Auto. +Qed. |