Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

DecimalPos

Proofs that conversions between decimal numbers and positive are bijections.

Require Import Decimal DecimalFacts PArith NArith.

Module Unsigned.

Local Open Scope N.

A direct version of of_little_uint

Fixpoint of_lu (d:uint) : N :=
  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.

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)).d:uint
of_lu d = hd d + 10 * of_lu (tl d)
Proof.d:uint
of_lu d = hd d + 10 * of_lu (tl d)
 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.d, d':uint
of_lu (revapp d d') =
of_lu (rev d) + of_lu d' * 10 ^ usize d
Proof.d, d':uint
of_lu (revapp d d') =
of_lu (rev d) + of_lu d' * 10 ^ usize d
 revert d'.d:uint
forall d' : uint,
of_lu (revapp d d') =
of_lu (rev d) + of_lu d' * 10 ^ usize 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.n:N
p, q:positive
N.pos (Nadd n (p * q)) = n + N.pos p * N.pos q
Proof.n:N
p, q:positive
N.pos (Nadd n (p * q)) = n + N.pos p * N.pos q
 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)).d:uint
acc:positive
d <> Nil ->
Pos.of_uint_acc d acc =
Pos.of_uint_acc (tl d) (Nadd (hd d) (10 * acc))
Proof.d:uint
acc:positive
d <> Nil ->
Pos.of_uint_acc d acc =
Pos.of_uint_acc (tl d) (Nadd (hd d) (10 * acc))
 destruct d; simpl; trivial.acc:positive
Nil <> Nil -> acc = ((acc + acc~0~0)~0)%positive 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.d:uint
acc:positive
N.pos (Pos.of_uint_acc d acc) =
of_lu (rev d) + N.pos acc * 10 ^ usize d
Proof.d:uint
acc:positive
N.pos (Pos.of_uint_acc d acc) =
of_lu (rev d) + N.pos acc * 10 ^ usize d
 revert acc.d:uint
forall acc : positive,
N.pos (Pos.of_uint_acc d acc) =
of_lu (rev d) + N.pos acc * 10 ^ usize d
 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).d:uint
Pos.of_uint d = of_lu (rev d)
Proof.d:uint
Pos.of_uint d = of_lu (rev d)
 induction d; simpl; trivial; unfold rev; simpl revapp;
 rewrite of_lu_revapp; simpl of_lu; try apply of_uint_acc_rev.d:uint
IHd:Pos.of_uint d = of_lu (rev d)
Pos.of_uint d = of_lu (rev d) + 0 * 10 ^ usize d
 rewrite IHd.d:uint
IHd:Pos.of_uint d = of_lu (rev d)
of_lu (rev d) = of_lu (rev d) + 0 * 10 ^ usize d ring.
Qed.

Lemma of_lu_rev d : Pos.of_uint (rev d) = of_lu d.d:uint
Pos.of_uint (rev d) = of_lu d
Proof.d:uint
Pos.of_uint (rev d) = of_lu d
 rewrite of_uint_alt.d:uint
of_lu (rev (rev d)) = of_lu d 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).d:uint
of_lu (Little.double d) = N.double (of_lu d) /\
of_lu (Little.succ_double d) = N.succ_double (of_lu d)
Proof.d:uint
of_lu (Little.double d) = N.double (of_lu d) /\
of_lu (Little.succ_double d) = N.succ_double (of_lu d)
 rewrite N.double_spec, N.succ_double_spec.d:uint
of_lu (Little.double d) = 2 * of_lu d /\
of_lu (Little.succ_double d) = 2 * of_lu d + 1
 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).d:uint
of_lu (Little.double d) = N.double (of_lu d)
Proof.d:uint
of_lu (Little.double d) = N.double (of_lu d)
 apply of_lu_double_gen.
Qed.

Lemma of_lu_succ_double d :
  of_lu (Little.succ_double d) = N.succ_double (of_lu d).d:uint
of_lu (Little.succ_double d) = N.succ_double (of_lu d)
Proof.d:uint
of_lu (Little.succ_double d) = N.succ_double (of_lu d)
 apply of_lu_double_gen.
Qed.

First bijection result

Lemma of_to (p:positive) : Pos.of_uint (Pos.to_uint p) = Npos p.p:positive
Pos.of_uint (Pos.to_uint p) = N.pos p
Proof.p:positive
Pos.of_uint (Pos.to_uint p) = N.pos p
 unfold Pos.to_uint.p:positive
