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

DecimalZ

Proofs that conversions between decimal numbers and Z are bijections.

Require Import Decimal DecimalFacts DecimalPos DecimalN ZArith.

Lemma of_to (z:Z) : Z.of_int (Z.to_int z) = z.z:Z
Z.of_int (Z.to_int z) = z
Proof.z:Z
Z.of_int (Z.to_int z) = z
 destruct z; simpl.Z.of_uint 0 = 0%Z
p:positive
Z.of_uint (Pos.to_uint p) = Z.pos p
p:positive
(- Z.of_uint (Pos.to_uint p))%Z = Z.neg p
 -Z.of_uint 0 = 0%Z trivial.
 -p:positive
Z.of_uint (Pos.to_uint p) = Z.pos p unfold Z.of_uint.p:positive
Z.of_N (Pos.of_uint (Pos.to_uint p)) = Z.pos p rewrite DecimalPos.Unsigned.of_to.p:positive
Z.of_N (N.pos p) = Z.pos p now destruct p.
 -p:positive
(- Z.of_uint (Pos.to_uint p))%Z = Z.neg p unfold Z.of_uint.p:positive
(- Z.of_N (Pos.of_uint (Pos.to_uint p)))%Z = Z.neg p rewrite DecimalPos.Unsigned.of_to.p:positive
(- Z.of_N (N.pos p))%Z = Z.neg p destruct p; auto.
Qed.

Lemma to_of (d:int) : Z.to_int (Z.of_int d) = norm d.d:int
Z.to_int (Z.of_int d) = norm d
Proof.d:int
Z.to_int (Z.of_int d) = norm d
 destruct d; simpl; unfold Z.to_int, Z.of_uint.d:uint
match Z.of_N (Pos.of_uint d) with
| 0%Z => 0%int
| Z.pos p => Pos (Pos.to_uint p)
| Z.neg p => Neg (Pos.to_uint p)
end = Pos (unorm d)
d:uint
match (- Z.of_N (Pos.of_uint d))%Z with
| 0%Z => 0%int
| Z.pos p => Pos (Pos.to_uint p)
| Z.neg p => Neg (Pos.to_uint p)
end =
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
 -d:uint
match Z.of_N (Pos.of_uint d) with
| 0%Z => 0%int
| Z.pos p => Pos (Pos.to_uint p)
| Z.neg p => Neg (Pos.to_uint p)
end = Pos (unorm d) rewrite <- (DecimalN.Unsigned.to_of d).d:uint
match Z.of_N (Pos.of_uint d) with
| 0%Z => 0%int
| Z.pos p => Pos (Pos.to_uint p)
| Z.neg p => Neg (Pos.to_uint p)
end = Pos (N.to_uint (N.of_uint d)) unfold N.of_uint.d:uint
match Z.of_N (Pos.of_uint d) with
| 0%Z => 0%int
| Z.pos p => Pos (Pos.to_uint p)
| Z.neg p => Neg (Pos.to_uint p)
end = Pos (N.to_uint (Pos.of_uint d))
   now destruct (Pos.of_uint d).
 -d:uint
match (- Z.of_N (Pos.of_uint d))%Z with
| 0%Z => 0%int
| Z.pos p => Pos (Pos.to_uint p)
| Z.neg p => Neg (Pos.to_uint p)
end =
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 destruct (Pos.of_uint d) eqn:Hd; simpl; f_equal.d:uint
Hd:Pos.of_uint d = 0%N
0%int =
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
d:uint
p:positive
Hd:Pos.of_uint d = N.pos p
Neg (Pos.to_uint p) =
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
   +d:uint
Hd:Pos.of_uint d = 0%N
0%int =
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 generalize (DecimalPos.Unsigned.to_of d).d:uint
Hd:Pos.of_uint d = 0%N
N.to_uint (Pos.of_uint d) = unorm d ->
0%int =
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 rewrite Hd.d:uint
Hd:Pos.of_uint d = 0%N
N.to_uint 0 = unorm d ->
0%int =
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 simpl.d:uint
Hd:Pos.of_uint d = 0%N
0%uint = unorm d ->
0%int =
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
     intros H.d:uint
Hd:Pos.of_uint d = 0%N
H:0%uint = unorm d
0%int =
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 symmetry in H.d:uint
Hd:Pos.of_uint d = 0%N
H:unorm d = 0%uint
0%int =
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 apply unorm_0 in H.d:uint
Hd:Pos.of_uint d = 0%N
H:nzhead d = Nil
0%int =
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 now rewrite H.
   +d:uint
p:positive
Hd:Pos.of_uint d = N.pos p
Neg (Pos.to_uint p) =
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 assert (Hp := DecimalPos.Unsigned.to_of d).d:uint
p:positive
Hd:Pos.of_uint d = N.pos p
Hp:N.to_uint (Pos.of_uint d) = unorm d
Neg (Pos.to_uint p) =
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 rewrite Hd in Hp.d:uint
p:positive
Hd:Pos.of_uint d = N.pos p
Hp:N.to_uint (N.pos p) = unorm d
Neg (Pos.to_uint p) =
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 simpl in *.d:uint
p:positive
Hd:Pos.of_uint d = N.pos p
Hp:Pos.to_uint p = unorm d
Neg (Pos.to_uint p) =
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
     rewrite Hp.d:uint
