diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-03-07 09:16:16 +0100 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-02-20 19:12:35 -0500 |
commit | c1d4048a12441df2977965b186bae9dcd32d4129 (patch) | |
tree | cff7fca9f6199a231fb4651de677862d0a88e0dc /theories/Init/Nat.v | |
parent | 960d48790121b876e6be7ca033138f5d28eae0cb (diff) |
Decimal: proofs that conversions from/to nat,N,Z are bijections
Diffstat (limited to 'theories/Init/Nat.v')
-rw-r--r-- | theories/Init/Nat.v | 38 |
1 files changed, 17 insertions, 21 deletions
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index 72d35827e..8f2648269 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.v @@ -136,25 +136,21 @@ where "n ^ m" := (pow n m) : nat_scope. (** ** Tail-recursive versions of [add] and [mul] *) -Module Tail. - -Fixpoint add n m := +Fixpoint tail_add n m := match n with | O => m - | S n => add n (S m) + | S n => tail_add n (S m) end. -(** [addmul r n m] is [r + n * m]. *) +(** [tail_addmul r n m] is [r + n * m]. *) -Fixpoint addmul r n m := +Fixpoint tail_addmul r n m := match n with | O => r - | S n => addmul (add m r) n m + | S n => tail_addmul (tail_add m r) n m end. -Definition mul n m := addmul 0 n m. - -End Tail. +Definition tail_mul n m := tail_addmul 0 n m. (** ** Conversion with a decimal representation for printing/parsing *) @@ -163,16 +159,16 @@ Local Notation ten := (S (S (S (S (S (S (S (S (S (S O)))))))))). Fixpoint of_uint_acc (d:Decimal.uint)(acc:nat) := match d with | Decimal.Nil => acc - | Decimal.D0 d => of_uint_acc d (Tail.mul ten acc) - | Decimal.D1 d => of_uint_acc d (S (Tail.mul ten acc)) - | Decimal.D2 d => of_uint_acc d (S (S (Tail.mul ten acc))) - | Decimal.D3 d => of_uint_acc d (S (S (S (Tail.mul ten acc)))) - | Decimal.D4 d => of_uint_acc d (S (S (S (S (Tail.mul ten acc))))) - | Decimal.D5 d => of_uint_acc d (S (S (S (S (S (Tail.mul ten acc)))))) - | Decimal.D6 d => of_uint_acc d (S (S (S (S (S (S (Tail.mul ten acc))))))) - | Decimal.D7 d => of_uint_acc d (S (S (S (S (S (S (S (Tail.mul ten acc)))))))) - | Decimal.D8 d => of_uint_acc d (S (S (S (S (S (S (S (S (Tail.mul ten acc))))))))) - | Decimal.D9 d => of_uint_acc d (S (S (S (S (S (S (S (S (S (Tail.mul ten acc)))))))))) + | Decimal.D0 d => of_uint_acc d (tail_mul ten acc) + | Decimal.D1 d => of_uint_acc d (S (tail_mul ten acc)) + | Decimal.D2 d => of_uint_acc d (S (S (tail_mul ten acc))) + | Decimal.D3 d => of_uint_acc d (S (S (S (tail_mul ten acc)))) + | Decimal.D4 d => of_uint_acc d (S (S (S (S (tail_mul ten acc))))) + | Decimal.D5 d => of_uint_acc d (S (S (S (S (S (tail_mul ten acc)))))) + | Decimal.D6 d => of_uint_acc d (S (S (S (S (S (S (tail_mul ten acc))))))) + | Decimal.D7 d => of_uint_acc d (S (S (S (S (S (S (S (tail_mul ten acc)))))))) + | Decimal.D8 d => of_uint_acc d (S (S (S (S (S (S (S (S (tail_mul ten acc))))))))) + | Decimal.D9 d => of_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul ten acc)))))))))) end. Definition of_uint (d:Decimal.uint) := of_uint_acc d O. @@ -184,7 +180,7 @@ Fixpoint to_little_uint n acc := end. Definition to_uint n := - Decimal.rev (to_little_uint n Decimal.zero) Decimal.Nil. + Decimal.rev (to_little_uint n Decimal.zero). Definition of_int (d:Decimal.int) : option nat := match Decimal.norm d with |