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)         *)
(************************************************************************)

DecimalNat

Proofs that conversions between decimal numbers and nat are bijections.

Require Import Decimal DecimalFacts Arith.

Module Unsigned.

A few helper functions used during proofs

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.

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).n:nat
to_lu (S n) = Little.succ (to_lu n)
Proof.n:nat
to_lu (S n) = Little.succ (to_lu n)
 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).n:nat
d:uint
Nat.to_little_uint n (Little.succ d) =
Little.succ (Nat.to_little_uint n d)
Proof.n:nat
d:uint
Nat.to_little_uint n (Little.succ d) =
Little.succ (Nat.to_little_uint n d)
 revert d; induction n; simpl; trivial.
Qed.

Lemma to_lu_equiv n :
  to_lu n = Nat.to_little_uint n zero.n:nat
to_lu n = Nat.to_little_uint n 0
Proof.n:nat
to_lu n = Nat.to_little_uint n 0
 induction n; simpl; trivial.n:nat
IHn:to_lu n = Nat.to_little_uint n 0
Little.succ (to_lu n) = Nat.to_little_uint n 1
 now rewrite IHn, <- to_little_uint_succ.
Qed.

Lemma to_uint_alt n :
 Nat.to_uint n = rev (to_lu n).n:nat
Nat.to_uint n = rev (to_lu n)
Proof.n:nat
Nat.to_uint n = rev (to_lu n)
 unfold Nat.to_uint.n:nat
rev (Nat.to_little_uint n 0) = rev (to_lu n) f_equal.n:nat
Nat.to_little_uint n 0 = to_lu n symmetry.n:nat
to_lu n = Nat.to_little_uint n 0 apply to_lu_equiv.
Qed.

Properties of of_lu

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.

Lemma of_lu_succ d :
 of_lu (Little.succ d) = S (of_lu d).d:uint
of_lu (Little.succ d) = S (of_lu d)
Proof.d:uint
of_lu (Little.succ d) = S (of_lu d)
 induction d; trivial.d:uint
IHd:of_lu (Little.succ d) = S (of_lu d)
of_lu (Little.succ (D9 d)) = S (of_lu (D9 d))
 simpl_of_lu.d:uint
IHd:of_lu (Little.succ d) = S (of_lu d)
0 + 10 * of_lu (Little.succ d) = S (of_lu (D9 d)) rewrite IHd.d:uint
IHd:of_lu (Little.succ d) = S (of_lu d)
0 + 10 * S (of_lu d) = S (of_lu (D9 d)) simpl_of_lu.d:uint
IHd:of_lu (Little.succ d) = S (of_lu d)
0 + 10 * S (of_lu d) = S (9 + 10 * of_lu d)
 now rewrite Nat.mul_succ_r, <- (Nat.add_comm 10).
Qed.

Lemma of_to_lu n :
 of_lu (to_lu n) = n.n:nat
of_lu (to_lu n) = n
Proof.n:nat
of_lu (to_lu n) = n
 induction n; simpl; trivial.n:nat
IHn:of_lu (to_lu n) = n
of_lu (Little.succ (to_lu n)) = S n rewrite of_lu_succ.n:nat
IHn:of_lu (to_lu n) = n
S (of_lu (to_lu n)) = S n 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.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; 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.n:nat
d:uint
Nat.of_uint_acc d n = of_lu (rev d) + n * 10 ^ usize d
Proof.n:nat
d:uint
Nat.of_uint_acc d n = of_lu (rev d) + n * 10 ^ usize d
 revert n.d:uint
forall n : nat,
Nat.of_uint_acc d n = of_lu (rev d) + n * 10 ^ usize d 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).d:uint
Nat.of_uint d = of_lu (rev d)
Proof.d:uint
Nat.of_uint d = of_lu (rev d)
 unfold Nat.of_uint.d:uint
Nat.of_uint_acc d 0 = of_lu (rev d) now rewrite of_uint_acc_spec.
Qed.

