Scheme Equality for uint.

Scheme Equality for int.

Lemma rev_revapp d d' :
rev (revapp d d') = revapp d' d.

Lemma rev_rev d : rev (rev d) = d.

Lemma revapp_rev_nil d : revapp (rev d) Nil = d.

Lemma app_nil_r d : app d Nil = d.

Lemma app_int_nil_r d : app_int d Nil = d.

Lemma revapp_revapp_1 d d' d'' :
nb_digits d <= 1 ->
revapp (revapp d d') d'' = revapp d' (revapp d d'').

Lemma nb_digits_pos d : d <> Nil -> 0 < nb_digits d.

Lemma nb_digits_revapp d d' :
nb_digits (revapp d d') = nb_digits d + nb_digits d'.

Lemma nb_digits_rev u : nb_digits (rev u) = nb_digits u.

Lemma nb_digits_iter_D0 n d :
nb_digits (Nat.iter n D0 d) = n + nb_digits d.

Fixpoint nth n u :=
match n with
| O =>
match u with
| Nil => Nil
| D0 d => D0 Nil
| D1 d => D1 Nil
| D2 d => D2 Nil
| D3 d => D3 Nil
| D4 d => D4 Nil
| D5 d => D5 Nil
| D6 d => D6 Nil
| D7 d => D7 Nil
| D8 d => D8 Nil
| D9 d => D9 Nil
| Da d => Da Nil
| Db d => Db Nil
| Dc d => Dc Nil
| Dd d => Dd Nil
| De d => De Nil
| Df d => Df Nil
end
| S n =>
match u with
| Nil => Nil
| 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 =>
nth n d
end
end.

Lemma nb_digits_nth n u : nb_digits (nth n u) <= 1.

Lemma nth_revapp_r n d d' :
nb_digits d <= n ->
nth n (revapp d d') = nth (n - nb_digits d) d'.

Lemma nth_revapp_l n d d' :
n < nb_digits d ->
nth n (revapp d d') = nth (nb_digits d - n - 1) d.

Normalization on little-endian numbers

Fixpoint nztail d :=
match d with
| Nil => Nil
| D0 d => match nztail d with Nil => Nil | d' => D0 d' end
| D1 d => D1 (nztail d)
| D2 d => D2 (nztail d)
| D3 d => D3 (nztail d)
| D4 d => D4 (nztail d)
| D5 d => D5 (nztail d)
| D6 d => D6 (nztail d)
| D7 d => D7 (nztail d)
| D8 d => D8 (nztail d)
| D9 d => D9 (nztail d)
| Da d => Da (nztail d)
| Db d => Db (nztail d)
| Dc d => Dc (nztail d)
| Dd d => Dd (nztail d)
| De d => De (nztail d)
| Df d => Df (nztail d)
end.

Definition lnorm d :=
match nztail d with
| Nil => zero
| d => d
end.

Lemma nzhead_revapp_0 d d' : nztail d = Nil ->

Lemma nzhead_revapp d d' : nztail d <> Nil ->
nzhead (revapp d d') = revapp (nztail d) d'.

Lemma nzhead_rev d : nztail d <> Nil ->
nzhead (rev d) = rev (nztail d).

Lemma rev_nztail_rev d :
rev (nztail (rev d)) = nzhead d.

Lemma revapp_nil_inv d d' : revapp d d' = Nil -> d = Nil /\ d' = Nil.

Lemma rev_nil_inv d : rev d = Nil -> d = Nil.

Lemma rev_lnorm_rev d :
rev (lnorm (rev d)) = unorm d.

Lemma unorm_0 d : unorm d = zero <-> nzhead d = Nil.

Lemma unorm_nonnil d : unorm d <> Nil.

Lemma unorm_D0 u : unorm (D0 u) = unorm u.

Lemma unorm_iter_D0 n u : unorm (Nat.iter n D0 u) = unorm u.

Lemma nb_digits_unorm u :
u <> Nil -> nb_digits (unorm u) <= nb_digits u.

Lemma nztail_invol d : nztail (nztail d) = nztail d.

Lemma unorm_invol d : unorm (unorm d) = unorm d.

Lemma norm_invol d : norm (norm d) = norm d.