Pos.of_uint (rev (Pos.to_little_uint p)) = N.pos p
 rewrite of_lu_rev.p:positive
of_lu (Pos.to_little_uint p) = N.pos p
 induction p; simpl; trivial.p:positive
IHp:of_lu (Pos.to_little_uint p) = N.pos p
of_lu (Little.succ_double (Pos.to_little_uint p)) =
N.pos p~1
p:positive
IHp:of_lu (Pos.to_little_uint p) = N.pos p
of_lu (Little.double (Pos.to_little_uint p)) =
N.pos p~0
 -p:positive
IHp:of_lu (Pos.to_little_uint p) = N.pos p
of_lu (Little.succ_double (Pos.to_little_uint p)) =
N.pos p~1 now rewrite of_lu_succ_double, IHp.
 -p:positive
IHp:of_lu (Pos.to_little_uint p) = N.pos p
of_lu (Little.double (Pos.to_little_uint p)) =
N.pos p~0 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).d:uint
Little.succ_double d = Little.succ (Little.double d)
Proof.d:uint
Little.succ_double d = Little.succ (Little.double d)
 now induction d.
Qed.

Lemma double_succ d :
  Little.double (Little.succ d) =
  Little.succ (Little.succ_double d).d:uint
Little.double (Little.succ d) =
Little.succ (Little.succ_double d)
Proof.d:uint
Little.double (Little.succ d) =
Little.succ (Little.succ_double d)
 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).n:N
to_lu (N.succ n) = Little.succ (to_lu n)
Proof.n:N
to_lu (N.succ n) = Little.succ (to_lu n)
 destruct n; simpl; trivial.p:positive
Pos.to_little_uint (Pos.succ p) =
Little.succ (Pos.to_little_uint p)
 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).n:nat
A:Type
f:A -> A
i:A
Nat.iter (S n) f i = f (Nat.iter n f i)
Proof.n:nat
A:Type
f:A -> A
i:A
Nat.iter (S n) f i = f (Nat.iter n f i)
 reflexivity.
Qed.

Lemma nat_iter_0 {A} (f:A->A) i : Nat.iter 0 f i = i.A:Type
f:A -> A
i:A
Nat.iter 0 f i = i
Proof.A:Type
f:A -> A
i:A
Nat.iter 0 f i = i
 reflexivity.
Qed.

Lemma to_ldec_tenfold p :
 to_lu (10 * Npos p) = D0 (to_lu (Npos p)).p:positive
to_lu (10 * N.pos p) = D0 (to_lu (N.pos p))
Proof.p:positive
to_lu (10 * N.pos p) = D0 (to_lu (N.pos p))
 induction p using Pos.peano_rect.to_lu (10 * 1) = D0 (to_lu 1)
p:positive
IHp:to_lu (10 * N.pos p) = D0 (to_lu (N.pos p))
to_lu (10 * N.pos (Pos.succ p)) =
D0 (to_lu (N.pos (Pos.succ p)))
 -to_lu (10 * 1) = D0 (to_lu 1) trivial.
 -p:positive
IHp:to_lu (10 * N.pos p) = D0 (to_lu (N.pos p))
to_lu (10 * N.pos (Pos.succ p)) =
D0 (to_lu (N.pos (Pos.succ p))) change (N.pos (Pos.succ p)) with (N.succ (N.pos p)).p:positive
IHp:to_lu (10 * N.pos p) = D0 (to_lu (N.pos p))
to_lu (10 * N.succ (N.pos p)) =
D0 (to_lu (N.succ (N.pos p)))
   rewrite N.mul_succ_r.p:positive
IHp:to_lu (10 * N.pos p) = D0 (to_lu (N.pos p))
to_lu (10 * N.pos p + 10) =
D0 (to_lu (N.succ (N.pos p)))
   change 10 at 2 with (Nat.iter 10%nat N.succ 0).p:positive
IHp:to_lu (10 * N.pos p) = D0 (to_lu (N.pos p))
to_lu (10 * N.pos p + Nat.iter 10 N.succ 0) =
D0 (to_lu (N.succ (N.pos p)))
   rewrite ?nat_iter_S, nat_iter_0.p:positive
IHp:to_lu (10 * N.pos p) = D0 (to_lu (N.pos p))
to_lu
  (10 * N.pos p +
   N.succ
     (N.succ
        (N.succ
           (N.succ
              (N.succ
                 (N.succ
                    (N.succ
                       (N.succ (N.succ (N.succ 0)))))))))) =
D0 (to_lu (N.succ (N.pos p)))
   rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp.p:positive
IHp:to_lu (10 * N.pos p) = D0 (to_lu (N.pos p))
Little.succ
  (Little.succ
     (Little.succ
        (Little.succ
           (Little.succ
              (Little.succ
                 (Little.succ
                    (Little.succ
                       (Little.succ
                          (Little.succ
                             (D0 (to_lu (N.pos p)))))))))))) =
D0 (Little.succ (to_lu (N.pos p)))
   destruct (to_lu (N.pos p)); simpl; auto.
Qed.

Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil.d:uint
of_lu d = 0 <-> nztail d = Nil
Proof.d:uint
of_lu d = 0 <-> nztail d = Nil
 induction d; try simpl_of_lu; split; trivial; try discriminate;
 try (intros H; now apply N.eq_add_0 in H).d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
0 + 10 * of_lu d = 0 -> nztail (D0 d) = Nil
d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
nztail (D0 d) = Nil -> 0 + 10 * of_lu d = 0
 -d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
0 + 10 * of_lu d = 0 -> nztail (D0 d) = Nil rewrite N.add_0_l.d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
10 * of_lu d = 0 -> nztail (D0 d) = Nil intros H.d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
H:10 * of_lu d = 0
nztail (D0 d) = Nil
   apply N.eq_mul_0_r in H; [|easy].d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
H:of_lu d = 0
nztail (D0 d) = Nil rewrite IHd in H.d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
H:nztail d = Nil
nztail (D0 d) = Nil
   simpl.d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
H:nztail d = Nil
match nztail d with
| Nil => Nil
| D0 u => D0 (D0 u)
| D1 u => D0 (D1 u)
| D2 u => D0 (D2 u)
| D3 u => D0 (D3 u)
| D4 u => D0 (D4 u)
| D5 u => D0 (D5 u)
| D6 u => D0 (D6 u)
| D7 u => D0 (D7 u)
| D8 u => D0 (D8 u)
| D9 u => D0 (D9 u)
end = Nil now rewrite H.
 -d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
nztail (D0 d) = Nil -> 0 + 10 * of_lu d = 0 simpl.d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
match nztail d with
| Nil => Nil
| D0 u => D0 (D0 u)
| D1 u => D0 (D1 u)
| D2 u => D0 (D2 u)
| D3 u => D0 (D3 u)
| D4 u => D0 (D4 u)
| D5 u => D0 (D5 u)
| D6 u => D0 (D6 u)
| D7 u => D0 (D7 u)
| D8 u => D0 (D8 u)
| D9 u => D0 (D9 u)
end = Nil ->
match of_lu d with
| 0 => 0
| N.pos q => N.pos (q + q~0~0)~0
end = 0 destruct (nztail d); try discriminate.d:uint
IHd:of_lu d = 0 <-> Nil = Nil
Nil = Nil ->
match of_lu d with
| 0 => 0
| N.pos q => N.pos (q + q~0~0)~0
end = 0
   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).d:uint
to_lu (of_lu d) = lnorm d ->
to_lu (10 * of_lu d) = lnorm (D0 d)
Proof.d:uint
to_lu (of_lu d) = lnorm d ->
to_lu (10 * of_lu d) = lnorm (D0 d)
 intro IH.d:uint
IH:to_lu (of_lu d) = lnorm d
to_lu (10 * of_lu d) = lnorm (D0 d)
 destruct (N.eq_dec (of_lu d) 0) as [H|H].d:uint
IH:to_lu (of_lu d) = lnorm d
H:of_lu d = 0
to_lu (10 * of_lu d) = lnorm (D0 d)
d:uint
IH:to_lu (of_lu d) = lnorm d
H:of_lu d <> 0
to_lu (10 * of_lu d) = lnorm (D0 d)
 -d:uint