First main bijection result

Lemma of_to (n:nat) : Nat.of_uint (Nat.to_uint n) = n.n:nat
Nat.of_uint (Nat.to_uint n) = n
Proof.n:nat
Nat.of_uint (Nat.to_uint n) = n
 rewrite to_uint_alt, of_uint_alt, rev_rev.n:nat
of_lu (to_lu n) = n apply of_to_lu.
Qed.

The other direction

Lemma to_lu_tenfold n : n<>0 ->
 to_lu (10 * n) = D0 (to_lu n).n:nat
n <> 0 -> to_lu (10 * n) = D0 (to_lu n)
Proof.n:nat
n <> 0 -> to_lu (10 * n) = D0 (to_lu n)
 induction n.0 <> 0 -> to_lu (10 * 0) = D0 (to_lu 0)
n:nat
IHn:n <> 0 -> to_lu (10 * n) = D0 (to_lu n)
S n <> 0 -> to_lu (10 * S n) = D0 (to_lu (S n))
 -0 <> 0 -> to_lu (10 * 0) = D0 (to_lu 0) simpl.0 <> 0 -> 0%uint = 00%uint now destruct 1.
 -n:nat
IHn:n <> 0 -> to_lu (10 * n) = D0 (to_lu n)
S n <> 0 -> to_lu (10 * S n) = D0 (to_lu (S n)) intros _.n:nat
IHn:n <> 0 -> to_lu (10 * n) = D0 (to_lu n)
to_lu (10 * S n) = D0 (to_lu (S n))
   destruct (Nat.eq_dec n 0) as [->|H]; simpl; trivial.n:nat
IHn:n <> 0 -> to_lu (10 * n) = D0 (to_lu n)
H:n <> 0
Little.succ
  (to_lu
     (n +
      S
        (n +
         S
           (n +
            S
              (n + S (n + S (n + S (n + S (n + ...))))))))) =
D0 (Little.succ (to_lu n))
   rewrite !Nat.add_succ_r.n:nat
IHn:n <> 0 -> to_lu (10 * n) = D0 (to_lu n)
H:n <> 0
Little.succ
  (to_lu
     (S
        (S
           (S
              (S (S (S (S (S (S (n + (n + (...))))))))))))) =
D0 (Little.succ (to_lu n))
   simpl in *.n:nat
IHn:n <> 0 ->
to_lu (n + (n + (n + (n + (n + (n + (n + (n + (n + (n + 0)))))))))) =
D0 (to_lu n)
H:n <> 0
Little.succ
  (Little.succ
     (Little.succ
        (Little.succ
           (Little.succ
              (Little.succ
                 (Little.succ
                    (Little.succ
                       (Little.succ
                          (Little.succ
                             (to_lu (n + (n + (...))))))))))))) =
D0 (Little.succ (to_lu n)) rewrite (IHn H).n:nat
IHn:n <> 0 ->
to_lu (n + (n + (n + (n + (n + (n + (n + (n + (n + (n + 0)))))))))) =
D0 (to_lu n)
H:n <> 0
Little.succ
  (Little.succ
     (Little.succ
        (Little.succ
           (Little.succ
              (Little.succ
                 (Little.succ
                    (Little.succ
                       (Little.succ
                          (Little.succ (D0 (to_lu n))))))))))) =
D0 (Little.succ (to_lu n)) now destruct (to_lu n).
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; try easy.d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
0 + 10 * of_lu d = 0 <-> nztail (D0 d) = Nil
 rewrite Nat.add_0_l.d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
10 * of_lu d = 0 <-> nztail (D0 d) = Nil
 split; intros H.d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
H:10 * of_lu d = 0
nztail (D0 d) = Nil
d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
H:nztail (D0 d) = Nil
10 * of_lu d = 0
 -d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
