diff options
Diffstat (limited to 'theories/Arith/PeanoNat.v')
| -rw-r--r-- | theories/Arith/PeanoNat.v | 30 |
1 files changed, 26 insertions, 4 deletions
diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index bde6f1bb4..4e4938a99 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) @@ -724,6 +726,26 @@ Definition shiftr_spec a n m (_:0<=m) := shiftr_specif a n m. Include NExtraProp. +(** Properties of tail-recursive addition and multiplication *) + +Lemma tail_add_spec n m : tail_add n m = n + m. +Proof. + revert m. induction n as [|n IH]; simpl; trivial. + intros. now rewrite IH, add_succ_r. +Qed. + +Lemma tail_addmul_spec r n m : tail_addmul r n m = r + n * m. +Proof. + revert m r. induction n as [| n IH]; simpl; trivial. + intros. rewrite IH, tail_add_spec. + rewrite add_assoc. f_equal. apply add_comm. +Qed. + +Lemma tail_mul_spec n m : tail_mul n m = n * m. +Proof. + unfold tail_mul. now rewrite tail_addmul_spec. +Qed. + End Nat. (** Re-export notations that should be available even when |