Require Import Decimal Arith ZArith.

Variant digits := d0 | d1 | d2 | d3 | d4 | d5 | d6 | d7 | d8 | d9.

Fixpoint to_list (u : uint) : list digits :=
  match u with
  | Nil => nil
  | D0 u => cons d0 (to_list u)
  | D1 u => cons d1 (to_list u)
  | D2 u => cons d2 (to_list u)
  | D3 u => cons d3 (to_list u)
  | D4 u => cons d4 (to_list u)
  | D5 u => cons d5 (to_list u)
  | D6 u => cons d6 (to_list u)
  | D7 u => cons d7 (to_list u)
  | D8 u => cons d8 (to_list u)
  | D9 u => cons d9 (to_list u)
  end.

Fixpoint of_list (l : list digits) : uint :=
  match l with
  | nil => Nil
  | cons d0 l => D0 (of_list l)
  | cons d1 l => D1 (of_list l)
  | cons d2 l => D2 (of_list l)
  | cons d3 l => D3 (of_list l)
  | cons d4 l => D4 (of_list l)
  | cons d5 l => D5 (of_list l)
  | cons d6 l => D6 (of_list l)
  | cons d7 l => D7 (of_list l)
  | cons d8 l => D8 (of_list l)
  | cons d9 l => D9 (of_list l)
  end.

Lemma of_list_to_list u : of_list (to_list u) = u.

Lemma to_list_of_list l : to_list (of_list l) = l.

Lemma to_list_inj u u' : to_list u = to_list u' -> u = u'.

Lemma of_list_inj u u' : of_list u = of_list u' -> u = u'.

Lemma nb_digits_spec u : nb_digits u = length (to_list u).

Fixpoint lnzhead l :=
  match l with
  | nil => nil
  | cons d l' =>
    match d with
    | d0 => lnzhead l'
    | _ => l
    end
  end.

Lemma nzhead_spec u : to_list (nzhead u) = lnzhead (to_list u).

Definition lzero := cons d0 nil.

Definition lunorm l :=
  match lnzhead l with
  | nil => lzero
  | d => d
  end.

Lemma unorm_spec u : to_list (unorm u) = lunorm (to_list u).

Lemma revapp_spec d d' :
  to_list (revapp d d') = List.rev_append (to_list d) (to_list d').

Lemma rev_spec d : to_list (rev d) = List.rev (to_list d).

Lemma app_spec d d' :
  to_list (app d d') = Datatypes.app (to_list d) (to_list d').

Definition lnztail l :=
  let fix aux l_rev :=
    match l_rev with
    | cons d0 l_rev => let (r, n) := aux l_rev in pair r (S n)
    | _ => pair l_rev O
    end in
  let (r, n) := aux (List.rev l) in pair (List.rev r) n.

Lemma nztail_spec d :
  let (r, n) := nztail d in
  let (r', n') := lnztail (to_list d) in
  to_list r = r' /\ n = n'.

Lemma del_head_spec_0 d : del_head 0 d = d.

Lemma del_head_spec_small n d :
  n <= length (to_list d) -> to_list (del_head n d) = List.skipn n (to_list d).

Lemma del_head_spec_large n d : length (to_list d) < n -> del_head n d = zero.

Lemma nb_digits_0 d : nb_digits d = 0 -> d = Nil.

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

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

Lemma length_lnzhead l : length (lnzhead l) <= length l.

Lemma nb_digits_nzhead u : nb_digits (nzhead u) <= nb_digits u.

Lemma unorm_nzhead u : nzhead u <> Nil -> unorm u = nzhead u.

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

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

Lemma nb_digits_del_head_sub d n :
  n <= nb_digits d ->
  nb_digits (del_head (nb_digits d - n) d) = n.

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

Lemma app_nil_l d : app Nil d = d.

Lemma app_nil_r d : app d Nil = d.

Lemma abs_app_int d d' : abs (app_int d d') = app (abs d) d'.

Lemma abs_norm d : abs (norm d) = unorm (abs d).

Lemma iter_D0_nzhead d :
  Nat.iter (nb_digits d - nb_digits (nzhead d)) D0 (nzhead d) = d.

Lemma iter_D0_unorm d :
  d <> Nil ->
  Nat.iter (nb_digits d - nb_digits (unorm d)) D0 (unorm d) = d.

Lemma nzhead_app_l d d' :
  nb_digits d' < nb_digits (nzhead (app d d')) ->
  nzhead (app d d') = app (nzhead d) d'.

Lemma nzhead_app_r d d' :
  nb_digits (nzhead (app d d')) <= nb_digits d' ->
  nzhead (app d d') = nzhead d'.

Lemma nzhead_app_nil_r d d' : nzhead (app d d') = Nil -> nzhead d' = Nil.

Lemma nzhead_app_nil d d' :
  nb_digits (nzhead (app d d')) <= nb_digits d' -> nzhead d = Nil.

Lemma nzhead_app_nil_l d d' : nzhead (app d d') = Nil -> nzhead d = Nil.

Lemma unorm_app_zero d d' :
  nb_digits (unorm (app d d')) <= nb_digits d' -> unorm d = zero.

Lemma app_int_nil_r d : app_int d Nil = d.

Lemma unorm_app_l d d' :
  nb_digits d' < nb_digits (unorm (app d d')) ->
  unorm (app d d') = app (unorm d) d'.

Lemma unorm_app_r d d' :
  nb_digits (unorm (app d d')) <= nb_digits d' ->
  unorm (app d d') = unorm d'.

Lemma norm_app_int d d' :
  nb_digits d' < nb_digits (unorm (app (abs d) d')) ->
  norm (app_int d d') = app_int (norm d) d'.

Lemma del_head_nb_digits d : del_head (nb_digits d) d = Nil.

Lemma del_tail_nb_digits d : del_tail (nb_digits d) d = Nil.

Lemma del_head_app n d d' :
  n <= nb_digits d -> del_head n (app d d') = app (del_head n d) d'.

Lemma del_tail_app n d d' :
  n <= nb_digits d' -> del_tail n (app d d') = app d (del_tail n d').

Lemma del_tail_app_int n d d' :
  n <= nb_digits d' -> del_tail_int n (app_int d d') = app_int d (del_tail n d').

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

Lemma app_int_del_tail_head n (d:int) :
  n <= nb_digits (abs d) ->
  app_int (del_tail_int n d) (del_head (nb_digits (abs d) - n) (abs d)) = d.

Lemma del_head_app_int_exact i f :
  nb_digits f < nb_digits (unorm (app (abs i) f)) ->
  del_head (nb_digits (unorm (app (abs i) f)) - nb_digits f) (unorm (app (abs i) f)) = f.

Lemma del_tail_app_int_exact i f :
  nb_digits f < nb_digits (unorm (app (abs i) f)) ->
  del_tail_int (nb_digits f) (norm (app_int i f)) = norm i.

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_rev d : rev (rev d) = 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_iter_D0 n u : unorm (Nat.iter n D0 u) = unorm 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_involutive d : nzhead (nzhead d) = nzhead d.

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

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

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

Lemma lnzhead_neq_d0_head l l' : ~(lnzhead l = cons d0 l').

Lemma lnzhead_head_nd0 h t : h <> d0 -> lnzhead (cons h t) = cons h t.

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

Lemma unorm_app_l_nil d d' : nzhead d = Nil -> unorm (app d d') = unorm d'.