Require Import Decimal Arith.

Lemma uint_dec (d d' : uint) : { d = d' } + { d <> d' }.

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_nzhead u : nb_digits (nzhead u) <= nb_digits u.

Lemma del_head_nb_digits (u:uint) : del_head (nb_digits u) u = Nil.

Lemma nb_digits_del_head n u :
  n <= nb_digits u -> nb_digits (del_head n u) = nb_digits u - n.

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
    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 =>
      nth n d
    end
  end.

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

Lemma del_head_nth n u :
  n < nb_digits u ->
  del_head n u = revapp (nth n u) (del_head (S n) u).

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.

Lemma app_del_tail_head (u:uint) n :
  n <= nb_digits u ->
  app (del_tail n u) (del_head (nb_digits u - n) u) = u.

Lemma app_int_del_tail_head n (d:int) :
  let ad := match d with Pos d | Neg d => d end in
  n <= nb_digits ad ->
  app_int (del_tail_int n d) (del_head (nb_digits ad - n) ad) = d.

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

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

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

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 nzhead_D0 u : nzhead (D0 u) = nzhead u.

Lemma nzhead_iter_D0 n u : nzhead (Nat.iter n D0 u) = nzhead u.

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 nzhead_nonzero d d' : nzhead d <> D0 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 del_head_nonnil n u :
  n < nb_digits u -> del_head n u <> Nil.

Lemma del_tail_nonnil n u :
  n < nb_digits u -> del_tail n u <> Nil.

Lemma nzhead_invol d : nzhead (nzhead d) = nzhead d.

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.

Lemma nzhead_del_tail_nzhead_eq n u :
  nzhead u = u ->
  n < nb_digits u ->
  nzhead (del_tail n u) = del_tail n u.

Lemma nzhead_del_tail_nzhead n u :
  n < nb_digits (nzhead u) ->
  nzhead (del_tail n (nzhead u)) = del_tail n (nzhead u).

Lemma unorm_del_tail_unorm n u :
  n < nb_digits (unorm u) ->
  unorm (del_tail n (unorm u)) = del_tail n (unorm u).

Lemma norm_del_tail_int_norm n d :
  n < nb_digits (match norm d with Pos d | Neg d => d end) ->
  norm (del_tail_int n (norm d)) = del_tail_int n (norm d).

Lemma nzhead_app_nzhead d d' :
  nzhead (app (nzhead d) d') = nzhead (app d d').

Lemma unorm_app_unorm d d' :
  unorm (app (unorm d) d') = unorm (app d d').

Lemma norm_app_int_norm d d' :
  unorm d' = zero ->
  norm (app_int (norm d) d') = norm (app_int d d').