From c1d4048a12441df2977965b186bae9dcd32d4129 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 7 Mar 2017 09:16:16 +0100 Subject: Decimal: proofs that conversions from/to nat,N,Z are bijections --- theories/Arith/PeanoNat.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'theories/Arith') 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 -- cgit v1.2.3