H:10 * of_lu d = 0
nztail (D0 d) = Nil apply Nat.eq_mul_0_r in H; auto.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
H:nztail (D0 d) = Nil
10 * of_lu d = 0 simpl in H.d:uint
IHd:of_lu d = 0 <-> nztail d = Nil
H: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
10 * of_lu d = 0 destruct (nztail d); try discriminate.d:uint
IHd:of_lu d = 0 <-> Nil = Nil
H:Nil = Nil
10 * of_lu d = 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 (Nat.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) rewrite (to_lu_tenfold _ H), IH.d:uint
IH:to_lu (of_lu d) = lnorm d
H:of_lu d <> 0
D0 (lnorm d) = lnorm (D0 d)
   rewrite of_lu_0 in H.d:uint
IH:to_lu (of_lu d) = lnorm d
H:nztail d <> Nil
D0 (lnorm d) = lnorm (D0 d)
   unfold lnorm.d:uint
IH:to_lu (of_lu d) = 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
IH:to_lu (of_lu d) = 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 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 ?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.d:uint
Nat.to_uint (Nat.of_uint d) = unorm d
Proof.d:uint
Nat.to_uint (Nat.of_uint d) = unorm d
 rewrite to_uint_alt, of_uint_alt, to_of_lu.d:uint
rev (lnorm (rev d)) = unorm d
 apply rev_lnorm_rev.
Qed.

Some consequences

Lemma to_uint_inj n n' : Nat.to_uint n = Nat.to_uint n' -> n = n'.n, n':nat
Nat.to_uint n = Nat.to_uint n' -> n = n'
Proof.n, n':nat
Nat.to_uint n = Nat.to_uint n' -> n = n'
 intro EQ.n, n':nat
