The Coq Proof Assistant

# Library Coq.Numbers.HexadecimalPos

# HexadecimalPos

Proofs that conversions between hexadecimal numbers and positive are bijections.
Require Import Hexadecimal HexadecimalFacts PArith NArith.
Module Unsigned.
Local Open Scope N.
A direct version of of_little_uint
Fixpoint of_lu (d:uint) : N :=
match d with
| Nil => 0
| 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.
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.
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.
Fixpoint usize (d:uint) : N :=
match d with
| Nil => 0
| D0 d => N.succ (usize d)
| D1 d => N.succ (usize d)
| D2 d => N.succ (usize d)
| D3 d => N.succ (usize d)
| D4 d => N.succ (usize d)
| D5 d => N.succ (usize d)
| D6 d => N.succ (usize d)
| D7 d => N.succ (usize d)
| D8 d => N.succ (usize d)
| D9 d => N.succ (usize d)
| Da d => N.succ (usize d)
| Db d => N.succ (usize d)
| Dc d => N.succ (usize d)
| Dd d => N.succ (usize d)
| De d => N.succ (usize d)
| Df d => N.succ (usize d)
end.
Lemma of_lu_revapp d d' :
of_lu (revapp d d') =
of_lu (rev d) + of_lu d' * 0x10^usize d.
Definition Nadd n p :=
match n with
| N0 => p
| Npos p0 => (p0+p)%positive
end.
Lemma Nadd_simpl n p q : Npos (Nadd n (p * q)) = n + Npos p * Npos q.
Lemma of_uint_acc_eqn d acc : d<>Nil ->
Pos.of_hex_uint_acc d acc = Pos.of_hex_uint_acc (tl d) (Nadd (hd d) (0x10*acc)).
Lemma of_uint_acc_rev d acc :
Npos (Pos.of_hex_uint_acc d acc) =
of_lu (rev d) + (Npos acc) * 0x10^usize d.
Lemma of_uint_alt d : Pos.of_hex_uint d = of_lu (rev d).
Lemma of_lu_rev d : Pos.of_hex_uint (rev d) = of_lu d.
Lemma of_lu_double_gen d :
of_lu (Little.double d) = N.double (of_lu d) /\
of_lu (Little.succ_double d) = N.succ_double (of_lu d).
Lemma of_lu_double d :
of_lu (Little.double d) = N.double (of_lu d).
Lemma of_lu_succ_double d :
of_lu (Little.succ_double d) = N.succ_double (of_lu d).
First bijection result
Lemma of_to (p:positive) : Pos.of_hex_uint (Pos.to_hex_uint p) = Npos p.
The other direction
Definition to_lu n :=
match n with
| N0 => Hexadecimal.zero
| Npos p => Pos.to_little_hex_uint p
end.
Lemma succ_double_alt d :
Little.succ_double d = Little.succ (Little.double d).
Lemma double_succ d :
Little.double (Little.succ d) =
Little.succ (Little.succ_double d).
Lemma to_lu_succ n :
to_lu (N.succ n) = Little.succ (to_lu n).
Lemma nat_iter_S n {A} (f:A->A) i :
Nat.iter (S n) f i = f (Nat.iter n f i).
Lemma nat_iter_0 {A} (f:A->A) i : Nat.iter 0 f i = i.
Lemma to_lhex_tenfold p :
to_lu (0x10 * Npos p) = D0 (to_lu (Npos p)).
Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil.
Lemma to_of_lu_tenfold d :
to_lu (of_lu d) = lnorm d ->
to_lu (0x10 * of_lu d) = lnorm (D0 d).
Lemma Nadd_alt n m : n + m = Nat.iter (N.to_nat n) N.succ m.
Ltac simpl_to_nat := simpl N.to_nat; unfold Pos.to_nat; simpl Pos.iter_op.
Lemma to_of_lu d : to_lu (of_lu d) = lnorm d.
Second bijection result
Lemma to_of (d:uint) : N.to_hex_uint (Pos.of_hex_uint d) = unorm d.
Some consequences
Lemma to_uint_nonzero p : Pos.to_hex_uint p <> zero.
Lemma to_uint_nonnil p : Pos.to_hex_uint p <> Nil.
Lemma to_uint_inj p p' : Pos.to_hex_uint p = Pos.to_hex_uint p' -> p = p'.
Lemma to_uint_pos_surj d :
unorm d<>zero -> exists p, Pos.to_hex_uint p = unorm d.
Lemma of_uint_norm d : Pos.of_hex_uint (unorm d) = Pos.of_hex_uint d.
Lemma of_inj d d' :
Pos.of_hex_uint d = Pos.of_hex_uint d' -> unorm d = unorm d'.
Lemma of_iff d d' : Pos.of_hex_uint d = Pos.of_hex_uint d' <-> unorm d = unorm d'.
Lemma nztail_to_hex_uint p :
let (h, n) := Hexadecimal.nztail (Pos.to_hex_uint p) in
Npos p = Pos.of_hex_uint h * 0x10^(N.of_nat n).
Definition double d := rev (Little.double (rev d)).
Lemma double_unorm d : double (unorm d) = unorm (double d).
Lemma double_nzhead d : double (nzhead d) = nzhead (double d).
Lemma of_hex_uint_double d :
Pos.of_hex_uint (double d) = N.double (Pos.of_hex_uint d).
End Unsigned.
Conversion from/to signed decimal numbers
Module Signed.
Lemma of_to (p:positive) : Pos.of_hex_int (Pos.to_hex_int p) = Some p.
Lemma to_of (d:int)(p:positive) :
Pos.of_hex_int d = Some p -> Pos.to_hex_int p = norm d.
Lemma to_int_inj p p' : Pos.to_hex_int p = Pos.to_hex_int p' -> p = p'.
Lemma to_int_pos_surj d :
unorm d <> zero -> exists p, Pos.to_hex_int p = norm (Pos d).
Lemma of_int_norm d : Pos.of_hex_int (norm d) = Pos.of_hex_int d.
Lemma of_inj_pos d d' :
Pos.of_hex_int (Pos d) = Pos.of_hex_int (Pos d') -> unorm d = unorm d'.
End Signed.