diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-24 09:29:26 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-24 09:29:26 +0100 |
| commit | 89bd76b6f6a534613b03aaa970baf513b7c9b76b (patch) | |
| tree | bfba682b6121778a64fcf1f593c37e4a6674990f /theories/Arith | |
| parent | 7895d276146496648d576914aab4aded4b4a32cd (diff) | |
| parent | 63da69cff704be2da61f3cd311fa7a67dca6fc51 (diff) | |
Merge PR #6599: Decimals in prelude
Diffstat (limited to 'theories/Arith')
| -rw-r--r-- | theories/Arith/PeanoNat.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index bde6f1bb4..68060900c 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -724,6 +724,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 |