IH:to_lu (of_lu d) = lnorm d
H:of_lu d = 0
to_lu (10 * of_lu d) = lnorm (D0 d) rewrite H.d:uint
IH:to_lu (of_lu d) = lnorm d
H:of_lu d = 0
to_lu (10 * 0) = lnorm (D0 d) simpl.d:uint
IH:to_lu (of_lu d) = lnorm d
H:of_lu d = 0
0%uint = lnorm (D0 d) rewrite of_lu_0 in H.d:uint
IH:to_lu (of_lu d) = lnorm d
H:nztail d = Nil
0%uint = lnorm (D0 d)
   unfold lnorm.d:uint
IH:to_lu (of_lu d) = lnorm d
H:nztail d = Nil
0%uint =
match nztail (D0 d) with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end simpl.d:uint
IH:to_lu (of_lu d) = lnorm d
H:nztail d = Nil
0%uint =
match
  match nztail d with
  | Nil => Nil
  | D0 u => D0 (D0 u)
  | D1 u => D0 (D1 u)
  | D2 u => D0 (D2 u)
  | D3 u => D0 (D3 u)
  | D4 u => D0 (D4 u)
  | D5 u => D0 (D5 u)
  | D6 u => D0 (D6 u)
  | D7 u => D0 (D7 u)
  | D8 u => D0 (D8 u)
  | D9 u => D0 (D9 u)
  end
with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end now rewrite H.
 -d:uint
IH:to_lu (of_lu d) = lnorm d
H:of_lu d <> 0
to_lu (10 * of_lu d) = lnorm (D0 d) destruct (of_lu d) eqn:Eq; [easy| ].d:uint
p:positive
Eq:of_lu d = N.pos p
IH:to_lu (N.pos p) = lnorm d
H:N.pos p <> 0
to_lu (10 * N.pos p) = lnorm (D0 d)
   rewrite to_ldec_tenfold; auto.d:uint
p:positive
Eq:of_lu d = N.pos p
IH:to_lu (N.pos p) = lnorm d
H:N.pos p <> 0
D0 (to_lu (N.pos p)) = lnorm (D0 d) rewrite IH.d:uint
p:positive
Eq:of_lu d = N.pos p
IH:to_lu (N.pos p) = lnorm d
H:N.pos p <> 0
D0 (lnorm d) = lnorm (D0 d)
   rewrite <- Eq in H.d:uint
p:positive
Eq:of_lu d = N.pos p
IH:to_lu (N.pos p) = lnorm d
H:of_lu d <> 0
D0 (lnorm d) = lnorm (D0 d) rewrite of_lu_0 in H.d:uint
p:positive
Eq:of_lu d = N.pos p
IH:to_lu (N.pos p) = lnorm d
H:nztail d <> Nil
D0 (lnorm d) = lnorm (D0 d)
   unfold lnorm.d:uint
p:positive
Eq:of_lu d = N.pos p
IH:to_lu (N.pos p) = lnorm d
H:nztail d <> Nil
D0
  match nztail d with
  | Nil => 0
  | D0 u => D0 u
  | D1 u => D1 u
  | D2 u => D2 u
  | D3 u => D3 u
  | D4 u => D4 u
  | D5 u => D5 u
  | D6 u => D6 u
  | D7 u => D7 u
  | D8 u => D8 u
  | D9 u => D9 u
  end =
match nztail (D0 d) with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end simpl.d:uint
p:positive
Eq:of_lu d = N.pos p
IH:to_lu (N.pos p) = lnorm d
H:nztail d <> Nil
D0
  match nztail d with
  | Nil => 0
  | D0 u => D0 u
  | D1 u => D1 u
  | D2 u => D2 u
  | D3 u => D3 u
  | D4 u => D4 u
  | D5 u => D5 u
  | D6 u => D6 u
  | D7 u => D7 u
  | D8 u => D8 u
  | D9 u => D9 u
  end =
match
  match nztail d with
  | Nil => Nil
  | D0 u => D0 (D0 u)
  | D1 u => D0 (D1 u)
  | D2 u => D0 (D2 u)
  | D3 u => D0 (D3 u)
  | D4 u => D0 (D4 u)
  | D5 u => D0 (D5 u)
  | D6 u => D0 (D6 u)
  | D7 u => D0 (D7 u)
  | D8 u => D0 (D8 u)
  | D9 u => D0 (D9 u)
  end
with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end now destruct (nztail d).
Qed.

