Decimal: proofs that conversions from/to nat,N,Z are bijections

2 files changed, 72 insertions, 68 deletions

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