p:positive
Hd:Pos.of_uint d = N.pos p
Hp:Pos.to_uint p = unorm d
Neg (unorm d) =
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 unfold unorm in *.d:uint
p:positive
Hd:Pos.of_uint d = N.pos p
Hp:Pos.to_uint p =
match nzhead 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
Neg
  match nzhead 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 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
     destruct (nzhead d); trivial.d:uint
p:positive
Hd:Pos.of_uint d = N.pos p
Hp:Pos.to_uint p = 0%uint
(-0)%int = 0%int
     generalize (DecimalPos.Unsigned.of_to p).d:uint
p:positive
Hd:Pos.of_uint d = N.pos p
Hp:Pos.to_uint p = 0%uint
Pos.of_uint (Pos.to_uint p) = N.pos p ->
(-0)%int = 0%int now rewrite Hp.
Qed.

Some consequences

Lemma to_int_inj n n' : Z.to_int n = Z.to_int n' -> n = n'.n, n':Z
Z.to_int n = Z.to_int n' -> n = n'
Proof.n, n':Z
Z.to_int n = Z.to_int n' -> n = n'
 intro EQ.n, n':Z
EQ:Z.to_int n = Z.to_int n'
n = n'
 now rewrite <- (of_to n), <- (of_to n'), EQ.
Qed.

Lemma to_int_surj d : exists n, Z.to_int n = norm d.d:int
exists n : Z, Z.to_int n = norm d
Proof.d:int
exists n : Z, Z.to_int n = norm d
 exists (Z.of_int d).d:int
Z.to_int (Z.of_int d) = norm d apply to_of.
Qed.

Lemma of_int_norm d : Z.of_int (norm d) = Z.of_int d.d:int
Z.of_int (norm d) = Z.of_int d
Proof.d:int
Z.of_int (norm d) = Z.of_int d
 unfold Z.of_int, Z.of_uint.d:int
match norm d with
| Pos d0 => Z.of_N (Pos.of_uint d0)
| Neg d0 => (- Z.of_N (Pos.of_uint d0))%Z
end =
match d with
| Pos d0 => Z.of_N (Pos.of_uint d0)
| Neg d0 => (- Z.of_N (Pos.of_uint d0))%Z
end
 destruct d.d:uint
match norm (Pos d) with
| Pos d0 => Z.of_N (Pos.of_uint d0)
| Neg d0 => (- Z.of_N (Pos.of_uint d0))%Z
end = Z.of_N (Pos.of_uint d)
d:uint
match norm (Neg d) with
| Pos d0 => Z.of_N (Pos.of_uint d0)
| Neg d0 => (- Z.of_N (Pos.of_uint d0))%Z
end = (- Z.of_N (Pos.of_uint d))%Z
 -d:uint
match norm (Pos d) with
| Pos d0 => Z.of_N (Pos.of_uint d0)
| Neg d0 => (- Z.of_N (Pos.of_uint d0))%Z
end = Z.of_N (Pos.of_uint d) simpl.d:uint
Z.of_N (Pos.of_uint (unorm d)) =
Z.of_N (Pos.of_uint d) now rewrite DecimalPos.Unsigned.of_uint_norm.
 -d:uint
match norm (Neg d) with
| Pos d0 => Z.of_N (Pos.of_uint d0)
| Neg d0 => (- Z.of_N (Pos.of_uint d0))%Z
end = (- Z.of_N (Pos.of_uint d))%Z 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 => Z.of_N (Pos.of_uint d0)
| Neg d0 => (- Z.of_N (Pos.of_uint d0))%Z
end = (- Z.of_N (Pos.of_uint d))%Z 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'.d, d':int
Z.of_int d = Z.of_int d' -> norm d = norm d'
Proof.d, d':int
Z.of_int d = Z.of_int d' -> norm d = norm d'
 intros.d, d':int
H:Z.of_int d = Z.of_int d'
norm d = norm d' rewrite <- !to_of.d, d':int
H:Z.of_int d = Z.of_int d'
Z.to_int (Z.of_int d) = Z.to_int (Z.of_int d') now f_equal.
Qed.

Lemma of_iff d d' : Z.of_int d = Z.of_int d' <-> norm d = norm d'.d, d':int
Z.of_int d = Z.of_int d' <-> norm d = norm d'
Proof.d, d':int
Z.of_int d = Z.of_int d' <-> norm d = norm d'
 split.d, d':int
Z.of_int d = Z.of_int d' -> norm d = norm d'
d, d':int
norm d = norm d' -> Z.of_int d = Z.of_int d' apply of_inj.d, d':int
norm d = norm d' -> Z.of_int d = Z.of_int d' intros E.d, d':int
E:norm d = norm d'
Z.of_int d = Z.of_int d' rewrite <- of_int_norm, E.d, d':int
E:norm d = norm d'
Z.of_int (norm d') = Z.of_int d'
 apply of_int_norm.
Qed.