Lemma Nadd_alt n m : n + m = Nat.iter (N.to_nat n) N.succ m.n, m:N
n + m = Nat.iter (N.to_nat n) N.succ m
Proof.n, m:N
n + m = Nat.iter (N.to_nat n) N.succ m
 destruct n.m:N
0 + m = Nat.iter (N.to_nat 0) N.succ m
p:positive
m:N
N.pos p + m = Nat.iter (N.to_nat (N.pos p)) N.succ m trivial.p:positive
m:N
N.pos p + m = Nat.iter (N.to_nat (N.pos p)) N.succ m
 induction p using Pos.peano_rect.m:N
1 + m = Nat.iter (N.to_nat 1) N.succ m
p:positive
m:N
IHp:N.pos p + m = Nat.iter (N.to_nat (N.pos p)) N.succ m
N.pos (Pos.succ p) + m =
Nat.iter (N.to_nat (N.pos (Pos.succ p))) N.succ m
 -m:N
1 + m = Nat.iter (N.to_nat 1) N.succ m now rewrite N.add_1_l.
 -p:positive
m:N
IHp:N.pos p + m = Nat.iter (N.to_nat (N.pos p)) N.succ m
N.pos (Pos.succ p) + m =
Nat.iter (N.to_nat (N.pos (Pos.succ p))) N.succ m change (N.pos (Pos.succ p)) with (N.succ (N.pos p)).p:positive
m:N
IHp:N.pos p + m = Nat.iter (N.to_nat (N.pos p)) N.succ m
N.succ (N.pos p) + m =
Nat.iter (N.to_nat (N.succ (N.pos p))) N.succ m
   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.d:uint
to_lu (of_lu d) = lnorm d
Proof.d:uint
to_lu (of_lu d) = lnorm d
 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.d:uint
N.to_uint (Pos.of_uint d) = unorm d
Proof.d:uint
N.to_uint (Pos.of_uint d) = unorm d
 rewrite of_uint_alt.d:uint
N.to_uint (of_lu (rev d)) = unorm d
 unfold N.to_uint, Pos.to_uint.d:uint
match of_lu (rev d) with
| 0 => 0%uint
| N.pos p => rev (Pos.to_little_uint p)
end = unorm d
 destruct (of_lu (rev d)) eqn:H.d:uint
H:of_lu (rev d) = 0
0%uint = unorm d
d:uint
p:positive
H:of_lu (rev d) = N.pos p
rev (Pos.to_little_uint p) = unorm d
 -d:uint
H:of_lu (rev d) = 0
0%uint = unorm d rewrite of_lu_0 in H.d:uint
H:nztail (rev d) = Nil
0%uint = unorm d rewrite <- rev_lnorm_rev.d:uint
H:nztail (rev d) = Nil
0%uint = rev (lnorm (rev d))
   unfold lnorm.d:uint
H:nztail (rev d) = Nil
0%uint =
rev
  match nztail (rev d) with
  | Nil => 0
  | D0 u => D0 u
  | D1 u => D1 u
  | D2 u => D2 u
  | D3 u => D3 u
  | D4 u => D4 u
  | D5 u => D5 u
  | D6 u => D6 u
  | D7 u => D7 u
  | D8 u => D8 u
  | D9 u => D9 u
  end now rewrite H.
 -d:uint
p:positive
H:of_lu (rev d) = N.pos p
rev (Pos.to_little_uint p) = unorm d change (Pos.to_little_uint p) with (to_lu (N.pos p)).d:uint
p:positive
H:of_lu (rev d) = N.pos p
rev (to_lu (N.pos p)) = unorm d
   rewrite <- H.d:uint
p:positive
H:of_lu (rev d) = N.pos p
rev (to_lu (of_lu (rev d))) = unorm d rewrite to_of_lu.d:uint
p:positive
H:of_lu (rev d) = N.pos p
rev (lnorm (rev d)) = unorm d apply rev_lnorm_rev.
Qed.

Some consequences

Lemma to_uint_nonzero p : Pos.to_uint p <> zero.p:positive
Pos.to_uint p <> 0%uint
Proof.p:positive
Pos.to_uint p <> 0%uint
 intro E.p:positive
E:Pos.to_uint p = 0%uint
False generalize (of_to p).p:positive
E:Pos.to_uint p = 0%uint
Pos.of_uint (Pos.to_uint p) = N.pos p -> False now rewrite E.
Qed.

