diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-10 17:46:01 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-10 17:46:01 +0000 |
commit | 9f8ccadf2f68ff44ee81d782b6881b9cc3c04c4b (patch) | |
tree | cb38ff6db4ade84d47f9788ae7bc821767abf638 /theories/Arith/Plus.v | |
parent | 20b4a46e9956537a0bb21c5eacf2539dee95cb67 (diff) |
mise sous CVS du repertoire theories/Arith
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@311 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Plus.v')
-rwxr-xr-x | theories/Arith/Plus.v | 113 |
1 files changed, 113 insertions, 0 deletions
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v new file mode 100755 index 000000000..f1bc532aa --- /dev/null +++ b/theories/Arith/Plus.v @@ -0,0 +1,113 @@ + +(* $Id$ *) + +(**************************************************************************) +(* Properties of addition *) +(**************************************************************************) + +Require Le. +Require Lt. + +Lemma plus_sym : (n,m:nat)((plus n m)=(plus 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. + +Lemma plus_Snm_nSm : + (n,m:nat)(plus (S n) m)=(plus n (S m)). +Intros. +Simpl. +Rewrite -> (plus_sym n m). +Rewrite -> (plus_sym n (S m)). +Trivial with arith. +Qed. + +Lemma simpl_plus_l : (n,m,p:nat)((plus n m)=(plus n p))->(m=p). +Proof. +Induction n ; Simpl ; Auto with arith. +Qed. + +Lemma plus_assoc_l : (n,m,p:nat)((plus n (plus m p))=(plus (plus 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) ((plus n (plus m p))=(plus m (plus 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)((plus (plus n m) p)=(plus n (plus m p))). +Proof. +Auto with arith. +Qed. +Hints Resolve plus_assoc_r : arith v62. + +Lemma simpl_le_plus_l : (p,n,m:nat)(le (plus p n) (plus p m))->(le n m). +Proof. +Induction p; Simpl; Auto with arith. +Qed. + +Lemma le_reg_l : (n,m,p:nat)(le n m)->(le (plus p n) (plus p m)). +Proof. +Induction p; Simpl; Auto with arith. +Qed. +Hints Resolve le_reg_l : arith v62. + +Lemma le_reg_r : (a,b,c:nat) (le a b)->(le (plus a c) (plus b c)). +Proof. +Induction 1 ; Simpl; Auto with arith. +Qed. +Hints Resolve le_reg_r : arith v62. + +Lemma le_plus_plus : + (n,m,p,q:nat) (le n m)->(le p q)->(le (plus n p) (plus m q)). +Proof. +Intros n m p q H H0. +Elim H; Simpl; Auto with arith. +Qed. + +Lemma le_plus_l : (n,m:nat)(le n (plus n m)). +Proof. +Induction n; Simpl; Auto with arith. +Qed. +Hints Resolve le_plus_l : arith v62. + +Lemma le_plus_r : (n,m:nat)(le m (plus 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)(le n m)->(le n (plus m p)). +Proof. +Intros; Apply le_trans with m; Auto with arith. +Qed. +Hints Resolve le_plus_trans : arith v62. + +Lemma simpl_lt_plus_l : (n,m,p:nat)(lt (plus p n) (plus p m))->(lt n m). +Proof. +Induction p; Simpl; Auto with arith. +Qed. + +Lemma lt_reg_l : (n,m,p:nat)(lt n m)->(lt (plus p n) (plus p m)). +Proof. +Induction p; Simpl; Auto with arith. +Qed. +Hints Resolve lt_reg_l : arith v62. + +Lemma lt_reg_r : (n,m,p:nat)(lt n m) -> (lt (plus n p) (plus 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. + +Theorem lt_plus_trans : (n,m,p:nat)(lt n m)->(lt n (plus m p)). +Proof. +Intros; Apply lt_le_trans with m; Auto with arith. +Qed. +Hints Immediate lt_plus_trans : arith v62. |