Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: DecimalNat.v Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   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).
Proof.
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).
Proof.
revert d; induction n; simpl; trivial.
Qed.

Lemma to_lu_equiv n :
  to_lu n = Nat.to_little_uint n zero.
Proof.
induction n; simpl; trivial.
now rewrite IHn, <- to_little_uint_succ.
Qed.

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

(** Properties of [of_lu] *)

Lemma of_lu_eqn d :
of_lu d = hd d + 10 * of_lu (tl d).
Proof.
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).
Proof.
induction d; trivial.
simpl_of_lu. rewrite IHd. simpl_of_lu.
now rewrite Nat.mul_succ_r, <- (Nat.add_comm 10).
Qed.

Lemma of_to_lu n :
of_lu (to_lu n) = n.
Proof.
induction n; simpl; trivial. rewrite of_lu_succ. 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.
Proof.
revert 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.
Proof.
revert n. 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).
Proof.
unfold Nat.of_uint. now rewrite of_uint_acc_spec.
Qed.

(** First main bijection result *)

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

(** The other direction *)

Lemma to_lu_tenfold n : n<>0 ->
to_lu (10 * n) = D0 (to_lu n).
Proof.
induction n.
- simpl. now destruct 1.
- intros _.
   destruct (Nat.eq_dec n 0) as [->|H]; simpl; trivial.
   rewrite !Nat.add_succ_r.
   simpl in *. rewrite (IHn H). now destruct (to_lu n).
Qed.

Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil.
Proof.
induction d; try simpl_of_lu; try easy.
rewrite Nat.add_0_l.
split; intros H.
- apply Nat.eq_mul_0_r in H; auto.
   rewrite IHd in H. simpl. now rewrite H.
- simpl in H. destruct (nztail d); try discriminate.
   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).
Proof.
intro IH.
destruct (Nat.eq_dec (of_lu d) 0) as [H|H].
- rewrite H. simpl. rewrite of_lu_0 in H.
   unfold lnorm. simpl. now rewrite H.
- rewrite (to_lu_tenfold _ H), IH.
   rewrite of_lu_0 in H.
   unfold lnorm. simpl. now destruct (nztail d).
Qed.

Lemma to_of_lu d : to_lu (of_lu d) = lnorm d.
Proof.
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.
Proof.
rewrite to_uint_alt, of_uint_alt, to_of_lu.
apply rev_lnorm_rev.
Qed.

(** Some consequences *)

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

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

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

Lemma of_inj d d' :
Nat.of_uint d = Nat.of_uint d' -> unorm d = unorm d'.
Proof.
intros. rewrite <- !to_of. now f_equal.
Qed.

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

Lemma to_of (d:int)(n:nat) : Nat.of_int d = Some n -> Nat.to_int n = norm d.
Proof.
unfold Nat.of_int.
destruct (norm d) eqn:Hd; intros [= <-].
unfold Nat.to_int. rewrite Unsigned.to_of. f_equal.
revert Hd; destruct d; simpl.
- intros [= <-]. apply unorm_invol.
- destruct (nzhead d); now intros [= <-].
Qed.

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

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

Lemma of_int_norm d : Nat.of_int (norm d) = Nat.of_int d.
Proof.
unfold Nat.of_int. 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'.
Proof.
unfold Nat.of_int. simpl. intros [= H]. apply Unsigned.of_inj.
now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm.
Qed.

End Signed.

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.