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

Require Import Decimal DecimalFacts DecimalPos PArith NArith.

Module Unsigned.

Lemma of_to (n:N) : N.of_uint (N.to_uint n) = n.
n:N
N.of_uint (N.to_uint n) = n
Proof.
n:N
N.of_uint (N.to_uint n) = n
 destruct n.
N.of_uint (N.to_uint 0) = 0%N
p:positive
N.of_uint (N.to_uint (N.pos p)) = N.pos p
 -
N.of_uint (N.to_uint 0) = 0%N reflexivity.
 -
p:positive
N.of_uint (N.to_uint (N.pos p)) = N.pos p apply DecimalPos.Unsigned.of_to.
Qed.

Lemma to_of (d:uint) : N.to_uint (N.of_uint d) = unorm d.
d:uint
N.to_uint (N.of_uint d) = unorm d
Proof.
d:uint
N.to_uint (N.of_uint d) = unorm d
 exact (DecimalPos.Unsigned.to_of d).
Qed.

Lemma to_uint_inj n n' : N.to_uint n = N.to_uint n' -> n = n'.
n, n':N
N.to_uint n = N.to_uint n' -> n = n'
Proof.
n, n':N
N.to_uint n = N.to_uint n' -> n = n'
 intros E.
n, n':N
E:N.to_uint n = N.to_uint n'
n = n' now rewrite <- (of_to n), <- (of_to n'), E.
Qed.

Lemma to_uint_surj d : exists p, N.to_uint p = unorm d.
d:uint
exists p : N, N.to_uint p = unorm d
Proof.
d:uint
exists p : N, N.to_uint p = unorm d
 exists (N.of_uint d).
d:uint
N.to_uint (N.of_uint d) = unorm d apply to_of.
Qed.

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

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

Lemma of_iff d d' : N.of_uint d = N.of_uint d' <-> unorm d = unorm d'.
d, d':uint
N.of_uint d = N.of_uint d' <-> unorm d = unorm d'
Proof.
d, d':uint
N.of_uint d = N.of_uint d' <-> unorm d = unorm d'
 split.
d, d':uint
N.of_uint d = N.of_uint d' -> unorm d = unorm d'
d, d':uint
unorm d = unorm d' -> N.of_uint d = N.of_uint d' apply of_inj.
d, d':uint
unorm d = unorm d' -> N.of_uint d = N.of_uint d' intros E.
d, d':uint
E:unorm d = unorm d'
N.of_uint d = N.of_uint d' rewrite <- of_uint_norm, E.
d, d':uint
E:unorm d = unorm d'
N.of_uint (unorm d') = N.of_uint d'
 apply of_uint_norm.
Qed.

End Unsigned.

Module Signed.

Lemma of_to (n:N) : N.of_int (N.to_int n) = Some n.
n:N
N.of_int (N.to_int n) = Some n
Proof.
n:N
N.of_int (N.to_int n) = Some n
 unfold N.to_int, N.of_int, norm.
n:N
Some (Pos.of_uint (unorm (N.to_uint n))) = Some n f_equal.
n:N
Pos.of_uint (unorm (N.to_uint n)) = n
 rewrite Unsigned.of_uint_norm.
n:N
N.of_uint (N.to_uint n) = n apply Unsigned.of_to.
Qed.

Lemma to_of (d:int)(n:N) : N.of_int d = Some n -> N.to_int n = norm d.
d:int
n:N
N.of_int d = Some n -> N.to_int n = norm d
Proof.
d:int
n:N
N.of_int d = Some n -> N.to_int n = norm d
 unfold N.of_int.
d:int
n:N
match norm d with
| Pos d0 => Some (Pos.of_uint d0)
| Neg _ => None
end = Some n -> N.to_int n = norm d
 destruct (norm d) eqn:Hd; intros [= <-].
d:int
d0:uint
Hd:norm d = Pos d0
N.to_int (Pos.of_uint d0) = Pos d0
 unfold N.to_int.
d:int
d0:uint
Hd:norm d = Pos d0
Pos (N.to_uint (Pos.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' : N.to_int n = N.to_int n' -> n = n'.
n, n':N
N.to_int n = N.to_int n' -> n = n'
Proof.
n, n':N
N.to_int n = N.to_int n' -> n = n'
 intro E.
n, n':N
E:N.to_int n = N.to_int n'
n = n'
 assert (E' : Some n = Some n').
n, n':N
E:N.to_int n = N.to_int n'
Some n = Some n'
n, n':N
E:N.to_int n = N.to_int n'
E':Some n = Some n'
n = n'
 {
n, n':N
E:N.to_int n = N.to_int n'
Some n = Some n' now rewrite <- (of_to n), <- (of_to n'), E. }
n, n':N
E:N.to_int n = N.to_int n'
E':Some n = Some n'
n = n'
 now injection E'.
Qed.

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

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

End Signed.