Lemma to_uint_nonnil p : Pos.to_uint p <> Nil.p:positive
Pos.to_uint p <> Nil
Proof.p:positive
Pos.to_uint p <> Nil
 intros E.p:positive
E:Pos.to_uint p = Nil
False generalize (of_to p).p:positive
E:Pos.to_uint p = Nil
Pos.of_uint (Pos.to_uint p) = N.pos p -> False now rewrite E.
Qed.

Lemma to_uint_inj p p' : Pos.to_uint p = Pos.to_uint p' -> p = p'.p, p':positive
Pos.to_uint p = Pos.to_uint p' -> p = p'
Proof.p, p':positive
Pos.to_uint p = Pos.to_uint p' -> p = p'
 intro E.p, p':positive
E:Pos.to_uint p = Pos.to_uint p'
p = p'
 assert (E' : N.pos p = N.pos p').p, p':positive
E:Pos.to_uint p = Pos.to_uint p'
N.pos p = N.pos p'
p, p':positive
E:Pos.to_uint p = Pos.to_uint p'
E':N.pos p = N.pos p'
p = p'
 {p, p':positive
E:Pos.to_uint p = Pos.to_uint p'
N.pos p = N.pos p' now rewrite <- (of_to p), <- (of_to p'), E. }p, p':positive
E:Pos.to_uint p = Pos.to_uint p'
E':N.pos p = N.pos p'
p = p'
 now injection E'.
Qed.

Lemma to_uint_pos_surj d :
 unorm d<>zero -> exists p, Pos.to_uint p = unorm d.d:uint
unorm d <> 0%uint ->
exists p : positive, Pos.to_uint p = unorm d
Proof.d:uint
unorm d <> 0%uint ->
exists p : positive, Pos.to_uint p = unorm d
 intros.d:uint
H:unorm d <> 0%uint
exists p : positive, Pos.to_uint p = unorm d
 destruct (Pos.of_uint d) eqn:E.d:uint
H:unorm d <> 0%uint
E:Pos.of_uint d = 0
exists p : positive, Pos.to_uint p = unorm d
d:uint
H:unorm d <> 0%uint
p:positive
E:Pos.of_uint d = N.pos p
exists p0 : positive, Pos.to_uint p0 = unorm d
 -d:uint
H:unorm d <> 0%uint
E:Pos.of_uint d = 0
exists p : positive, Pos.to_uint p = unorm d destruct H.d:uint
E:Pos.of_uint d = 0
unorm d = 0%uint generalize (to_of d).d:uint
E:Pos.of_uint d = 0
N.to_uint (Pos.of_uint d) = unorm d ->
unorm d = 0%uint now rewrite E.
 -d:uint
H:unorm d <> 0%uint
p:positive
E:Pos.of_uint d = N.pos p
exists p0 : positive, Pos.to_uint p0 = unorm d exists p.d:uint
H:unorm d <> 0%uint
p:positive
E:Pos.of_uint d = N.pos p
Pos.to_uint p = unorm d generalize (to_of d).d:uint
H:unorm d <> 0%uint
p:positive
E:Pos.of_uint d = N.pos p
N.to_uint (Pos.of_uint d) = unorm d ->
Pos.to_uint p = unorm d now rewrite E.
Qed.

Lemma of_uint_norm d : Pos.of_uint (unorm d) = Pos.of_uint d.d:uint
Pos.of_uint (unorm d) = Pos.of_uint d
Proof.d:uint
Pos.of_uint (unorm d) = Pos.of_uint d
 now induction d.
Qed.

Lemma of_inj d d' :
 Pos.of_uint d = Pos.of_uint d' -> unorm d = unorm d'.d, d':uint
Pos.of_uint d = Pos.of_uint d' -> unorm d = unorm d'
Proof.d, d':uint
Pos.of_uint d = Pos.of_uint d' -> unorm d = unorm d'
 intros.d, d':uint
