From 960d48790121b876e6be7ca033138f5d28eae0cb Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 27 Feb 2017 19:56:27 +0100
Subject: Decimal: simple representation of base-10 numbers
---
theories/Init/Decimal.v | 153 ++++++++++++++++++++++++++++++++++++++++++++
theories/Init/Nat.v | 62 +++++++++++++++++-
theories/Init/Prelude.v | 1 +
theories/NArith/BinNatDef.v | 18 ++++++
theories/PArith/BinPosDef.v | 55 ++++++++++++++++
theories/ZArith/BinIntDef.v | 17 +++++
6 files changed, 305 insertions(+), 1 deletion(-)
create mode 100644 theories/Init/Decimal.v
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
new file mode 100644
index 000000000..bf4764895
--- /dev/null
+++ b/theories/Init/Decimal.v
@@ -0,0 +1,153 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* nonzero_head d
+ | _ => d
+ end.
+
+Definition unorm d :=
+ match nonzero_head d with
+ | Nil => zero
+ | d => d
+ end.
+
+Definition norm d :=
+ match d with
+ | Pos d => Pos (unorm d)
+ | Neg d =>
+ match nonzero_head d with
+ | Nil => Pos zero
+ | d => Neg d
+ end
+ end.
+
+(** A few easy operations. For more advanced computations, use the conversions
+ with other Coq numeral datatypes (e.g. Z) and the operations on them. *)
+
+Definition opp (d:int) :=
+ match d with
+ | Pos d => Neg d
+ | Neg d => Pos d
+ end.
+
+(** 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')
+ end.
+
+Module Little.
+
+(** Successor of little-endian numbers *)
+
+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)
+ end.
+
+(** Doubling little-endian numbers *)
+
+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)
+ 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)
+ end.
+
+End Little.
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index e942ca562..72d35827e 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -7,7 +7,7 @@
(************************************************************************)
Require Import Notations Logic Datatypes.
-
+Require Decimal.
Local Open Scope nat_scope.
(**********************************************************************)
@@ -134,6 +134,66 @@ Fixpoint pow n m :=
where "n ^ m" := (pow n m) : nat_scope.
+(** ** Tail-recursive versions of [add] and [mul] *)
+
+Module Tail.
+
+Fixpoint add n m :=
+ match n with
+ | O => m
+ | S n => add n (S m)
+ end.
+
+(** [addmul r n m] is [r + n * m]. *)
+
+Fixpoint addmul r n m :=
+ match n with
+ | O => r
+ | S n => addmul (add m r) n m
+ end.
+
+Definition mul n m := addmul 0 n m.
+
+End Tail.
+
+(** ** Conversion with a decimal representation for printing/parsing *)
+
+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))))))))))
+ end.
+
+Definition of_uint (d:Decimal.uint) := of_uint_acc d O.
+
+Fixpoint to_little_uint n acc :=
+ match n with
+ | O => acc
+ | S n => to_little_uint n (Decimal.Little.succ acc)
+ end.
+
+Definition to_uint n :=
+ Decimal.rev (to_little_uint n Decimal.zero) Decimal.Nil.
+
+Definition of_int (d:Decimal.int) : option nat :=
+ match Decimal.norm d with
+ | Decimal.Pos u => Some (of_uint u)
+ | _ => None
+ end.
+
+Definition to_int n := Decimal.Pos (to_uint n).
+
(** ** Euclidean division *)
(** This division is linear and tail-recursive.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index f0867a034..63c431e8e 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -11,6 +11,7 @@ Require Export Logic.
Require Export Logic_Type.
Require Export Datatypes.
Require Export Specif.
+Require Coq.Init.Decimal.
Require Coq.Init.Nat.
Require Export Peano.
Require Export Coq.Init.Wf.
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 6771e57ad..e07758914 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -378,4 +378,22 @@ Definition iter (n:N) {A} (f:A->A) (x:A) : A :=
| pos p => Pos.iter f x p
end.
+(** Conversion with a decimal representation for printing/parsing *)
+
+Definition of_uint (d:Decimal.uint) := Pos.of_uint d.
+
+Definition of_int (d:Decimal.int) :=
+ match Decimal.norm d with
+ | Decimal.Pos d => Some (Pos.of_uint d)
+ | Decimal.Neg _ => None
+ end.
+
+Definition to_uint n :=
+ match n with
+ | 0 => Decimal.zero
+ | pos p => Pos.to_uint p
+ end.
+
+Definition to_int n := Decimal.Pos (to_uint n).
+
End N.
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 2b647555c..85c401cf4 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -557,4 +557,59 @@ Fixpoint of_succ_nat (n:nat) : positive :=
| S x => succ (of_succ_nat x)
end.
+(** ** Conversion with a decimal representation for printing/parsing *)
+
+Local Notation ten := 1~0~1~0.
+
+Fixpoint of_uint_acc (d:Decimal.uint)(acc:positive) :=
+ match d with
+ | Decimal.Nil => acc
+ | Decimal.D0 l => of_uint_acc l (mul ten acc)
+ | Decimal.D1 l => of_uint_acc l (add 1 (mul ten acc))
+ | Decimal.D2 l => of_uint_acc l (add 1~0 (mul ten acc))
+ | Decimal.D3 l => of_uint_acc l (add 1~1 (mul ten acc))
+ | Decimal.D4 l => of_uint_acc l (add 1~0~0 (mul ten acc))
+ | Decimal.D5 l => of_uint_acc l (add 1~0~1 (mul ten acc))
+ | Decimal.D6 l => of_uint_acc l (add 1~1~0 (mul ten acc))
+ | Decimal.D7 l => of_uint_acc l (add 1~1~1 (mul ten acc))
+ | Decimal.D8 l => of_uint_acc l (add 1~0~0~0 (mul ten acc))
+ | Decimal.D9 l => of_uint_acc l (add 1~0~0~1 (mul ten acc))
+ end.
+
+Fixpoint of_uint (d:Decimal.uint) : N :=
+ match d with
+ | Decimal.Nil => N0
+ | Decimal.D0 l => of_uint l
+ | Decimal.D1 l => Npos (of_uint_acc l 1)
+ | Decimal.D2 l => Npos (of_uint_acc l 1~0)
+ | Decimal.D3 l => Npos (of_uint_acc l 1~1)
+ | Decimal.D4 l => Npos (of_uint_acc l 1~0~0)
+ | Decimal.D5 l => Npos (of_uint_acc l 1~0~1)
+ | Decimal.D6 l => Npos (of_uint_acc l 1~1~0)
+ | Decimal.D7 l => Npos (of_uint_acc l 1~1~1)
+ | Decimal.D8 l => Npos (of_uint_acc l 1~0~0~0)
+ | Decimal.D9 l => Npos (of_uint_acc l 1~0~0~1)
+ end.
+
+Definition of_int (d:Decimal.int) : option positive :=
+ match d with
+ | Decimal.Pos d =>
+ match of_uint d with
+ | N0 => None
+ | Npos p => Some p
+ end
+ | Decimal.Neg _ => None
+ end.
+
+Fixpoint to_little_uint p :=
+ match p with
+ | 1 => Decimal.D1 Decimal.Nil
+ | p~1 => Decimal.Little.succ_double (to_little_uint p)
+ | p~0 => Decimal.Little.double (to_little_uint p)
+ end.
+
+Definition to_uint p := Decimal.rev (to_little_uint p) Decimal.Nil.
+
+Definition to_int n := Decimal.Pos (to_uint n).
+
End Pos.
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 443667f48..a0393f318 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -299,6 +299,23 @@ Definition to_pos (z:Z) : positive :=
| _ => 1%positive
end.
+(** Conversion with a decimal representation for printing/parsing *)
+
+Definition of_uint (d:Decimal.uint) := of_N (Pos.of_uint d).
+
+Definition of_int (d:Decimal.int) :=
+ match d with
+ | Decimal.Pos d => of_uint d
+ | Decimal.Neg d => opp (of_uint d)
+ end.
+
+Definition to_int n :=
+ match n with
+ | 0 => Decimal.Pos Decimal.zero
+ | pos p => Decimal.Pos (Pos.to_uint p)
+ | neg p => Decimal.Neg (Pos.to_uint p)
+ end.
+
(** ** Iteration of a function
By convention, iterating a negative number of times is identity.
--
cgit v1.2.3
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 +++
theories/Init/Decimal.v | 102 ++++++-----
theories/Init/Nat.v | 38 ++--
theories/Numbers/DecimalFacts.v | 141 +++++++++++++++
theories/Numbers/DecimalN.v | 105 +++++++++++
theories/Numbers/DecimalNat.v | 300 +++++++++++++++++++++++++++++++
theories/Numbers/DecimalPos.v | 381 ++++++++++++++++++++++++++++++++++++++++
theories/Numbers/DecimalZ.v | 73 ++++++++
theories/PArith/BinPosDef.v | 2 +-
9 files changed, 1093 insertions(+), 69 deletions(-)
create mode 100644 theories/Numbers/DecimalFacts.v
create mode 100644 theories/Numbers/DecimalN.v
create mode 100644 theories/Numbers/DecimalNat.v
create mode 100644 theories/Numbers/DecimalPos.v
create mode 100644 theories/Numbers/DecimalZ.v
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
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
diff --git a/theories/Numbers/DecimalFacts.v b/theories/Numbers/DecimalFacts.v
new file mode 100644
index 000000000..3eef63c7f
--- /dev/null
+++ b/theories/Numbers/DecimalFacts.v
@@ -0,0 +1,141 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* d' }.
+Proof.
+ decide equality.
+Defined.
+
+Lemma rev_revapp d d' :
+ rev (revapp d d') = revapp d' d.
+Proof.
+ revert d'. induction d; simpl; intros; now rewrite ?IHd.
+Qed.
+
+Lemma rev_rev d : rev (rev d) = d.
+Proof.
+ apply rev_revapp.
+Qed.
+
+(** Normalization on little-endian numbers *)
+
+Fixpoint nztail d :=
+ match d with
+ | Nil => Nil
+ | D0 d => match nztail d with Nil => Nil | d' => D0 d' end
+ | D1 d => D1 (nztail d)
+ | D2 d => D2 (nztail d)
+ | D3 d => D3 (nztail d)
+ | D4 d => D4 (nztail d)
+ | D5 d => D5 (nztail d)
+ | D6 d => D6 (nztail d)
+ | D7 d => D7 (nztail d)
+ | D8 d => D8 (nztail d)
+ | D9 d => D9 (nztail d)
+ end.
+
+Definition lnorm d :=
+ match nztail d with
+ | Nil => zero
+ | d => d
+ end.
+
+Lemma nzhead_revapp_0 d d' : nztail d = Nil ->
+ nzhead (revapp d d') = nzhead d'.
+Proof.
+ revert d'. induction d; intros d' [=]; simpl; trivial.
+ destruct (nztail d); now rewrite IHd.
+Qed.
+
+Lemma nzhead_revapp d d' : nztail d <> Nil ->
+ nzhead (revapp d d') = revapp (nztail d) d'.
+Proof.
+ revert d'.
+ induction d; intros d' H; simpl in *;
+ try destruct (nztail d) eqn:E;
+ (now rewrite ?nzhead_revapp_0) || (now rewrite IHd).
+Qed.
+
+Lemma nzhead_rev d : nztail d <> Nil ->
+ nzhead (rev d) = rev (nztail d).
+Proof.
+ apply nzhead_revapp.
+Qed.
+
+Lemma rev_nztail_rev d :
+ rev (nztail (rev d)) = nzhead d.
+Proof.
+ destruct (uint_dec (nztail (rev d)) Nil) as [H|H].
+ - rewrite H. unfold rev; simpl.
+ rewrite <- (rev_rev d). symmetry.
+ now apply nzhead_revapp_0.
+ - now rewrite <- nzhead_rev, rev_rev.
+Qed.
+
+Lemma revapp_nil_inv d d' : revapp d d' = Nil -> d = Nil /\ d' = Nil.
+Proof.
+ revert d'.
+ induction d; simpl; intros d' H; auto; now apply IHd in H.
+Qed.
+
+Lemma rev_nil_inv d : rev d = Nil -> d = Nil.
+Proof.
+ apply revapp_nil_inv.
+Qed.
+
+Lemma rev_lnorm_rev d :
+ rev (lnorm (rev d)) = unorm d.
+Proof.
+ unfold unorm, lnorm.
+ rewrite <- rev_nztail_rev.
+ destruct nztail; simpl; trivial;
+ destruct rev eqn:E; trivial; now apply rev_nil_inv in E.
+Qed.
+
+Lemma nzhead_nonzero d d' : nzhead d <> D0 d'.
+Proof.
+ induction d; easy.
+Qed.
+
+Lemma unorm_0 d : unorm d = zero <-> nzhead d = Nil.
+Proof.
+ unfold unorm. split.
+ - generalize (nzhead_nonzero d).
+ destruct nzhead; intros H [=]; trivial. now destruct (H u).
+ - now intros ->.
+Qed.
+
+Lemma unorm_nonnil d : unorm d <> Nil.
+Proof.
+ unfold unorm. now destruct nzhead.
+Qed.
+
+Lemma nzhead_invol d : nzhead (nzhead d) = nzhead d.
+Proof.
+ now induction d.
+Qed.
+
+Lemma unorm_invol d : unorm (unorm d) = unorm d.
+Proof.
+ unfold unorm.
+ destruct (nzhead d) eqn:E; trivial.
+ destruct (nzhead_nonzero _ _ E).
+Qed.
+
+Lemma norm_invol d : norm (norm d) = norm d.
+Proof.
+ unfold norm.
+ destruct d.
+ - f_equal. apply unorm_invol.
+ - destruct (nzhead d) eqn:E; auto.
+ destruct (nzhead_nonzero _ _ E).
+Qed.
diff --git a/theories/Numbers/DecimalN.v b/theories/Numbers/DecimalN.v
new file mode 100644
index 000000000..998f009a7
--- /dev/null
+++ b/theories/Numbers/DecimalN.v
@@ -0,0 +1,105 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* n = n'.
+Proof.
+ intros E. now rewrite <- (of_to n), <- (of_to n'), E.
+Qed.
+
+Lemma to_uint_surj d : exists p, N.to_uint p = unorm d.
+Proof.
+ exists (N.of_uint d). apply to_of.
+Qed.
+
+Lemma of_uint_norm d : N.of_uint (unorm d) = N.of_uint d.
+Proof.
+ now induction d.
+Qed.
+
+Lemma of_inj d d' :
+ N.of_uint d = N.of_uint d' -> unorm d = unorm d'.
+Proof.
+ intros. rewrite <- !to_of. now f_equal.
+Qed.
+
+Lemma of_iff d d' : N.of_uint d = N.of_uint d' <-> unorm d = unorm d'.
+Proof.
+ split. apply of_inj. intros E. rewrite <- of_uint_norm, E.
+ apply of_uint_norm.
+Qed.
+
+End Unsigned.
+
+(** Conversion from/to signed decimal numbers *)
+
+Module Signed.
+
+Lemma of_to (n:N) : N.of_int (N.to_int n) = Some n.
+Proof.
+ unfold N.to_int, N.of_int, norm. f_equal.
+ rewrite Unsigned.of_uint_norm. apply Unsigned.of_to.
+Qed.
+
+Lemma to_of (d:int)(n:N) : N.of_int d = Some n -> N.to_int n = norm d.
+Proof.
+ unfold N.of_int.
+ destruct (norm d) eqn:Hd; intros [= <-].
+ unfold N.to_int. rewrite Unsigned.to_of. f_equal.
+ revert Hd; destruct d; simpl.
+ - intros [= <-]. apply unorm_invol.
+ - destruct (nzhead d); now intros [= <-].
+Qed.
+
+Lemma to_int_inj n n' : N.to_int n = N.to_int n' -> n = n'.
+Proof.
+ intro E.
+ assert (E' : Some n = Some n').
+ { now rewrite <- (of_to n), <- (of_to n'), E. }
+ now injection E'.
+Qed.
+
+Lemma to_int_pos_surj d : exists n, N.to_int n = norm (Pos d).
+Proof.
+ exists (N.of_uint d). unfold N.to_int. now rewrite Unsigned.to_of.
+Qed.
+
+Lemma of_int_norm d : N.of_int (norm d) = N.of_int d.
+Proof.
+ unfold N.of_int. now rewrite norm_invol.
+Qed.
+
+Lemma of_inj_pos d d' :
+ N.of_int (Pos d) = N.of_int (Pos d') -> unorm d = unorm d'.
+Proof.
+ unfold N.of_int. simpl. intros [= H]. apply Unsigned.of_inj.
+ change Pos.of_uint with N.of_uint in H.
+ now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm.
+Qed.
+
+End Signed.
diff --git a/theories/Numbers/DecimalNat.v b/theories/Numbers/DecimalNat.v
new file mode 100644
index 000000000..4aa189e24
--- /dev/null
+++ b/theories/Numbers/DecimalNat.v
@@ -0,0 +1,300 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* 0
+ | D0 _ => 0
+ | D1 _ => 1
+ | D2 _ => 2
+ | D3 _ => 3
+ | D4 _ => 4
+ | D5 _ => 5
+ | D6 _ => 6
+ | D7 _ => 7
+ | D8 _ => 8
+ | D9 _ => 9
+end.
+
+Definition tl d :=
+ match d with
+ | Nil => d
+ | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => d
+end.
+
+Fixpoint usize (d:uint) : nat :=
+ match d with
+ | Nil => 0
+ | D0 d => S (usize d)
+ | D1 d => S (usize d)
+ | D2 d => S (usize d)
+ | D3 d => S (usize d)
+ | D4 d => S (usize d)
+ | D5 d => S (usize d)
+ | D6 d => S (usize d)
+ | D7 d => S (usize d)
+ | D8 d => S (usize d)
+ | D9 d => S (usize d)
+ end.
+
+(** A direct version of [to_little_uint], not tail-recursive *)
+Fixpoint to_lu n :=
+ match n with
+ | 0 => Decimal.zero
+ | S n => Little.succ (to_lu n)
+ end.
+
+(** A direct version of [of_little_uint] *)
+Fixpoint of_lu (d:uint) : nat :=
+ match d with
+ | Nil => 0
+ | D0 d => 10 * of_lu d
+ | D1 d => 1 + 10 * of_lu d
+ | D2 d => 2 + 10 * of_lu d
+ | D3 d => 3 + 10 * of_lu d
+ | D4 d => 4 + 10 * of_lu d
+ | D5 d => 5 + 10 * of_lu d
+ | D6 d => 6 + 10 * of_lu d
+ | D7 d => 7 + 10 * of_lu d
+ | D8 d => 8 + 10 * of_lu d
+ | D9 d => 9 + 10 * of_lu d
+ end.
+
+(** Properties of [to_lu] *)
+
+Lemma to_lu_succ n : to_lu (S n) = Little.succ (to_lu n).
+Proof.
+ reflexivity.
+Qed.
+
+Lemma to_little_uint_succ n d :
+ Nat.to_little_uint n (Little.succ d) =
+ Little.succ (Nat.to_little_uint n d).
+Proof.
+ revert d; induction n; simpl; trivial.
+Qed.
+
+Lemma to_lu_equiv n :
+ to_lu n = Nat.to_little_uint n zero.
+Proof.
+ induction n; simpl; trivial.
+ now rewrite IHn, <- to_little_uint_succ.
+Qed.
+
+Lemma to_uint_alt n :
+ Nat.to_uint n = rev (to_lu n).
+Proof.
+ unfold Nat.to_uint. f_equal. symmetry. apply to_lu_equiv.
+Qed.
+
+(** Properties of [of_lu] *)
+
+Lemma of_lu_eqn d :
+ of_lu d = hd d + 10 * of_lu (tl d).
+Proof.
+ induction d; simpl; trivial.
+Qed.
+
+Ltac simpl_of_lu :=
+ match goal with
+ | |- context [ of_lu (?f ?x) ] =>
+ rewrite (of_lu_eqn (f x)); simpl hd; simpl tl
+ end.
+
+Lemma of_lu_succ d :
+ of_lu (Little.succ d) = S (of_lu d).
+Proof.
+ induction d; trivial.
+ simpl_of_lu. rewrite IHd. simpl_of_lu.
+ now rewrite Nat.mul_succ_r, <- (Nat.add_comm 10).
+Qed.
+
+Lemma of_to_lu n :
+ of_lu (to_lu n) = n.
+Proof.
+ induction n; simpl; trivial. rewrite of_lu_succ. now f_equal.
+Qed.
+
+Lemma of_lu_revapp d d' :
+of_lu (revapp d d') =
+ of_lu (rev d) + of_lu d' * 10^usize d.
+Proof.
+ revert d'.
+ induction d; intro d'; simpl usize;
+ [ simpl; now rewrite Nat.mul_1_r | .. ];
+ unfold rev; simpl revapp; rewrite 2 IHd;
+ rewrite <- Nat.add_assoc; f_equal; simpl_of_lu; simpl of_lu;
+ rewrite Nat.pow_succ_r'; ring.
+Qed.
+
+Lemma of_uint_acc_spec n d :
+ Nat.of_uint_acc d n = of_lu (rev d) + n * 10^usize d.
+Proof.
+ revert n. induction d; intros;
+ simpl Nat.of_uint_acc; rewrite ?Nat.tail_mul_spec, ?IHd;
+ simpl rev; simpl usize; rewrite ?Nat.pow_succ_r';
+ [ simpl; now rewrite Nat.mul_1_r | .. ];
+ unfold rev at 2; simpl revapp; rewrite of_lu_revapp;
+ simpl of_lu; ring.
+Qed.
+
+Lemma of_uint_alt d : Nat.of_uint d = of_lu (rev d).
+Proof.
+ unfold Nat.of_uint. now rewrite of_uint_acc_spec.
+Qed.
+
+(** First main bijection result *)
+
+Lemma of_to (n:nat) : Nat.of_uint (Nat.to_uint n) = n.
+Proof.
+ rewrite to_uint_alt, of_uint_alt, rev_rev. apply of_to_lu.
+Qed.
+
+(** The other direction *)
+
+Lemma to_lu_tenfold n : n<>0 ->
+ to_lu (10 * n) = D0 (to_lu n).
+Proof.
+ induction n.
+ - simpl. now destruct 1.
+ - intros _.
+ destruct (Nat.eq_dec n 0) as [->|H]; simpl; trivial.
+ rewrite !Nat.add_succ_r.
+ simpl in *. rewrite (IHn H). now destruct (to_lu n).
+Qed.
+
+Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil.
+Proof.
+ induction d; try simpl_of_lu; try easy.
+ rewrite Nat.add_0_l.
+ split; intros H.
+ - apply Nat.eq_mul_0_r in H; auto.
+ rewrite IHd in H. simpl. now rewrite H.
+ - simpl in H. destruct (nztail d); try discriminate.
+ now destruct IHd as [_ ->].
+Qed.
+
+Lemma to_of_lu_tenfold d :
+ to_lu (of_lu d) = lnorm d ->
+ to_lu (10 * of_lu d) = lnorm (D0 d).
+Proof.
+ intro IH.
+ destruct (Nat.eq_dec (of_lu d) 0) as [H|H].
+ - rewrite H. simpl. rewrite of_lu_0 in H.
+ unfold lnorm. simpl. now rewrite H.
+ - rewrite (to_lu_tenfold _ H), IH.
+ rewrite of_lu_0 in H.
+ unfold lnorm. simpl. now destruct (nztail d).
+Qed.
+
+Lemma to_of_lu d : to_lu (of_lu d) = lnorm d.
+Proof.
+ induction d; [ reflexivity | .. ];
+ simpl_of_lu;
+ rewrite ?Nat.add_succ_l, Nat.add_0_l, ?to_lu_succ, to_of_lu_tenfold
+ by assumption;
+ unfold lnorm; simpl; now destruct nztail.
+Qed.
+
+(** Second bijection result *)
+
+Lemma to_of (d:uint) : Nat.to_uint (Nat.of_uint d) = unorm d.
+Proof.
+ rewrite to_uint_alt, of_uint_alt, to_of_lu.
+ apply rev_lnorm_rev.
+Qed.
+
+(** Some consequences *)
+
+Lemma to_uint_inj n n' : Nat.to_uint n = Nat.to_uint n' -> n = n'.
+Proof.
+ intro EQ.
+ now rewrite <- (of_to n), <- (of_to n'), EQ.
+Qed.
+
+Lemma to_uint_surj d : exists n, Nat.to_uint n = unorm d.
+Proof.
+ exists (Nat.of_uint d). apply to_of.
+Qed.
+
+Lemma of_uint_norm d : Nat.of_uint (unorm d) = Nat.of_uint d.
+Proof.
+ unfold Nat.of_uint. now induction d.
+Qed.
+
+Lemma of_inj d d' :
+ Nat.of_uint d = Nat.of_uint d' -> unorm d = unorm d'.
+Proof.
+ intros. rewrite <- !to_of. now f_equal.
+Qed.
+
+Lemma of_iff d d' : Nat.of_uint d = Nat.of_uint d' <-> unorm d = unorm d'.
+Proof.
+ split. apply of_inj. intros E. rewrite <- of_uint_norm, E.
+ apply of_uint_norm.
+Qed.
+
+End Unsigned.
+
+(** Conversion from/to signed decimal numbers *)
+
+Module Signed.
+
+Lemma of_to (n:nat) : Nat.of_int (Nat.to_int n) = Some n.
+Proof.
+ unfold Nat.to_int, Nat.of_int, norm. f_equal.
+ rewrite Unsigned.of_uint_norm. apply Unsigned.of_to.
+Qed.
+
+Lemma to_of (d:int)(n:nat) : Nat.of_int d = Some n -> Nat.to_int n = norm d.
+Proof.
+ unfold Nat.of_int.
+ destruct (norm d) eqn:Hd; intros [= <-].
+ unfold Nat.to_int. rewrite Unsigned.to_of. f_equal.
+ revert Hd; destruct d; simpl.
+ - intros [= <-]. apply unorm_invol.
+ - destruct (nzhead d); now intros [= <-].
+Qed.
+
+Lemma to_int_inj n n' : Nat.to_int n = Nat.to_int n' -> n = n'.
+Proof.
+ intro E.
+ assert (E' : Some n = Some n').
+ { now rewrite <- (of_to n), <- (of_to n'), E. }
+ now injection E'.
+Qed.
+
+Lemma to_int_pos_surj d : exists n, Nat.to_int n = norm (Pos d).
+Proof.
+ exists (Nat.of_uint d). unfold Nat.to_int. now rewrite Unsigned.to_of.
+Qed.
+
+Lemma of_int_norm d : Nat.of_int (norm d) = Nat.of_int d.
+Proof.
+ unfold Nat.of_int. now rewrite norm_invol.
+Qed.
+
+Lemma of_inj_pos d d' :
+ Nat.of_int (Pos d) = Nat.of_int (Pos d') -> unorm d = unorm d'.
+Proof.
+ unfold Nat.of_int. simpl. intros [= H]. apply Unsigned.of_inj.
+ now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm.
+Qed.
+
+End Signed.
diff --git a/theories/Numbers/DecimalPos.v b/theories/Numbers/DecimalPos.v
new file mode 100644
index 000000000..40c8f5a5a
--- /dev/null
+++ b/theories/Numbers/DecimalPos.v
@@ -0,0 +1,381 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* 0
+ | D0 d => 10 * of_lu d
+ | D1 d => 1 + 10 * of_lu d
+ | D2 d => 2 + 10 * of_lu d
+ | D3 d => 3 + 10 * of_lu d
+ | D4 d => 4 + 10 * of_lu d
+ | D5 d => 5 + 10 * of_lu d
+ | D6 d => 6 + 10 * of_lu d
+ | D7 d => 7 + 10 * of_lu d
+ | D8 d => 8 + 10 * of_lu d
+ | D9 d => 9 + 10 * of_lu d
+ end.
+
+Definition hd d :=
+match d with
+ | Nil => 0
+ | D0 _ => 0
+ | D1 _ => 1
+ | D2 _ => 2
+ | D3 _ => 3
+ | D4 _ => 4
+ | D5 _ => 5
+ | D6 _ => 6
+ | D7 _ => 7
+ | D8 _ => 8
+ | D9 _ => 9
+end.
+
+Definition tl d :=
+ match d with
+ | Nil => d
+ | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => d
+end.
+
+Lemma of_lu_eqn d :
+ of_lu d = hd d + 10 * (of_lu (tl d)).
+Proof.
+ induction d; simpl; trivial.
+Qed.
+
+Ltac simpl_of_lu :=
+ match goal with
+ | |- context [ of_lu (?f ?x) ] =>
+ rewrite (of_lu_eqn (f x)); simpl hd; simpl tl
+ end.
+
+Fixpoint usize (d:uint) : N :=
+ match d with
+ | Nil => 0
+ | D0 d => N.succ (usize d)
+ | D1 d => N.succ (usize d)
+ | D2 d => N.succ (usize d)
+ | D3 d => N.succ (usize d)
+ | D4 d => N.succ (usize d)
+ | D5 d => N.succ (usize d)
+ | D6 d => N.succ (usize d)
+ | D7 d => N.succ (usize d)
+ | D8 d => N.succ (usize d)
+ | D9 d => N.succ (usize d)
+ end.
+
+Lemma of_lu_revapp d d' :
+ of_lu (revapp d d') =
+ of_lu (rev d) + of_lu d' * 10^usize d.
+Proof.
+ revert d'.
+ induction d; simpl; intro d'; [ now rewrite N.mul_1_r | .. ];
+ unfold rev; simpl revapp; rewrite 2 IHd;
+ rewrite <- N.add_assoc; f_equal; simpl_of_lu; simpl of_lu;
+ rewrite N.pow_succ_r'; ring.
+Qed.
+
+Definition Nadd n p :=
+ match n with
+ | N0 => p
+ | Npos p0 => (p0+p)%positive
+ end.
+
+Lemma Nadd_simpl n p q : Npos (Nadd n (p * q)) = n + Npos p * Npos q.
+Proof.
+ now destruct n.
+Qed.
+
+Lemma of_uint_acc_eqn d acc : d<>Nil ->
+ Pos.of_uint_acc d acc = Pos.of_uint_acc (tl d) (Nadd (hd d) (10*acc)).
+Proof.
+ destruct d; simpl; trivial. now destruct 1.
+Qed.
+
+Lemma of_uint_acc_rev d acc :
+ Npos (Pos.of_uint_acc d acc) =
+ of_lu (rev d) + (Npos acc) * 10^usize d.
+Proof.
+ revert acc.
+ induction d; intros; simpl usize;
+ [ simpl; now rewrite Pos.mul_1_r | .. ];
+ rewrite N.pow_succ_r';
+ unfold rev; simpl revapp; try rewrite of_lu_revapp; simpl of_lu;
+ rewrite of_uint_acc_eqn by easy; simpl tl; simpl hd;
+ rewrite IHd, Nadd_simpl; ring.
+Qed.
+
+Lemma of_uint_alt d : Pos.of_uint d = of_lu (rev d).
+Proof.
+ induction d; simpl; trivial; unfold rev; simpl revapp;
+ rewrite of_lu_revapp; simpl of_lu; try apply of_uint_acc_rev.
+ rewrite IHd. ring.
+Qed.
+
+Lemma of_lu_rev d : Pos.of_uint (rev d) = of_lu d.
+Proof.
+ rewrite of_uint_alt. now rewrite rev_rev.
+Qed.
+
+Lemma of_lu_double_gen d :
+ of_lu (Little.double d) = N.double (of_lu d) /\
+ of_lu (Little.succ_double d) = N.succ_double (of_lu d).
+Proof.
+ rewrite N.double_spec, N.succ_double_spec.
+ induction d; try destruct IHd as (IH1,IH2);
+ simpl Little.double; simpl Little.succ_double;
+ repeat (simpl_of_lu; rewrite ?IH1, ?IH2); split; reflexivity || ring.
+Qed.
+
+Lemma of_lu_double d :
+ of_lu (Little.double d) = N.double (of_lu d).
+Proof.
+ apply of_lu_double_gen.
+Qed.
+
+Lemma of_lu_succ_double d :
+ of_lu (Little.succ_double d) = N.succ_double (of_lu d).
+Proof.
+ apply of_lu_double_gen.
+Qed.
+
+(** First bijection result *)
+
+Lemma of_to (p:positive) : Pos.of_uint (Pos.to_uint p) = Npos p.
+Proof.
+ unfold Pos.to_uint.
+ rewrite of_lu_rev.
+ induction p; simpl; trivial.
+ - now rewrite of_lu_succ_double, IHp.
+ - now rewrite of_lu_double, IHp.
+Qed.
+
+(** The other direction *)
+
+Definition to_lu n :=
+ match n with
+ | N0 => Decimal.zero
+ | Npos p => Pos.to_little_uint p
+ end.
+
+Lemma succ_double_alt d :
+ Little.succ_double d = Little.succ (Little.double d).
+Proof.
+ now induction d.
+Qed.
+
+Lemma double_succ d :
+ Little.double (Little.succ d) =
+ Little.succ (Little.succ_double d).
+Proof.
+ induction d; simpl; f_equal; auto using succ_double_alt.
+Qed.
+
+Lemma to_lu_succ n :
+ to_lu (N.succ n) = Little.succ (to_lu n).
+Proof.
+ destruct n; simpl; trivial.
+ induction p; simpl; rewrite ?IHp;
+ auto using succ_double_alt, double_succ.
+Qed.
+
+Lemma nat_iter_S n {A} (f:A->A) i :
+ Nat.iter (S n) f i = f (Nat.iter n f i).
+Proof.
+ reflexivity.
+Qed.
+
+Lemma nat_iter_0 {A} (f:A->A) i : Nat.iter 0 f i = i.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma to_ldec_tenfold p :
+ to_lu (10 * Npos p) = D0 (to_lu (Npos p)).
+Proof.
+ induction p using Pos.peano_rect.
+ - trivial.
+ - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)).
+ rewrite N.mul_succ_r.
+ change 10 at 2 with (Nat.iter 10%nat N.succ 0).
+ rewrite ?nat_iter_S, nat_iter_0.
+ rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp.
+ destruct (to_lu (N.pos p)); simpl; auto.
+Qed.
+
+Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil.
+Proof.
+ induction d; try simpl_of_lu; split; trivial; try discriminate;
+ try (intros H; now apply N.eq_add_0 in H).
+ - rewrite N.add_0_l. intros H.
+ apply N.eq_mul_0_r in H; [|easy]. rewrite IHd in H.
+ simpl. now rewrite H.
+ - simpl. destruct (nztail d); try discriminate.
+ now destruct IHd as [_ ->].
+Qed.
+
+Lemma to_of_lu_tenfold d :
+ to_lu (of_lu d) = lnorm d ->
+ to_lu (10 * of_lu d) = lnorm (D0 d).
+Proof.
+ intro IH.
+ destruct (N.eq_dec (of_lu d) 0) as [H|H].
+ - rewrite H. simpl. rewrite of_lu_0 in H.
+ unfold lnorm. simpl. now rewrite H.
+ - destruct (of_lu d) eqn:Eq; [easy| ].
+ rewrite to_ldec_tenfold; auto. rewrite IH.
+ rewrite <- Eq in H. rewrite of_lu_0 in H.
+ unfold lnorm. simpl. now destruct (nztail d).
+Qed.
+
+Lemma Nadd_alt n m : n + m = Nat.iter (N.to_nat n) N.succ m.
+Proof.
+ destruct n. trivial.
+ induction p using Pos.peano_rect.
+ - now rewrite N.add_1_l.
+ - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)).
+ now rewrite N.add_succ_l, IHp, N2Nat.inj_succ.
+Qed.
+
+Ltac simpl_to_nat := simpl N.to_nat; unfold Pos.to_nat; simpl Pos.iter_op.
+
+Lemma to_of_lu d : to_lu (of_lu d) = lnorm d.
+Proof.
+ induction d; [reflexivity|..];
+ simpl_of_lu; rewrite Nadd_alt; simpl_to_nat;
+ rewrite ?nat_iter_S, nat_iter_0, ?to_lu_succ, to_of_lu_tenfold by assumption;
+ unfold lnorm; simpl; destruct nztail; auto.
+Qed.
+
+(** Second bijection result *)
+
+Lemma to_of (d:uint) : N.to_uint (Pos.of_uint d) = unorm d.
+Proof.
+ rewrite of_uint_alt.
+ unfold N.to_uint, Pos.to_uint.
+ destruct (of_lu (rev d)) eqn:H.
+ - rewrite of_lu_0 in H. rewrite <- rev_lnorm_rev.
+ unfold lnorm. now rewrite H.
+ - change (Pos.to_little_uint p) with (to_lu (N.pos p)).
+ rewrite <- H. rewrite to_of_lu. apply rev_lnorm_rev.
+Qed.
+
+(** Some consequences *)
+
+Lemma to_uint_nonzero p : Pos.to_uint p <> zero.
+Proof.
+ intro E. generalize (of_to p). now rewrite E.
+Qed.
+
+Lemma to_uint_nonnil p : Pos.to_uint p <> Nil.
+Proof.
+ intros E. generalize (of_to p). now rewrite E.
+Qed.
+
+Lemma to_uint_inj p p' : Pos.to_uint p = Pos.to_uint p' -> p = p'.
+Proof.
+ intro E.
+ assert (E' : N.pos p = N.pos p').
+ { now rewrite <- (of_to p), <- (of_to p'), E. }
+ now injection E'.
+Qed.
+
+Lemma to_uint_pos_surj d :
+ unorm d<>zero -> exists p, Pos.to_uint p = unorm d.
+Proof.
+ intros.
+ destruct (Pos.of_uint d) eqn:E.
+ - destruct H. generalize (to_of d). now rewrite E.
+ - exists p. generalize (to_of d). now rewrite E.
+Qed.
+
+Lemma of_uint_norm d : Pos.of_uint (unorm d) = Pos.of_uint d.
+Proof.
+ now induction d.
+Qed.
+
+Lemma of_inj d d' :
+ Pos.of_uint d = Pos.of_uint d' -> unorm d = unorm d'.
+Proof.
+ intros. rewrite <- !to_of. now f_equal.
+Qed.
+
+Lemma of_iff d d' : Pos.of_uint d = Pos.of_uint d' <-> unorm d = unorm d'.
+Proof.
+ split. apply of_inj. intros E. rewrite <- of_uint_norm, E.
+ apply of_uint_norm.
+Qed.
+
+End Unsigned.
+
+(** Conversion from/to signed decimal numbers *)
+
+Module Signed.
+
+Lemma of_to (p:positive) : Pos.of_int (Pos.to_int p) = Some p.
+Proof.
+ unfold Pos.to_int, Pos.of_int, norm.
+ now rewrite Unsigned.of_to.
+Qed.
+
+Lemma to_of (d:int)(p:positive) :
+ Pos.of_int d = Some p -> Pos.to_int p = norm d.
+Proof.
+ unfold Pos.of_int.
+ destruct d; [ | intros [=]].
+ simpl norm. rewrite <- Unsigned.to_of.
+ destruct (Pos.of_uint d); now intros [= <-].
+Qed.
+
+Lemma to_int_inj p p' : Pos.to_int p = Pos.to_int p' -> p = p'.
+Proof.
+ intro E.
+ assert (E' : Some p = Some p').
+ { now rewrite <- (of_to p), <- (of_to p'), E. }
+ now injection E'.
+Qed.
+
+Lemma to_int_pos_surj d :
+ unorm d <> zero -> exists p, Pos.to_int p = norm (Pos d).
+Proof.
+ simpl. unfold Pos.to_int. intros H.
+ destruct (Unsigned.to_uint_pos_surj d H) as (p,Hp).
+ exists p. now f_equal.
+Qed.
+
+Lemma of_int_norm d : Pos.of_int (norm d) = Pos.of_int d.
+Proof.
+ unfold Pos.of_int.
+ destruct d.
+ - simpl. now rewrite Unsigned.of_uint_norm.
+ - simpl. now destruct (nzhead d) eqn:H.
+Qed.
+
+Lemma of_inj_pos d d' :
+ Pos.of_int (Pos d) = Pos.of_int (Pos d') -> unorm d = unorm d'.
+Proof.
+ unfold Pos.of_int.
+ destruct (Pos.of_uint d) eqn:Hd, (Pos.of_uint d') eqn:Hd';
+ intros [=].
+ - apply Unsigned.of_inj; now rewrite Hd, Hd'.
+ - apply Unsigned.of_inj; rewrite Hd, Hd'; now f_equal.
+Qed.
+
+End Signed.
diff --git a/theories/Numbers/DecimalZ.v b/theories/Numbers/DecimalZ.v
new file mode 100644
index 000000000..92d66ecfb
--- /dev/null
+++ b/theories/Numbers/DecimalZ.v
@@ -0,0 +1,73 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* n = n'.
+Proof.
+ intro EQ.
+ now rewrite <- (of_to n), <- (of_to n'), EQ.
+Qed.
+
+Lemma to_int_surj d : exists n, Z.to_int n = norm d.
+Proof.
+ exists (Z.of_int d). apply to_of.
+Qed.
+
+Lemma of_int_norm d : Z.of_int (norm d) = Z.of_int d.
+Proof.
+ unfold Z.of_int, Z.of_uint.
+ destruct d.
+ - simpl. now rewrite DecimalPos.Unsigned.of_uint_norm.
+ - simpl. destruct (nzhead d) eqn:H;
+ [ induction d; simpl; auto; discriminate |
+ destruct (nzhead_nonzero _ _ H) | .. ];
+ f_equal; f_equal; apply DecimalPos.Unsigned.of_iff;
+ unfold unorm; now rewrite H.
+Qed.
+
+Lemma of_inj d d' :
+ Z.of_int d = Z.of_int d' -> norm d = norm d'.
+Proof.
+ intros. rewrite <- !to_of. now f_equal.
+Qed.
+
+Lemma of_iff d d' : Z.of_int d = Z.of_int d' <-> norm d = norm d'.
+Proof.
+ split. apply of_inj. intros E. rewrite <- of_int_norm, E.
+ apply of_int_norm.
+Qed.
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 85c401cf4..a77c26e5a 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -608,7 +608,7 @@ Fixpoint to_little_uint p :=
| p~0 => Decimal.Little.double (to_little_uint p)
end.
-Definition to_uint p := Decimal.rev (to_little_uint p) Decimal.Nil.
+Definition to_uint p := Decimal.rev (to_little_uint p).
Definition to_int n := Decimal.Pos (to_uint n).
--
cgit v1.2.3
From 0f2b6099073ef9494f09cfd68edfd64508561b62 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 7 Mar 2017 12:31:29 +0100
Subject: Decimal goodies : conversion to/from Coq strings
Just because it's fun and easy. Not used by the Numeral Notation command.
---
theories/Numbers/DecimalString.v | 263 +++++++++++++++++++++++++++++++++++++++
1 file changed, 263 insertions(+)
create mode 100644 theories/Numbers/DecimalString.v
diff --git a/theories/Numbers/DecimalString.v b/theories/Numbers/DecimalString.v
new file mode 100644
index 000000000..7e937f481
--- /dev/null
+++ b/theories/Numbers/DecimalString.v
@@ -0,0 +1,263 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* None
+ | Some d =>
+ match a with
+ | "0" => Some (D0 d)
+ | "1" => Some (D1 d)
+ | "2" => Some (D2 d)
+ | "3" => Some (D3 d)
+ | "4" => Some (D4 d)
+ | "5" => Some (D5 d)
+ | "6" => Some (D6 d)
+ | "7" => Some (D7 d)
+ | "8" => Some (D8 d)
+ | "9" => Some (D9 d)
+ | _ => None
+ end
+ end%char.
+
+Lemma uint_of_char_spec c d d' :
+ uint_of_char c (Some d) = Some d' ->
+ (c = "0" /\ d' = D0 d \/
+ c = "1" /\ d' = D1 d \/
+ c = "2" /\ d' = D2 d \/
+ c = "3" /\ d' = D3 d \/
+ c = "4" /\ d' = D4 d \/
+ c = "5" /\ d' = D5 d \/
+ c = "6" /\ d' = D6 d \/
+ c = "7" /\ d' = D7 d \/
+ c = "8" /\ d' = D8 d \/
+ c = "9" /\ d' = D9 d)%char.
+Proof.
+ destruct c as [[|] [|] [|] [|] [|] [|] [|] [|]];
+ intros [= <-]; intuition.
+Qed.
+
+(** Decimal/String conversion where [Nil] is [""] *)
+
+Module NilEmpty.
+
+Fixpoint string_of_uint (d:uint) :=
+ match d with
+ | Nil => EmptyString
+ | D0 d => String "0" (string_of_uint d)
+ | D1 d => String "1" (string_of_uint d)
+ | D2 d => String "2" (string_of_uint d)
+ | D3 d => String "3" (string_of_uint d)
+ | D4 d => String "4" (string_of_uint d)
+ | D5 d => String "5" (string_of_uint d)
+ | D6 d => String "6" (string_of_uint d)
+ | D7 d => String "7" (string_of_uint d)
+ | D8 d => String "8" (string_of_uint d)
+ | D9 d => String "9" (string_of_uint d)
+ end.
+
+Fixpoint uint_of_string s :=
+ match s with
+ | EmptyString => Some Nil
+ | String a s => uint_of_char a (uint_of_string s)
+ end.
+
+Definition string_of_int (d:int) :=
+ match d with
+ | Pos d => string_of_uint d
+ | Neg d => String "-" (string_of_uint d)
+ end.
+
+Definition int_of_string s :=
+ match s with
+ | EmptyString => Some (Pos Nil)
+ | String a s' =>
+ if ascii_dec a "-" then option_map Neg (uint_of_string s')
+ else option_map Pos (uint_of_string s)
+ end.
+
+(* NB: For the moment whitespace between - and digits are not accepted.
+ And in this variant [int_of_string "-" = Some (Neg Nil)].
+
+Compute int_of_string "-123456890123456890123456890123456890".
+Compute string_of_int (-123456890123456890123456890123456890).
+*)
+
+(** Corresponding proofs *)
+
+Lemma usu d :
+ uint_of_string (string_of_uint d) = Some d.
+Proof.
+ induction d; simpl; rewrite ?IHd; simpl; auto.
+Qed.
+
+Lemma sus s d :
+ uint_of_string s = Some d -> string_of_uint d = s.
+Proof.
+ revert d.
+ induction s; simpl.
+ - now intros d [= <-].
+ - intros d.
+ destruct (uint_of_string s); [intros H | intros [=]].
+ apply uint_of_char_spec in H.
+ intuition subst; simpl; f_equal; auto.
+Qed.
+
+Lemma isi d : int_of_string (string_of_int d) = Some d.
+Proof.
+ destruct d; simpl.
+ - unfold int_of_string.
+ destruct (string_of_uint d) eqn:Hd.
+ + now destruct d.
+ + destruct ascii_dec; subst.
+ * now destruct d.
+ * rewrite <- Hd, usu; auto.
+ - rewrite usu; auto.
+Qed.
+
+Lemma sis s d :
+ int_of_string s = Some d -> string_of_int d = s.
+Proof.
+ destruct s; [intros [= <-]| ]; simpl; trivial.
+ destruct ascii_dec; subst; simpl.
+ - destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
+ simpl; f_equal. now apply sus.
+ - destruct d; [ | now destruct uint_of_char].
+ simpl string_of_int.
+ intros. apply sus; simpl.
+ destruct uint_of_char; simpl in *; congruence.
+Qed.
+
+End NilEmpty.
+
+(** Decimal/String conversions where [Nil] is ["0"] *)
+
+Module NilZero.
+
+Definition string_of_uint (d:uint) :=
+ match d with
+ | Nil => "0"
+ | _ => NilEmpty.string_of_uint d
+ end.
+
+Definition uint_of_string s :=
+ match s with
+ | EmptyString => None
+ | _ => NilEmpty.uint_of_string s
+ end.
+
+Definition string_of_int (d:int) :=
+ match d with
+ | Pos d => string_of_uint d
+ | Neg d => String "-" (string_of_uint d)
+ end.
+
+Definition int_of_string s :=
+ match s with
+ | EmptyString => None
+ | String a s' =>
+ if ascii_dec a "-" then option_map Neg (uint_of_string s')
+ else option_map Pos (uint_of_string s)
+ end.
+
+(** Corresponding proofs *)
+
+Lemma uint_of_string_nonnil s : uint_of_string s <> Some Nil.
+Proof.
+ destruct s; simpl.
+ - easy.
+ - destruct (NilEmpty.uint_of_string s); [intros H | intros [=]].
+ apply uint_of_char_spec in H.
+ now intuition subst.
+Qed.
+
+Lemma sus s d :
+ uint_of_string s = Some d -> string_of_uint d = s.
+Proof.
+ destruct s; [intros [=] | intros H].
+ apply NilEmpty.sus in H. now destruct d.
+Qed.
+
+Lemma usu d :
+ d<>Nil -> uint_of_string (string_of_uint d) = Some d.
+Proof.
+ destruct d; (now destruct 1) || (intros _; apply NilEmpty.usu).
+Qed.
+
+Lemma usu_nil :
+ uint_of_string (string_of_uint Nil) = Some Decimal.zero.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma usu_gen d :
+ uint_of_string (string_of_uint d) = Some d \/
+ uint_of_string (string_of_uint d) = Some Decimal.zero.
+Proof.
+ destruct d; (now right) || (left; now apply usu).
+Qed.
+
+Lemma isi d :
+ d<>Pos Nil -> d<>Neg Nil ->
+ int_of_string (string_of_int d) = Some d.
+Proof.
+ destruct d; simpl.
+ - intros H _.
+ unfold int_of_string.
+ destruct (string_of_uint d) eqn:Hd.
+ + now destruct d.
+ + destruct ascii_dec; subst.
+ * now destruct d.
+ * rewrite <- Hd, usu; auto. now intros ->.
+ - intros _ H.
+ rewrite usu; auto. now intros ->.
+Qed.
+
+Lemma isi_posnil :
+ int_of_string (string_of_int (Pos Nil)) = Some (Pos Decimal.zero).
+Proof.
+ reflexivity.
+Qed.
+
+(** Warning! (-0) won't parse (compatibility with the behavior of Z). *)
+
+Lemma isi_negnil :
+ int_of_string (string_of_int (Neg Nil)) = Some (Neg (D0 Nil)).
+Proof.
+ reflexivity.
+Qed.
+
+Lemma sis s d :
+ int_of_string s = Some d -> string_of_int d = s.
+Proof.
+ destruct s; [intros [=]| ]; simpl.
+ destruct ascii_dec; subst; simpl.
+ - destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
+ simpl; f_equal. now apply sus.
+ - destruct d; [ | now destruct uint_of_char].
+ simpl string_of_int.
+ intros. apply sus; simpl.
+ destruct uint_of_char; simpl in *; congruence.
+Qed.
+
+End NilZero.
--
cgit v1.2.3
From db77b92f7cc426aa9fb784be3b07b4097d81ae0d Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 31 May 2017 01:23:50 -0400
Subject: Doc: add Decimal-related files to index-list.html.template
---
doc/stdlib/index-list.html.template | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 48048b7a0..95e541f81 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -18,6 +18,7 @@ through the Require Import command.
theories/Init/Logic.v
theories/Init/Logic_Type.v
theories/Init/Nat.v
+ theories/Init/Decimal.v
theories/Init/Peano.v
theories/Init/Specif.v
theories/Init/Tactics.v
@@ -225,6 +226,12 @@ through the Require Import command.
theories/Numbers/BinNums.v
theories/Numbers/NumPrelude.v
theories/Numbers/NaryFunctions.v
+ theories/Numbers/DecimalFacts.v
+ theories/Numbers/DecimalNat.v
+ theories/Numbers/DecimalPos.v
+ theories/Numbers/DecimalN.v
+ theories/Numbers/DecimalZ.v
+ theories/Numbers/DecimalString.v
NatInt:
--
cgit v1.2.3
From 2fb9e915a8095701c3758cba0d6238b4db8212fa Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 1 Jun 2017 14:36:09 -0400
Subject: Update SearchPattern.out for numeral notations
There is more churn than there should be because SearchPattern uses a
non-local sorting algorithm; the comparison function considers many
constants equal in priority and leaves it up to the heap structure to
break ties, which seems wrong. This has been reported as
[bug #5573](https://coq.inria.fr/bugs/show_bug.cgi?id=5573).
---
test-suite/output/SearchPattern.out | 43 ++++++++++++++++++++++---------------
1 file changed, 26 insertions(+), 17 deletions(-)
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 45ff5e73b..b0ac9ea29 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -12,32 +12,37 @@ Nat.ltb: nat -> nat -> bool
Nat.testbit: nat -> nat -> bool
Nat.eqb: nat -> nat -> bool
Nat.two: nat
-Nat.zero: nat
Nat.one: nat
+Nat.zero: nat
O: nat
-Nat.double: nat -> nat
-Nat.sqrt: nat -> nat
Nat.div2: nat -> nat
Nat.log2: nat -> nat
+Nat.succ: nat -> nat
+Nat.sqrt: nat -> nat
Nat.pred: nat -> nat
+Nat.double: nat -> nat
Nat.square: nat -> nat
S: nat -> nat
-Nat.succ: nat -> nat
Nat.ldiff: nat -> nat -> nat
-Nat.add: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
-Nat.lxor: nat -> nat -> nat
+Nat.tail_add: nat -> nat -> nat
Nat.land: nat -> nat -> nat
-Nat.mul: nat -> nat -> nat
-Nat.sub: nat -> nat -> nat
-Nat.max: nat -> nat -> nat
+Nat.tail_mul: nat -> nat -> nat
Nat.div: nat -> nat -> nat
-Nat.pow: nat -> nat -> nat
-Nat.min: nat -> nat -> nat
-Nat.modulo: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
Nat.gcd: nat -> nat -> nat
-Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
+Nat.modulo: nat -> nat -> nat
+Nat.max: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
+Nat.mul: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
+Nat.min: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
+Nat.of_uint: Decimal.uint -> nat
+Nat.tail_addmul: nat -> nat -> nat -> nat
+Nat.of_uint_acc: Decimal.uint -> nat -> nat
Nat.log2_iter: nat -> nat -> nat -> nat -> nat
+Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
length: forall A : Type, list A -> nat
Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
Nat.div2: nat -> nat
@@ -53,14 +58,18 @@ Nat.pow: nat -> nat -> nat
Nat.land: nat -> nat -> nat
Nat.lxor: nat -> nat -> nat
Nat.div: nat -> nat -> nat
-Nat.mul: nat -> nat -> nat
-Nat.min: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.tail_mul: nat -> nat -> nat
Nat.modulo: nat -> nat -> nat
Nat.sub: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
+Nat.mul: nat -> nat -> nat
Nat.gcd: nat -> nat -> nat
Nat.max: nat -> nat -> nat
+Nat.tail_add: nat -> nat -> nat
Nat.add: nat -> nat -> nat
+Nat.min: nat -> nat -> nat
+Nat.tail_addmul: nat -> nat -> nat -> nat
+Nat.of_uint_acc: Decimal.uint -> nat -> nat
Nat.log2_iter: nat -> nat -> nat -> nat -> nat
Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
--
cgit v1.2.3
From 63da69cff704be2da61f3cd311fa7a67dca6fc51 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 16 Jan 2018 12:18:36 -0500
Subject: Add CHANGES entry for decimals in prelude
---
CHANGES | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/CHANGES b/CHANGES
index 8d344d4f0..05337dc6c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -89,6 +89,15 @@ Documentation
moved to the GitHub wiki section of this repository; the main entry
page is https://github.com/coq/coq/wiki/The-Coq-FAQ.
+Standard Library
+
+- New libraries Coq.Init.Decimal, Coq.Numbers.DecimalFacts,
+ Coq.Numbers.DecimalNat, Coq.Numbers.DecimalPos,
+ Coq.Numbers.DecimalN, Coq.Numbers.DecimalZ,
+ Coq.Numbers.DecimalString providing a type of decimal numbers, some
+ facts about them, and conversions between decimal numbers and nat,
+ positive, N, Z, and string.
+
Changes from 8.7.1 to 8.7.2
===========================
--
cgit v1.2.3