EQ:Nat.to_uint n = Nat.to_uint n'
n = n'
 now rewrite <- (of_to n), <- (of_to n'), EQ.
Qed.

Lemma to_uint_surj d : exists n, Nat.to_uint n = unorm d.d:uint
exists n : nat, Nat.to_uint n = unorm d
Proof.d:uint
exists n : nat, Nat.to_uint n = unorm d
 exists (Nat.of_uint d).d:uint
Nat.to_uint (Nat.of_uint d) = unorm d apply to_of.
Qed.

Lemma of_uint_norm d : Nat.of_uint (unorm d) = Nat.of_uint d.d:uint
Nat.of_uint (unorm d) = Nat.of_uint d
Proof.d:uint
Nat.of_uint (unorm d) = Nat.of_uint d
 unfold Nat.of_uint.d:uint
Nat.of_uint_acc (unorm d) 0 = Nat.of_uint_acc d 0 now induction d.
Qed.

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

Lemma of_iff d d' : Nat.of_uint d = Nat.of_uint d' <-> unorm d = unorm d'.d, d':uint
Nat.of_uint d = Nat.of_uint d' <-> unorm d = unorm d'
Proof.d, d':uint
Nat.of_uint d = Nat.of_uint d' <-> unorm d = unorm d'
 split.d, d':uint
Nat.of_uint d = Nat.of_uint d' -> unorm d = unorm d'
d, d':uint
unorm d = unorm d' -> Nat.of_uint d = Nat.of_uint d' apply of_inj.d, d':uint
unorm d = unorm d' -> Nat.of_uint d = Nat.of_uint d' intros E.d, d':uint
E:unorm d = unorm d'
Nat.of_uint d = Nat.of_uint d' rewrite <- of_uint_norm, E.d, d':uint
E:unorm d = unorm d'
Nat.of_uint (unorm d') = Nat.of_uint d'
 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.n:nat
Nat.of_int (Nat.to_int n) = Some n
Proof.n:nat
Nat.of_int (Nat.to_int n) = Some n
 unfold Nat.to_int, Nat.of_int, norm.n:nat
Some (Nat.of_uint (unorm (Nat.to_uint n))) = Some n f_equal.n:nat
Nat.of_uint (unorm (Nat.to_uint n)) = n
 rewrite Unsigned.of_uint_norm.n:nat
Nat.of_uint (Nat.to_uint n) = n apply Unsigned.of_to.
Qed.

Lemma to_of (d:int)(n:nat) : Nat.of_int d = Some n -> Nat.to_int n = norm d.d:int
n:nat
Nat.of_int d = Some n -> Nat.to_int n = norm d
Proof.d:int
n:nat
Nat.of_int d = Some n -> Nat.to_int n = norm d
 unfold Nat.of_int.d:int
n:nat
match norm d with
| Pos u => Some (Nat.of_uint u)
| Neg _ => None
end = Some n -> Nat.to_int n = norm d
 destruct (norm d) eqn:Hd; intros [= <-].d:int
d0:uint
Hd:norm d = Pos d0
Nat.to_int (Nat.of_uint d0) = Pos d0
 unfold Nat.to_int.d:int
d0:uint
Hd:norm d = Pos d0
Pos (Nat.to_uint (Nat.of_uint d0)) = Pos d0 rewrite Unsigned.to_of.d:int
d0:uint
Hd:norm d = Pos d0
Pos (unorm d0) = Pos d0 f_equal.d:int
d0:uint
Hd:norm d = Pos d0
unorm d0 = d0
 revert Hd; destruct d; simpl.d, d0:uint
Pos (unorm d) = Pos d0 -> unorm d0 = d0
d, d0:uint
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 = Pos d0 -> unorm d0 = d0
 -d, d0:uint
Pos (unorm d) = Pos d0 -> unorm d0 = d0 intros [= <-].d:uint
unorm (unorm d) = unorm d apply unorm_invol.
 -d, d0:uint
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 = Pos d0 -> unorm d0 = d0 destruct (nzhead d); now intros [= <-].
Qed.

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

Lemma to_int_pos_surj d : exists n, Nat.to_int n = norm (Pos d).d:uint
exists n : nat, Nat.to_int n = norm (Pos d)
Proof.d:uint
exists n : nat, Nat.to_int n = norm (Pos d)
 exists (Nat.of_uint d).d:uint
Nat.to_int (Nat.of_uint d) = norm (Pos d) unfold Nat.to_int.d:uint
Pos (Nat.to_uint (Nat.of_uint d)) = norm (Pos d) now rewrite Unsigned.to_of.
Qed.

Lemma of_int_norm d : Nat.of_int (norm d) = Nat.of_int d.d:int
Nat.of_int (norm d) = Nat.of_int d
Proof.d:int
Nat.of_int (norm d) = Nat.of_int d
 unfold Nat.of_int.d:int
match norm (norm d) with
| Pos u => Some (Nat.of_uint u)
| Neg _ => None
end =
match norm d with
| Pos u => Some (Nat.of_uint u)
| Neg _ => None
end 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'.d, d':uint
Nat.of_int (Pos d) = Nat.of_int (Pos d') ->
unorm d = unorm d'
Proof.d, d':uint
Nat.of_int (Pos d) = Nat.of_int (Pos d') ->
unorm d = unorm d'
 unfold Nat.of_int.d, d':uint
match norm (Pos d) with
| Pos u => Some (Nat.of_uint u)
| Neg _ => None
end =
match norm (Pos d') with
| Pos u => Some (Nat.of_uint u)
| Neg _ => None
end -> unorm d = unorm d' simpl.d, d':uint
Some (Nat.of_uint (unorm d)) =
Some (Nat.of_uint (unorm d')) -> unorm d = unorm d' intros [= H].d, d':uint
H:Nat.of_uint (unorm d) = Nat.of_uint (unorm d')
unorm d = unorm d' apply Unsigned.of_inj.d, d':uint
H:Nat.of_uint (unorm d) = Nat.of_uint (unorm d')
Nat.of_uint d = Nat.of_uint d'
 now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm.
Qed.

End Signed.