H:Pos.of_uint d = Pos.of_uint d'
unorm d = unorm d' rewrite <- !to_of.d, d':uint
H:Pos.of_uint d = Pos.of_uint d'
N.to_uint (Pos.of_uint d) = N.to_uint (Pos.of_uint d') now f_equal.
Qed.

Lemma of_iff d d' : Pos.of_uint d = Pos.of_uint d' <-> unorm d = unorm d'.d, d':uint
Pos.of_uint d = Pos.of_uint d' <-> unorm d = unorm d'
Proof.d, d':uint
Pos.of_uint d = Pos.of_uint d' <-> unorm d = unorm d'
 split.d, d':uint
Pos.of_uint d = Pos.of_uint d' -> unorm d = unorm d'
d, d':uint
unorm d = unorm d' -> Pos.of_uint d = Pos.of_uint d' apply of_inj.d, d':uint
unorm d = unorm d' -> Pos.of_uint d = Pos.of_uint d' intros E.d, d':uint
E:unorm d = unorm d'
Pos.of_uint d = Pos.of_uint d' rewrite <- of_uint_norm, E.d, d':uint
E:unorm d = unorm d'
Pos.of_uint (unorm d') = Pos.of_uint d'
 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.p:positive
Pos.of_int (Pos.to_int p) = Some p
Proof.p:positive
Pos.of_int (Pos.to_int p) = Some p
 unfold Pos.to_int, Pos.of_int, norm.p:positive
match Pos.of_uint (Pos.to_uint p) with
| 0%N => None
| N.pos p0 => Some p0
end = Some p
 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.d:int
p:positive
Pos.of_int d = Some p -> Pos.to_int p = norm d
Proof.d:int
p:positive
Pos.of_int d = Some p -> Pos.to_int p = norm d
 unfold Pos.of_int.d:int
p:positive
match d with
| Pos d0 =>
    match Pos.of_uint d0 with
    | 0%N => None
    | N.pos p0 => Some p0
    end
| Neg _ => None
end = Some p -> Pos.to_int p = norm d
 destruct d; [ | intros [=]].d:uint
p:positive
match Pos.of_uint d with
| 0%N => None
| N.pos p0 => Some p0
end = Some p -> Pos.to_int p = norm (Pos d)
 simpl norm.d:uint
p:positive
match Pos.of_uint d with
| 0%N => None
| N.pos p0 => Some p0
end = Some p -> Pos.to_int p = Pos (unorm d) rewrite <- Unsigned.to_of.d:uint
p:positive
match Pos.of_uint d with
| 0%N => None
| N.pos p0 => Some p0
end = Some p ->
Pos.to_int p = Pos (N.to_uint (Pos.of_uint d))
 destruct (Pos.of_uint d); now intros [= <-].
Qed.

Lemma to_int_inj p p' : Pos.to_int p = Pos.to_int p' -> p = p'.p, p':positive
Pos.to_int p = Pos.to_int p' -> p = p'
Proof.p, p':positive
Pos.to_int p = Pos.to_int p' -> p = p'
 intro E.p, p':positive
E:Pos.to_int p = Pos.to_int p'
p = p'
 assert (E' : Some p = Some p').p, p':positive
E:Pos.to_int p = Pos.to_int p'
Some p = Some p'
p, p':positive
E:Pos.to_int p = Pos.to_int p'
E':Some p = Some p'
p = p'
 {p, p':positive
E:Pos.to_int p = Pos.to_int p'
Some p = Some p' now rewrite <- (of_to p), <- (of_to p'), E. }p, p':positive
E:Pos.to_int p = Pos.to_int p'
E':Some p = Some p'
p = p'
 now injection E'.
Qed.

Lemma to_int_pos_surj d :
 unorm d <> zero -> exists p, Pos.to_int p = norm (Pos d).d:uint
unorm d <> 0%uint ->
exists p : positive, Pos.to_int p = norm (Pos d)
Proof.d:uint
unorm d <> 0%uint ->
exists p : positive, Pos.to_int p = norm (Pos d)
 simpl.d:uint
unorm d <> 0%uint ->
exists p : positive, Pos.to_int p = Pos (unorm d) unfold Pos.to_int.d:uint
unorm d <> 0%uint ->
exists p : positive,
  Pos (Pos.to_uint p) = Pos (unorm d) intros H.d:uint
H:unorm d <> 0%uint
exists p : positive,
  Pos (Pos.to_uint p) = Pos (unorm d)
 destruct (Unsigned.to_uint_pos_surj d H) as (p,Hp).d:uint
H:unorm d <> 0%uint
p:positive
Hp:Pos.to_uint p = unorm d
exists p0 : positive,
  Pos (Pos.to_uint p0) = Pos (unorm d)
 exists p.d:uint
H:unorm d <> 0%uint
p:positive
Hp:Pos.to_uint p = unorm d
Pos (Pos.to_uint p) = Pos (unorm d) now f_equal.
Qed.

Lemma of_int_norm d : Pos.of_int (norm d) = Pos.of_int d.d:int
Pos.of_int (norm d) = Pos.of_int d
Proof.d:int
Pos.of_int (norm d) = Pos.of_int d
 unfold Pos.of_int.d:int
match norm d with
| Pos d0 =>
    match Pos.of_uint d0 with
    | 0%N => None
    | N.pos p => Some p
    end
| Neg _ => None
end =
match d with
| Pos d0 =>
    match Pos.of_uint d0 with
    | 0%N => None
    | N.pos p => Some p
    end
| Neg _ => None
end
 destruct d.d:uint
match norm (Pos d) with
| Pos d0 =>
    match Pos.of_uint d0 with
    | 0%N => None
    | N.pos p => Some p
    end
| Neg _ => None
end =
match Pos.of_uint d with
| 0%N => None
| N.pos p => Some p
end
d:uint
match norm (Neg d) with
| Pos d0 =>
    match Pos.of_uint d0 with
    | 0%N => None
    | N.pos p => Some p
    end
| Neg _ => None
end = None
 -d:uint
match norm (Pos d) with
| Pos d0 =>
    match Pos.of_uint d0 with
    | 0%N => None
    | N.pos p => Some p
    end
| Neg _ => None
end =
match Pos.of_uint d with
| 0%N => None
| N.pos p => Some p
end simpl.d:uint
match Pos.of_uint (unorm d) with
| 0%N => None
| N.pos p => Some p
end =
match Pos.of_uint d with
| 0%N => None
| N.pos p => Some p
end now rewrite Unsigned.of_uint_norm.
 -d:uint
match norm (Neg d) with
| Pos d0 =>
    match Pos.of_uint d0 with
    | 0%N => None
    | N.pos p => Some p
    end
| Neg _ => None
end = None simpl.d:uint
match
  match nzhead d with
  | Nil => 0%int
  | D0 u => Neg (D0 u)
  | D1 u => Neg (D1 u)
  | D2 u => Neg (D2 u)
  | D3 u => Neg (D3 u)
  | D4 u => Neg (D4 u)
  | D5 u => Neg (D5 u)
  | D6 u => Neg (D6 u)
  | D7 u => Neg (D7 u)
  | D8 u => Neg (D8 u)
  | D9 u => Neg (D9 u)
  end
with
| Pos d0 =>
    match Pos.of_uint d0 with
    | 0%N => None
    | N.pos p => Some p
    end
| Neg _ => None
end = None 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'.d, d':uint
Pos.of_int (Pos d) = Pos.of_int (Pos d') ->
unorm d = unorm d'
Proof.d, d':uint
Pos.of_int (Pos d) = Pos.of_int (Pos d') ->
unorm d = unorm d'
 unfold Pos.of_int.d, d':uint
match Pos.of_uint d with
| 0%N => None
| N.pos p => Some p
end =
match Pos.of_uint d' with
| 0%N => None
| N.pos p => Some p
end -> unorm d = unorm d'
 destruct (Pos.of_uint d) eqn:Hd, (Pos.of_uint d') eqn:Hd';
  intros [=].d, d':uint
Hd:Pos.of_uint d = 0%N
Hd':Pos.of_uint d' = 0%N
unorm d = unorm d'
d, d':uint
p:positive
Hd:Pos.of_uint d = N.pos p
p0:positive
Hd':Pos.of_uint d' = N.pos p0
H0:p = p0
unorm d = unorm d'
 -d, d':uint
Hd:Pos.of_uint d = 0%N
Hd':Pos.of_uint d' = 0%N
unorm d = unorm d' apply Unsigned.of_inj; now rewrite Hd, Hd'.
 -d, d':uint
p:positive
Hd:Pos.of_uint d = N.pos p
p0:positive
Hd':Pos.of_uint d' = N.pos p0
H0:p = p0
unorm d = unorm d' apply Unsigned.of_inj; rewrite Hd, Hd'; now f_equal.
Qed.

End Signed.