Library Coq.Numbers.HexadecimalNat


HexadecimalNat

Proofs that conversions between hexadecimal numbers and nat are bijections.

Require Import Hexadecimal HexadecimalFacts Arith.

Module Unsigned.

A few helper functions used during proofs

Definition hd d :=
  match d with
  | Nil => 0x0
  | D0 _ => 0x0
  | D1 _ => 0x1
  | D2 _ => 0x2
  | D3 _ => 0x3
  | D4 _ => 0x4
  | D5 _ => 0x5
  | D6 _ => 0x6
  | D7 _ => 0x7
  | D8 _ => 0x8
  | D9 _ => 0x9
  | Da _ => 0xa
  | Db _ => 0xb
  | Dc _ => 0xc
  | Dd _ => 0xd
  | De _ => 0xe
  | Df _ => 0xf
  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
  | Da d | Db d | Dc d | Dd d | De d | Df 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)
  | Da d => S (usize d)
  | Db d => S (usize d)
  | Dc d => S (usize d)
  | Dd d => S (usize d)
  | De d => S (usize d)
  | Df d => S (usize d)
  end.

A direct version of to_little_uint, not tail-recursive
Fixpoint to_lu n :=
  match n with
  | 0 => Hexadecimal.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 => 0x0
  | D0 d => 0x10 * of_lu d
  | D1 d => 0x1 + 0x10 * of_lu d
  | D2 d => 0x2 + 0x10 * of_lu d
  | D3 d => 0x3 + 0x10 * of_lu d
  | D4 d => 0x4 + 0x10 * of_lu d
  | D5 d => 0x5 + 0x10 * of_lu d
  | D6 d => 0x6 + 0x10 * of_lu d
  | D7 d => 0x7 + 0x10 * of_lu d
  | D8 d => 0x8 + 0x10 * of_lu d
  | D9 d => 0x9 + 0x10 * of_lu d
  | Da d => 0xa + 0x10 * of_lu d
  | Db d => 0xb + 0x10 * of_lu d
  | Dc d => 0xc + 0x10 * of_lu d
  | Dd d => 0xd + 0x10 * of_lu d
  | De d => 0xe + 0x10 * of_lu d
  | Df d => 0xf + 0x10 * of_lu d
  end.

Properties of to_lu
Properties of of_lu

Lemma of_lu_eqn d :
  of_lu d = hd d + 0x10 * of_lu (tl d).

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).

Lemma of_to_lu n :
  of_lu (to_lu n) = n.

Lemma of_lu_revapp d d' :
  of_lu (revapp d d') =
    of_lu (rev d) + of_lu d' * 0x10^usize d.

Lemma of_uint_acc_spec n d :
  Nat.of_hex_uint_acc d n = of_lu (rev d) + n * 0x10^usize d.

Lemma of_uint_alt d : Nat.of_hex_uint d = of_lu (rev d).

First main bijection result
The other direction

Lemma to_lu_sixteenfold n : n<>0 ->
  to_lu (0x10 * n) = D0 (to_lu n).

Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil.

Lemma to_of_lu_sixteenfold d :
  to_lu (of_lu d) = lnorm d ->
  to_lu (0x10 * of_lu d) = lnorm (D0 d).

Lemma to_of_lu d : to_lu (of_lu d) = lnorm d.

Second bijection result
Some consequences
Conversion from/to signed hexadecimal numbers