Timings for DecimalN.v
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./Numbers/DecimalN.timing
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./Numbers/DecimalN.timing
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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) *)
(************************************************************************)
(** * DecimalN
Proofs that conversions between decimal numbers and [N]
are bijections *)
Require Import Decimal DecimalFacts DecimalPos PArith NArith.
Lemma of_to (n:N) : N.of_uint (N.to_uint n) = n.
apply DecimalPos.Unsigned.of_to.
Lemma to_of (d:uint) : N.to_uint (N.of_uint d) = unorm d.
exact (DecimalPos.Unsigned.to_of d).
Lemma to_uint_inj n n' : N.to_uint n = N.to_uint n' -> n = n'.
now rewrite <- (of_to n), <- (of_to n'), E.
Lemma to_uint_surj d : exists p, N.to_uint p = unorm d.
Lemma of_uint_norm d : N.of_uint (unorm d) = N.of_uint d.
Lemma of_inj d d' :
N.of_uint d = N.of_uint d' -> unorm d = unorm d'.
Lemma of_iff d d' : N.of_uint d = N.of_uint d' <-> unorm d = unorm d'.
rewrite <- of_uint_norm, E.
(** Conversion from/to signed decimal numbers *)
Lemma of_to (n:N) : N.of_int (N.to_int n) = Some n.
unfold N.to_int, N.of_int, norm.
rewrite Unsigned.of_uint_norm.
Lemma to_of (d:int)(n:N) : N.of_int d = Some n -> N.to_int n = norm d.
destruct (norm d) eqn:Hd; intros [= <-].
revert Hd; destruct d; simpl.
destruct (nzhead d); now intros [= <-].
Lemma to_int_inj n n' : N.to_int n = N.to_int n' -> n = n'.
assert (E' : Some n = Some n').
now rewrite <- (of_to n), <- (of_to n'), E.
Lemma to_int_pos_surj d : exists n, N.to_int n = norm (Pos d).
now rewrite Unsigned.to_of.
Lemma of_int_norm d : N.of_int (norm d) = N.of_int d.
now rewrite norm_involutive.
Lemma of_inj_pos d d' :
N.of_int (Pos d) = N.of_int (Pos d') -> unorm d = unorm d'.
change Pos.of_uint with N.of_uint in H.
now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm.