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/Init/Decimal.v | 102 ++++++++++++++++++++++++++---------------------- theories/Init/Nat.v | 38 ++++++++---------- 2 files changed, 72 insertions(+), 68 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index bf4764895..fa462f147 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -50,23 +50,29 @@ Bind Scope int_scope with int. and choose our canonical representation of 0 (here [D0 Nil] for unsigned numbers and [Pos (D0 Nil)] for signed numbers). *) -Fixpoint nonzero_head d := +(** [nzhead] removes all head zero digits *) + +Fixpoint nzhead d := match d with - | D0 d => nonzero_head d + | D0 d => nzhead d | _ => d end. +(** [unorm] : normalization of unsigned integers *) + Definition unorm d := - match nonzero_head d with + match nzhead d with | Nil => zero | d => d end. +(** [norm] : normalization of signed integers *) + Definition norm d := match d with | Pos d => Pos (unorm d) | Neg d => - match nonzero_head d with + match nzhead d with | Nil => Pos zero | d => Neg d end @@ -84,21 +90,23 @@ Definition opp (d:int) := (** For conversions with binary numbers, it is easier to operate on little-endian numbers. *) -Fixpoint rev (l l' : uint) := - match l with - | Nil => l' - | D0 l => rev l (D0 l') - | D1 l => rev l (D1 l') - | D2 l => rev l (D2 l') - | D3 l => rev l (D3 l') - | D4 l => rev l (D4 l') - | D5 l => rev l (D5 l') - | D6 l => rev l (D6 l') - | D7 l => rev l (D7 l') - | D8 l => rev l (D8 l') - | D9 l => rev l (D9 l') +Fixpoint revapp (d d' : uint) := + match d with + | Nil => d' + | D0 d => revapp d (D0 d') + | D1 d => revapp d (D1 d') + | D2 d => revapp d (D2 d') + | D3 d => revapp d (D3 d') + | D4 d => revapp d (D4 d') + | D5 d => revapp d (D5 d') + | D6 d => revapp d (D6 d') + | D7 d => revapp d (D7 d') + | D8 d => revapp d (D8 d') + | D9 d => revapp d (D9 d') end. +Definition rev d := revapp d Nil. + Module Little. (** Successor of little-endian numbers *) @@ -106,16 +114,16 @@ Module Little. Fixpoint succ d := match d with | Nil => D1 Nil - | D0 l => D1 l - | D1 l => D2 l - | D2 l => D3 l - | D3 l => D4 l - | D4 l => D5 l - | D5 l => D6 l - | D6 l => D7 l - | D7 l => D8 l - | D8 l => D9 l - | D9 l => D0 (succ l) + | D0 d => D1 d + | D1 d => D2 d + | D2 d => D3 d + | D3 d => D4 d + | D4 d => D5 d + | D5 d => D6 d + | D6 d => D7 d + | D7 d => D8 d + | D8 d => D9 d + | D9 d => D0 (succ d) end. (** Doubling little-endian numbers *) @@ -123,31 +131,31 @@ Fixpoint succ d := Fixpoint double d := match d with | Nil => Nil - | D0 l => D0 (double l) - | D1 l => D2 (double l) - | D2 l => D4 (double l) - | D3 l => D6 (double l) - | D4 l => D8 (double l) - | D5 l => D0 (succ_double l) - | D6 l => D2 (succ_double l) - | D7 l => D4 (succ_double l) - | D8 l => D6 (succ_double l) - | D9 l => D8 (succ_double l) + | D0 d => D0 (double d) + | D1 d => D2 (double d) + | D2 d => D4 (double d) + | D3 d => D6 (double d) + | D4 d => D8 (double d) + | D5 d => D0 (succ_double d) + | D6 d => D2 (succ_double d) + | D7 d => D4 (succ_double d) + | D8 d => D6 (succ_double d) + | D9 d => D8 (succ_double d) end with succ_double d := match d with | Nil => D1 Nil - | D0 l => D1 (double l) - | D1 l => D3 (double l) - | D2 l => D5 (double l) - | D3 l => D7 (double l) - | D4 l => D9 (double l) - | D5 l => D1 (succ_double l) - | D6 l => D3 (succ_double l) - | D7 l => D5 (succ_double l) - | D8 l => D7 (succ_double l) - | D9 l => D9 (succ_double l) + | D0 d => D1 (double d) + | D1 d => D3 (double d) + | D2 d => D5 (double d) + | D3 d => D7 (double d) + | D4 d => D9 (double d) + | D5 d => D1 (succ_double d) + | D6 d => D3 (succ_double d) + | D7 d => D5 (succ_double d) + | D8 d => D7 (succ_double d) + | D9 d => D9 (succ_double d) end. End Little. 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 -- cgit v1.2.3