aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-03-07 09:16:16 +0100
committerGravatar Jason Gross <jgross@mit.edu>2018-02-20 19:12:35 -0500
commitc1d4048a12441df2977965b186bae9dcd32d4129 (patch)
treecff7fca9f6199a231fb4651de677862d0a88e0dc /theories/Arith
parent960d48790121b876e6be7ca033138f5d28eae0cb (diff)
Decimal: proofs that conversions from/to nat,N,Z are bijections
Diffstat (limited to 'theories/Arith')
-rw-r--r--theories/Arith/PeanoNat.v20
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